nLab pseudomonic functor

Contents

Contents

Definition

A functor F:CDF: C \to D is pseudomonic if

  1. it is faithful; that is, for any pair of objects x,yCx,y\in C the component function F:C(x,y)D(Fx,Fy)F \colon C(x,y) \to D(F x,F y) between hom-sets is injective, and

  2. it is full on isomorphisms, meaning that for any pair of objects x,yCx,y\in C the function F:Iso C(x,y)Iso D(Fx,Fy)F \colon Iso_C(x,y) \to Iso_D(F x, F y) to the set of isomorphisms between them is surjective (hence bijective), where Iso C(x,y)Iso_C(x,y).

More generally, a 1-morphism f:CDf \colon C\to D in any 2-category KK is called a pseudomonic morphism if the square analogous to that below is a 2-pullback, or equivalently if K(X,C)K(X,D)K(X,C)\to K(X,D) is a pseudomonic functor for any XX.

Properties

Every fully faithful functor is pseudomonic, and every pseudomonic functor is conservative, as well as essentially injective. In fact, being full on isomorphisms is exactly what essential injectivity means.

A functor F:CDF \colon C \to D is pseudomonic if and only if the commuting square

C Id C Id F C F D \array{ C &\overset{Id}{\longrightarrow}& C \\ \Big\downarrow\mathrlap{^{Id}} && \Big\downarrow\mathrlap{{}^F} \\ C &\underset{F}{\longrightarrow}& D }

is a 2-pullback in Cat (cf. the pullback characterization of 1-monomorphisms, here).

Examples

An interesting example of the notion appears in the context of Joyal’s combinatorial species of structures.

A combinatorial species is a functor from the category BijBij of finite sets and bijections between them to Set, and the functors that are obtained by taking left Kan extensions of species along the subcategory-inclusion I:BijSetI \colon Bij \to Set are called analytic functors. Now taking left Kan extensions along II is pseudomonic, and this implies that the coefficients of an analytic functor are unique up to isomorphism.

Arguably, pseudomonic functors are precisely the functors for which it makes sense to say that AA is uniquely determined by FAF A up to unique isomorphism. However, we do not really need faithfulness for this; bijectivity on isos suffices.

References

Formalization in cubical Agda:

Last revised on September 22, 2023 at 12:06:06. See the history of this page for a list of all contributions to it.