nLab functor comprehension principle

Contents

Context

Category theory

2-category theory

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

Contents

Idea

There are multiple ways to categorify the function comprehension principle from a method of constructing functions to a method of constructing functors. They have in common that they give a method of defining a functor without explicitly defining functions on objects or morphisms. Since one also doesn’t need to prove the action on morphisms is functorial, this can lead to a large reduction in effort, and so these constructions are very commonly used, though not often by a name. These principles become even more useful in higher category theory, due to the combinatorial explosion in coherence conditions at higher dimension.

We describe on this page two formulations that have well-known generalizations to categories. First, the formulation

Every anafunction is the graph of a function.

can be generalized to the statement that every anafunctor is (naturally isomorphic to) the graph of a functor. Since anafunctions/anafunctors are not a commonly used notion (precisely because of the comprehension principles), this principle is usually stated as

Every injective, surjective function has a (necessarily unique) inverse.

and the “anafunctors determine functors” formulation can be rephrased as the more familiar category theoretic principle that every fully faithful, essentially surjective functor has a (necessarily unique up to unique natural isomorphism) inverse.

A second formulation of the function comprehension principle, that is not quite as trivially equivalent, is the following, sometimes called the "axiom/principle of unique choice" for its resemblance in logical structure to a formulation of the axiom of choice:

Given a relation, i.e. a function to a powerset P:APBP : A \to P B, if for every xAx \in A, P(a)P(a) is uniquely inhabited, then PP is equal to the extension of a unique function f:ABf : A \to B by the inclusion i:BP(B)i : B \to P(B) of singletons. That is, P=ifP = i \circ f.

This definition can be cleanly generalized to functors as follows. Given a profunctor, i.e., a functor to a presheaf category P:CPsh(D)P : C \to Psh(D), if for every cCc \in C, P(c)P(c) is representable, then PP is naturally isomorphic to the extension of a unique (up to unique natural isomorphism) functor F:CDF : C \to D by the Yoneda embedding Y:DPsh(D)Y : D \to Psh(D). That is, PYFP \cong Y \circ F. This formulation is sometimes referred to as “parameterized representability”, or simply as an application of the Yoneda lemma.

Every Fully Faithful Eso is an Equivalence

Consider the statement:

If ff is a fully faithful and essentially surjective functor, then it is an equivalence of categories.

If we use a set-theoretic foundation for mathematics, then this statement is equivalent to the axiom of choice. However, as we now show, in the internal logic of a regular 2-category, it is simply true. Thus, it should really be regarded as a “functor comprehension principle” or an “axiom of non-choice,” analogous for categories to the fact (true in any regular 1-category) that any injective and surjective function of sets is an isomorphism, or equivalently that one can always make “choices” when those choices are uniquely specified.

We start by characterizing full, faithful, and eso morphisms in the internal logic.

Faithful morphisms

Consider first the following theory with two 1-types AA and BB:

  • x:Af(x):Bx:A \vdash f(x):B
  • x:A,y:A,α:hom A(x,y),β:hom A(x,y),f(α)=f(β)α=βx:A, y:A, \alpha: hom_A(x,y), \beta : hom_A(x,y), f(\alpha)=f(\beta) \vdash \alpha = \beta

Of course, the first axiom interprets by a morphism f:ABf\colon A\to B. This induces a map from ker(A)(f/f)ker(A) \to (f/f) over A×AA\times A. The context of the second axiom above is the kernel pair of this map (as a map between discrete objects in K/A×AK/A\times A); thus the second axiom asserts that this kernel pair factors through the diagonal of ker(A)ker(A), and hence is monic. But this is equivalent to saying that ff is faithful, so a model of this theory in a lex 2-category is precisely a faithful morphism.

Full and ff morphisms

Now consider the following theory, again with two 1-types AA and BB:

  • x:Af(x):Bx:A \vdash f(x):B
  • x:A,y:A,γ:hom B(f(x),f(y))γ¯:hom A(x,y).f(γ¯)=γx:A, y:A, \gamma: hom_B(f(x),f(y)) \vdash \exists \bar{\gamma}:hom_A(x,y). f(\bar{\gamma})=\gamma

In a regular 2-category, the truth of this axiom asserts that the map ker(A)(f/f)ker(A) \to (f/f) is eso, which implies that ff is a full morphism. The converse is true at least in an exact 2-category. It is also true if ff is additionally faithful, since then ker(A)(f/f)ker(A) \to (f/f) is ff, hence (if also eso) an equivalence, so that ff is ff (and in particular full). Therefore, a model of the combined theory

  • x:Af(x):Bx:A \vdash f(x):B
  • x:A,y:A,α:hom A(x,y),β:hom A(x,y),f(α)=f(β)α=βx:A, y:A, \alpha: hom_A(x,y), \beta : hom_A(x,y), f(\alpha)=f(\beta) \vdash \alpha = \beta
  • x:A,y:A,γ:hom B(f(x),f(y))γ¯:hom A(x,y).f(γ¯)=γx:A, y:A, \gamma: hom_B(f(x),f(y)) \vdash \exists \bar{\gamma}:hom_A(x,y). f(\bar{\gamma})=\gamma

in a regular 2-category is precisely a ff morphism.

