A functor is pseudomonic if it is:
faithful; that is, for any pair of objects the component function between hom-sets is injective,
full on isomorphisms, meaning that for any pair of objects the function between the subsets of isomorphisms is surjective (hence bijective).
Arguably, pseudomonic functors are precisely the functors for which it makes sense to say that is uniquely determined by up to unique isomorphism. However, we do not really need faithfulness for this; bijectivity on isos suffices.
More generally, a 1-morphism in any 2-category is called a pseudomonic morphism if the square analogous to that below is a 2-pullback, or equivalently if is a pseudomonic functor for any .
Every fully faithful functor is pseudomonic, and every pseudomonic functor is conservative, as well as essentially injective.
A functor is pseudomonic if and only if the commuting square
is a 2-pullback in Cat (cf. the pullback characterization of 1-monomorphisms, here).
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 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 are called analytic functors. Now taking left Kan extensions along is pseudomonic, and this implies that the coefficients of an analytic functor are unique up to isomorphism.
Aurelio Carboni, Scott Johnson?, Ross Street, Dominic Verity, §2.7 in: Modulated bicategories, Journal of Pure and Applied Algebra 94 (1994) 229-282 [doi:10.1016/0022-4049(94)90009-4, pdf]
G. Max Kelly, Steve Lack, p. 18 of: On property-like structures, Theory and Applications of Categories 3 9 (1997) [tac:3-09, pdf]
Formalization in cubical Agda:
Last revised on June 28, 2024 at 17:50:09. See the history of this page for a list of all contributions to it.