nLab bijective-on-objects functor




The concept of an identity-on-objects functor is important for defining various structures in category theory, such as Freyd categories and dagger categories. However, in a structural set theory such as ETCS or SEAR, there is no concept of equality of sets, and thus, an identity-on-objects functor cannot be defined via the usual definition. Instead, equality of sets is expressed through bijection of sets, which, when applied to the definition of identity-on-objects functor, yields a bijective-on-objects functor.

In foundations where categories are weak by default and thus the collection of objects do not form a set, the concept of a bijective-on-objects functor still makes sense for strict categories, where the functor is a strict functor by definition.

Another motivation for bijective-on-objects functors is that they together with full and faithful strict functors form an orthogonal factorization system on StrCat; see bo-ff factorization system. This factorization system can also be constructed using a generalized kernel.



A strict functor between two strict categories AA and BB is called bijective-on-objects, or bo, if it is a bijection on objects, if its underlying object function F ob:ob(A)โ†’ob(B)F_{ob}: ob(A) \to ob(B) is a bijection F ob:ob(A)โ‰ƒob(B)F_{ob}: ob(A) \simeq ob(B).

Principle of equivalence

To be more in accord with the principle of equivalence, one could require that the functor be bijective on objects only up to isomorphism; that is, it is essentially surjective and full on isomorphisms. However, from the point of view of factorization systems, the version of the concept of a bo functor which is in accord with the principle of equivalence is nothing more or less than an essentially surjective functor, since essentially surjective functors and ff functors form a bicategorical factorization system on the bicategory CatCat.


R. Street in Categorical and combinatorial aspects of descent theory proves

Proposition. A functor is bijective on objects if and only if it exhibits its codomain as the (2-categorical) codescent object of some simplicial category.

This can be generalized to any regular 2-category.

Relation to equivalent-on-objects functors

Every bijective-on-objects functor between two strict categories is an equivalent-on-objects functor between two strict categories.

Relation to identity-on-objects functors

In the context of type theory, if both strict categories live in a univalent universe ๐’ฐ\mathcal{U}, a bijective-on-objects functor also becomes an identity-on-objects functor due to the univalence axiom and the fact that equivalences between sets are equivalent to bijections of sets:

For sets A:๐’ฐA:\mathcal{U} and B:๐’ฐB:\mathcal{U}, there is an identity type A= ๐’ฐBA =_\mathcal{U} B, a type of equivalences between AA and BB, Aโ‰ƒ ๐’ฐBA \simeq_\mathcal{U} B, and a type of bijections between AA and BB, Aโ‰… ๐’ฐBA \cong_\mathcal{U} B, as well as canonical canonical functions IdtoEquiv:A= ๐’ฐBโ†’Aโ‰ƒ ๐’ฐB\mathrm{IdtoEquiv}:A =_\mathcal{U} B \to A \simeq_\mathcal{U} B and IdtoBij:A= ๐’ฐBโ†’Aโ‰… ๐’ฐB\mathrm{IdtoBij}:A =_\mathcal{U} B \to A \cong_\mathcal{U} B.

Since between equivalences between sets are equivalent to bijections between sets, there is a function EquivtoBij:Aโ‰ƒ ๐’ฐBโ‰ƒAโ‰… ๐’ฐB\mathrm{EquivtoBij}:A \simeq_\mathcal{U} B \simeq A \cong_\mathcal{U} B which is an equivalence of types.

Since ๐’ฐ\mathcal{U} is univalent, IdtoEquiv\mathrm{IdtoEquiv} is an equivalence of types IdtoEquiv:A= ๐’ฐBโ‰ƒAโ‰ƒ ๐’ฐB\mathrm{IdtoEquiv}:A =_\mathcal{U} B \simeq A \simeq_\mathcal{U} B. By the properties of equivalences, the function IdtoBij\mathrm{IdtoBij} is also an equivalence of types IdtoBij:A= ๐’ฐBโ‰ƒAโ‰… ๐’ฐB\mathrm{IdtoBij}:A =_\mathcal{U} B \simeq A \cong_\mathcal{U} B. Thus there is a homotopy inverse BijtoId:Aโ‰ƒ ๐’ฐBโ†’A= ๐’ฐB\mathrm{BijtoId}:A \simeq_\mathcal{U} B \to A =_\mathcal{U} B.

Thus, in an univalent universe, bijective-on-objects functors and identity-on-objects functors are the same:


An identity-on-objects functor F:Aโ†’BF: A\to B between strict categories AA and BB in a univalent universe ๐’ฐ\mathcal{U} is a strict functor with an identification BijtoId(F ob):ob(A)= ๐’ฐob(B)\mathrm{BijtoId}(F_{ob}):ob(A) =_\mathcal{U} ob(B), where F ob:ob(A)โ†’ob(B)F_{ob}: ob(A) \to ob(B) is the underlying object function of the functor FF.

basic properties ofโ€ฆ

Last revised on August 24, 2022 at 11:44:48. See the history of this page for a list of all contributions to it.