A function from to is injective if whenever . An injective function is also called one-to-one or an injection; it is the same as a monomorphism in the category of sets.
A bijection is a function that is both injective and surjective.
In constructive mathematics, a strongly extensional function between sets equipped with tight apartness relations is called strongly injective if whenever (which implies that the function is injective). This is the same as a regular monomorphism in the category of such sets and strongly extensional functions (while any merely injective function, if strongly extensional, is still a monomorphism). Some authors use ‘one-to-one’ for an injective function as defined above and reserve ‘injective’ for the stronger notion.
Since an element in a set in the category of sets is just a global element , one could define injections in any category with a terminal object :
A morphism in is an injection or a one-to-one morphism if, given any two global elements , if .
The term injective morphism is already used in category theory in a different context to mean a morphism with a right lifting property.
In a category with a terminal object , every monomorphism is an injection.
This follows from the definition of a monomorphism.
In a category with a terminal object , every global element is an injection.
By definition of terminal object , the unique global element is the identity morphism of the terminal object. Thus for every global element , for any two global elements , is always true, making an injection.
If the category has a strict initial object , then every morphism is vacuously an injection, since there are no global elements .
Anonymous: Under what conditions are all injections in a category monomorphisms? Obviously injections are monomorphisms in a well-pointed? topos or pretopos (those are models of particular types of set theories), but does that remain true in a (pre)topos without well-pointedness, a coherent category or an exact category?
Anonymous: There is this stackexchange post, but the answers only refer to concrete categories with a forgetful functor to Set and a free functor from Set, rather than arbitrary abstract categories.
Last revised on December 14, 2020 at 02:02:20. See the history of this page for a list of all contributions to it.