In a merely lex 2-category, we can instead consider the theory

  • x:Af(x):Bx:A \vdash f(x):B
  • x:A,y:A,α:hom A(x,y),β:hom A(x,y),f(α)=f(β)α=βx:A, y:A, \alpha: hom_A(x,y), \beta : hom_A(x,y), f(\alpha)=f(\beta) \vdash \alpha = \beta
  • x:A,y:A,γ:hom B(f(x),f(y))γ¯:hom A(x,y)x:A, y:A, \gamma: hom_B(f(x),f(y)) \vdash \bar{\gamma}:hom_A(x,y)
  • x:A,y:A,γ:hom B(f(x),f(y))f(γ¯)=γx:A, y:A, \gamma: hom_B(f(x),f(y)) \vdash f(\bar{\gamma})=\gamma

The first two axioms give a faithful morphism f:ABf\colon A\to B, as above, and now the third and fourth axioms supply a section of the map ker(A)(f/f)ker(A) \to (f/f), which is thus both ff and split epic, hence an equivalence. Thus, a model of this theory in a lex 2-category is also precisely a ff morphism.

I don’t know whether there is a theory in lex 2-logic whose models in lex 2-categories are precisely full morphisms, but I suspect not. I also don’t know whether there is a theory in regular 2-logic whose models in non-exact regular 2-categories are precisely full morphisms.

Eso morphisms

Now consider the regular 2-theory

  • x:Af(x):Bx:A \vdash f(x):B
  • y:Bx:A.i:iso B(f(x),y)y:B \vdash \exists x:A. \exists i:iso_B(f(x),y)

Since iso B(f(x),y)iso_B(f(x),y) in context x:A,y:Bx:A,y:B is interpreted by (1,f):AA×B(1,f)\colon A\to A\times B, the second axiom asserts that the image of the composite A(1,f)A×BBA \overset{(1,f)}{\to} A\times B \to B is all of BB, i.e. that this composite is eso. But this composite is clearly just ff, so a model of this theory is precisely an eso morphism.

Of course, we can then write the combined theory

  • x:Af(x):Bx:A \vdash f(x):B
  • x:A,y:A,γ:hom B(f(x),f(y))γ¯:hom A(x,y).f(γ¯)=γx:A, y:A, \gamma: hom_B(f(x),f(y)) \vdash \exists \bar{\gamma}:hom_A(x,y). f(\bar{\gamma})=\gamma
  • y:Bx:A.i:iso B(f(x),y)y:B \vdash \exists x:A. \exists i:iso_B(f(x),y)

whose models in exact 2-categories are precisely the eso+full morphisms.

Equivalences

It follows from the above considerations that a model of the following theory:

  • x:Af(x):Bx:A \vdash f(x):B
  • x:A,y:A,α:hom A(x,y),β:hom A(x,y),f(α)=f(β)α=βx:A, y:A, \alpha: hom_A(x,y), \beta : hom_A(x,y), f(\alpha)=f(\beta) \vdash \alpha = \beta
  • x:A,y:A,γ:hom B(f(x),f(y))γ¯:hom A(x,y).f(γ¯)=γx:A, y:A, \gamma: hom_B(f(x),f(y)) \vdash \exists \bar{\gamma}:hom_A(x,y). f(\bar{\gamma})=\gamma
  • y:Bx:A.i:iso B(f(x),y)y:B \vdash \exists x:A. \exists i:iso_B(f(x),y)

in a regular 2-category is precisely a morphism ff which is ff and eso, i.e. an equivalence. Since this theory evidently asserts that ff is “faithful, full, and essentially surjective on objects” in the internal logic, this is the desired “functor comprehension principle.”

Of course, in a Heyting 2-category, the latter three axioms can equivalently be stated as

  • x:A,y:A,α:hom A(x,y),β:hom A(x,y),f(α)=f(β)α=β\vdash \forall x:A, \forall y:A, \forall \alpha: hom_A(x,y), \forall \beta : hom_A(x,y), f(\alpha)=f(\beta) \Rightarrow \alpha = \beta
  • x:A,y:A,γ:hom B(f(x),f(y)),γ¯:hom A(x,y).f(γ¯)=γ\vdash \forall x:A, \forall y:A, \forall \gamma: hom_B(f(x),f(y)), \exists \bar{\gamma}:hom_A(x,y). f(\bar{\gamma})=\gamma
  • y:B,x:A.i:iso B(f(x),y)\vdash \forall y:B, \exists x:A. \exists i:iso_B(f(x),y)

which have perhaps the most familiar form.

Every Point-wise Representable Profunctor is the graph of a Functor

Let P:CPsh(D)P : C \to Psh(D) be a profunctor that is point-wise representable in that for each cCc \in C, we have a F 0(c)F_0(c) with a natural isomorphism e c:Y(F 0(c))P(c)e_c : Y(F_0(c)) \cong P(c). Then we can extend this F 0F_0 to a functor F:CDF : C \to D as follows. Given f:C(c,c)f : C(c,c'), the functorial action of PP gives a natural transformation P(f):P(c)P(c)P(f) : P(c) \to P(c'). We can compose this with the natural isomorphisms to get a natural transformation e cP(f)e c 1:Y(F 0(c))Y(F 0(c))e_c \circ P(f) \circ e_{c'}^{-1} : Y(F_0(c)) \to Y(F_0(c')). Since the Yoneda embedding is fully faithful, there is a unique F(f)F(f) such that Y(F(f))=e cP(f)e c 1Y(F(f)) = e_c \circ P(f) \circ e_{c'}^{-1}. This action preserves identity and composition by straightforward calculation, and we can define a natural isomorphism e:YFPe : Y \circ F \cong P.

For more see representability determines functoriality, which should eventually be merged with this page.

References

The definitions and observations on the first given formulation of the principle are originally due to

Last revised on November 4, 2024 at 19:20:38. See the history of this page for a list of all contributions to it.