nLab Inj

Idea

$Inj$ (or $Set_inj$) is the wide subcategory of the topos Set with its morphisms restricted to monomorphisms (injective functions).

• The arrow category $Inj^\to$ of $Inj$ is, in turn, a wide subcategory of the quasitopos Mono of set monomorphisms. The two categories have the same objects, namely injective functions, but in Mono the morphism are arbitrary commutative squares from one injection to another, whereas in $Inj^\to$ the other two arrows in the commutative square must also be injective. Note that $Mono$ is a reflective subcategory of the presheaf topos $Set^{\to}$ (the Sierpinski topos), and the category of separated presheaves for the double negation topology on $Set^\to$.

• For a set $S$, its power set ($\mathcal{P}S$ or $2^S$) is the slice category $Inj/S$ which has objects that are injections to $S$ and morphisms that are injections of injections that form commuting triangles. $2^S$ is a quasitopos because it is a Heyting algebra.

Related concepts

• Surj
• FinInj