surjection

**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 $f$ (of sets) from $A$ to $B$ is **surjective** if, given any element $y$ of $B$, $y = f(x)$ for some $x$. A surjective function is also called **onto** or a **surjection**; it is the same as an epimorphism in the category of sets.

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

In classical set theory, one writes $|B| \leq^* |A|$ to mean that either there is a surjection $A \to B$ *or* $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_{inh}$ of inhabited sets and surjections.

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

Contrast with the notation $|B| \leq |A|$ if there is an injection $B\to A$. Since subobjects are subquotients (e.g. we can take $B'=B$ above), $|B| \leq |A|$ implies $|B| \leq^* |A|$. (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: $|B| \leq^* |A|$ implies $|B| \leq |A|$, and so $|B| \leq^* |A|$ iff $|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 $X$ there is a set $Y$ such that for every surjection $q\colon Z \to X$ there is a function $s\colon Y \to Z$ such that $q\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 $X$ the full subcategory of $Set/X$ on the surjections: every fibre has a weakly initial object.

Revised on July 12, 2017 12:13:54
by Mike Shulman
(76.167.222.204)