nLab
Inj

InjInj (or Set injSet_inj) is the wide subcategory of the topos Set with its morphisms restricted to monomorphisms (injective functions).

  • The arrow category Inj Inj^\to of InjInj is, in turn, a wide subcategory of the quasitopos#mono? 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 Inj^\to the other two arrows in the commutative square must also be injective. Note that MonoMono is a reflective subcategory of the presheaf topos Set Set^{\to} (the Sierpinski topos), and the category of separated presheaves for the double negation topology? on Set Set^\to.

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

See also

  • Surj?

Last revised on September 8, 2017 at 15:48:36. See the history of this page for a list of all contributions to it.