nLab surjection

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Definition

A function ff (of sets) from AA to BB is surjective if, given any element yy of BB, y=f(x)y = f(x) for some xx. A surjective function is also called onto or a surjection.

Surjections are the same as epimorphisms in the category of sets and effective epimorphisms in the (infinity,1)-category of sets.

A bijection is a function that is both surjective and injective.

The surjection preorder

In classical set theory, one writes |B| *|A||B| \leq^* |A| to mean that either there is a surjection ABA \to B or B=B=\empty. The relation *\leq^* is a preorder on the class of all sets, and its restriction to inhabited sets is the preorder reflection of the category Surj inhSurj_{inh} of inhabited sets and surjections.

To make this definition less piecemeal and more constructive, one can define |B| *|A||B| \leq^* |A| to mean BB is a subquotient of AA, in other words one has a surjection BBB' \to B and an injection BAB' \to A. For BB inhabited and a subquotient of AA, excluded middle implies there is a surjection from AA to BB, so in classical mathematics this coincides with the piecemeal definition.

Contrast with the notation |B||A||B| \leq |A| if there is an injection BAB\to A. Since subobjects are subquotients (e.g. we can take B=BB'=B above), |B||A||B| \leq |A| implies |B| *|A||B| \leq^* |A|. (If we wanted to prove this using the piecemeal definition, we would require excluded middle.)

Axioms of choice

The axiom of choice states precisely that every surjection in the category of sets has a section. Thus in this setting one has: |B| *|A||B| \leq^* |A| implies |B||A||B| \leq |A|, and so |B| *|A||B| \leq^* |A| iff |B||A||B| \leq |A| assuming AC. Some authors who doubt the axiom of choice use the term ‘onto’ for a surjection as defined above and reserve ‘surjective’ for the stronger notion of a function with a section (a split epimorphism).

The axiom WISC has an equivalent statement (that works in any Boolean topos) due to François Dorais phrased almost entirely in terms of surjections (or epimorphisms):

For every set XX there is a set YY such that for every surjection q:ZXq\colon Z \to X there is a function s:YZs\colon Y \to Z such that qs:YXq\circ s\colon Y\to X is a surjection.

One can view this as really a statement about the Grothendieck fibration over Set with fibre over XX the full subcategory of Set/XSet/X on the surjections: every fibre has a weakly initial object.

In other categories

Since an element aa in a set AA in the category of sets is just a global element a:1Aa:1\rightarrow A, one could define surjections in any category 𝒞\mathcal{C} with a terminal object 11:

Definition

A morphism f:ABf:A\rightarrow B in a category 𝒞\mathcal{C} with a terminal object 11 is called a surjection. a surjective morphism, or an onto morphism if, given any global element y:1By:1\rightarrow B, there exists a global element x:1Ax:1\rightarrow A such that y=fxy = f \circ x.

Remark

Some authors regard surjection as a synonym of split epimorphism, and only use ‘onto’ for the definition above.

Proposition

In a category 𝒞\mathcal{C} with a terminal object 11, the unique morphism !:A1!:A\rightarrow 1 is a surjection for every object AA.

Proof

By definition of a terminal object, for every object AA there exists a unique morphism !:A1!:A\rightarrow 1, and the identity morphism is the unique global element 1 1:111_{1}:1\rightarrow 1. The composite of a global element x:1Ax:1\rightarrow A with the function !:A1!:A\rightarrow 1 results in a function !x:11! \circ x:1\rightarrow 1, which by definition of a terminal object is the same as 1 1:111_{1}:1\rightarrow 1. Since !x=1 1! \circ x = 1_{1}, for every object AA, !:A1!:A\rightarrow 1 is a surjection.

Proposition

In a category of pointed objects 𝒞\mathcal{C}, every morphism f:ABf:A\rightarrow B is a surjection for every object AA.

Proof

A pointed object in a category with terminal objects is a object AA with a global element a:1Aa:1\rightarrow A to the object, and morphisms in the category preserve the global element, which means there is only a unique global element for each object AA. Therefore, for every morphism f:ABf:A\rightarrow B and global element y:1By:1\rightarrow B, there exists a global element x:1Ax:1\rightarrow A such that y=fxy = f \circ x.

Just because a morphism is a surjection in a concrete category does not mean that the morphism in the underlying category of sets is a surjection; equivalently, the forgetful functor from any category 𝒞\mathcal{C} to Set does not preserve surjections.

Well-pointedness

The fact that surjections are epimorphisms in Set is a result of the fact that Set is well-pointed. This could be generalised to any category with a terminal separator 11.

Proposition

In a category 𝒞\mathcal{C} with a terminal object 11 such that 11 is a separator, every surjection is an epimorphism.

Proof

For any surjection f:ABf:A\rightarrow B, suppose there are parallel morphisms g,h:BCg, h:B\rightarrow C such that there gf=hfg \circ f = h \circ f (a fork). Then for every global element y:1By:1\rightarrow B there exists a global element x:1Ax:1\rightarrow A such that y=fxy = f \circ x, and thus gy=gfxg \circ y = g \circ f \circ x and hy=hfxh \circ y = h \circ f \circ x. But since gf=hfg \circ f = h \circ f, gfx=hfxg \circ f \circ x = h \circ f \circ x, which implies that gy=hyg \circ y = h \circ y. Since 11 is a separator, then for every global element y:1By:1\rightarrow B, if gy=hyg \circ y = h \circ y, then g=hg = h. Therefore, every surjection is an epimorphism.

Axiom of choice

The axiom of choice for surjections in Set is the following statement:

This axiom could be defined in every category with a terminal object, and could be contrasted with the axiom of choice for epimorphisms, as not every epimorphism is an surjection, nor is every surjection an epimorphism.

Proposition

In a category 𝒞\mathcal{C} with a terminal object 11 and binary equalisers such that every surjection is a split epimorphism, the terminal object 11 is a separator.

Proof

Suppose there are parallel morphisms g,h:BCg, h:B\rightarrow C such that for every global element y:1By:1\rightarrow B, gy=hyg \circ y = h \circ y. One could construct an equaliser f:eq(g,h)Bf:eq(g,h)\rightarrow B, which implies that gf=hfg \circ f = h \circ f and that for any global element x:1eq(g,h)x:1\rightarrow eq(g,h), gfx=hfxg \circ f \circ x = h \circ f \circ x. This implies that for every global element y:1By:1\rightarrow B, there exists a global element x:1eq(g,h)x:1\rightarrow eq(g,h) where y=fxy = f \circ x, and the equaliser f:eq(g,h)Bf:eq(g,h)\rightarrow B is a surjection. Since every surjection is a split epimorphism, ff has a section i:Beq(g,h)i:B\rightarrow eq(g,h) such that fi=1 Bf \circ i = 1_{B}, the identity morphism on BB, gfi=hfig \circ f \circ i = h \circ f \circ i, g1 B=h1 Bg \circ 1_{B} = h \circ 1_{B}, and g=fg = f. Because for every global element y:1By:1\rightarrow B, gy=hyg \circ y = h \circ y implies g=hg = h, the terminal object 11 is a separator.

Last revised on December 9, 2023 at 07:32:09. See the history of this page for a list of all contributions to it.