natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
A function (of sets) from to is surjective if, given any element of , for some . 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.
In classical set theory, one writes to mean that either there is a surjection or . The relation is a preorder on the class of all sets, and its restriction to inhabited sets is the preorder reflection of the category of inhabited sets and surjections.
To make this definition less piecemeal and more constructive, one can define to mean is a subquotient of , in other words one has a surjection and an injection . For inhabited and a subquotient of , excluded middle implies there is a surjection from to , so in classical mathematics this coincides with the piecemeal definition.
Contrast with the notation if there is an injection . Since subobjects are subquotients (e.g. we can take above), implies . (If we wanted to prove this using the piecemeal definition, we would require excluded middle.)
The axiom of choice states precisely that every surjection in the category of sets has a section. Thus in this setting one has: implies , and so iff 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 there is a set such that for every surjection there is a function such that is a surjection.
One can view this as really a statement about the Grothendieck fibration over Set with fibre over the full subcategory of on the surjections: every fibre has a weakly initial object.
Since an element in a set in the category of sets is just a global element , one could define surjections in any category with a terminal object :
A morphism in a category with a terminal object is called a surjection. a surjective morphism, or an onto morphism if, given any global element , there exists a global element such that .
Some authors regard surjection as a synonym of split epimorphism, and only use ‘onto’ for the definition above.
In a category with a terminal object , the unique morphism is a surjection for every object .
By definition of a terminal object, for every object there exists a unique morphism , and the identity morphism is the unique global element . The composite of a global element with the function results in a function , which by definition of a terminal object is the same as . Since , for every object , is a surjection.
In a category of pointed objects , every morphism is a surjection for every object .
A pointed object in a category with terminal objects is a object with a global element to the object, and morphisms in the category preserve the global element, which means there is only a unique global element for each object . Therefore, for every morphism and global element , there exists a global element such that .
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 to Set does not preserve surjections.
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 .
In a category with a terminal object such that is a separator, every surjection is an epimorphism.
For any surjection , suppose there are parallel morphisms such that there (a fork). Then for every global element there exists a global element such that , and thus and . But since , , which implies that . Since is a separator, then for every global element , if , then . Therefore, every surjection is an epimorphism.
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.
In a category with a terminal object and binary equalisers such that every surjection is a split epimorphism, the terminal object is a separator.
Suppose there are parallel morphisms such that for every global element , . One could construct an equaliser , which implies that and that for any global element , . This implies that for every global element , there exists a global element where , and the equaliser is a surjection. Since every surjection is a split epimorphism, has a section such that , the identity morphism on , , , and . Because for every global element , implies , the terminal object 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.