nLab representability determines functoriality

Contents

Contents

Idea

If a functor represents a given profunctor, then the action of the functor on morphisms is determined by the action of the profunctor and the representation isomorphism.

This theorem can make it easier to define certain adjoint functors, and is also implicit in type theory where type connectives are presentation of functors, but the action on morphisms is derivable rather than primitive.

Statement

Let R:CR : C D D be a profunctor, i.e., a functor from D op×CSetD^{op}\times C \to Set and F:CDF : C\to D a functor that represents it by a natural isomorphism α:RD(,F=)\alpha : R \Rightarrow D(-,F=). Then the action of FF on morphisms is determined by R,αR,\alpha by the formula:

F(f:cc)=α(R(id Fc,f)(α 1(id Fc)))F(f : c \to c') = \alpha \Big( R(id_{F c}, f)\big(\alpha^{-1}(id_{F c})\big) \Big)

or the following composite acting on id Fcid_{F c}:

D(Fc,Fc)α 1R(Fc,c)R(id Fc,f)R(Fc,c)αD(Fc,Fc) D(F c, F c) \xrightarrow{\alpha^{-1}} R (Fc, c) \xrightarrow{R (id_{F c}, f)} R (F c, c') \xrightarrow{\alpha} D(F c, F c')

Representation Presentation of a Functor

Since the action of the functor on morphisms is determined by the data of a representation of a profunctor, we can even define the functor by giving that data. Crucially though, what does it mean for α\alpha to be natural if we have not yet defined the action of FF? It turns out that it is sufficient to require naturality in DD only. Furthermore, α 1\alpha^{-1} can be recovered from its action on the identity by the Yoneda lemma.

A right functor presentation from CC to DD consists of

  1. A profunctor R:CR : C D D.
  2. An object function F 0:C 0D 0F_0 : C_0 \to D_0.
  3. An “introduction rule” ι c,d:R(d,c)D(d,F 0c)\iota_{c,d} : R(d,c) \to D(d,F_0c).
  4. A “universal morphism” ϵ c:R(F 0c,c)\epsilon_c : R(F_0c,c).

satisfying

  1. left-naturality of ι\iota, meaning ιR(f,id)=D(f,id)ι\iota \circ R(f,id) = D(f,id) \circ \iota
  2. isomorphism, R(,id)(ϵ)R(-,id)(\epsilon) is an inverse to ι\iota.
Theorem

Given a profunctor R:CR : C D D, right functor presentations representing RR are in bijection with functors F:CDF : C \to D with a natural isomorphism α c,d:R(c,d)D(c,Fd)\alpha_{c,d} : R(c,d) \equiv D(c,Fd).

Given a right functor presentation (R,F 0,ι,ϵ)(R, F_0, \iota, \epsilon), we can define a functor that represents RR by extending FF to act on morphisms by F 1(f)=ι(R(id,f)(c))F_1(f) = \iota(R(id, f)(c)). Then the functoriality of FF and naturality of α\alpha and α 1\alpha^{-1} follow from the above equalities.

Given a functor representing RR, the universal morphism is defined as in the Yoneda lemma: ϵ c=α 1(id)\epsilon_c = \alpha^{-1}(id).

In Type Theory

A right functor presentation consists of exactly the data that define a negative type in type theory. The introduction rule of the presentation, unsurprisingly corresponds to the introduction rule in the type theory. The universal morphism corresponds to the (0 or more) elimination rules that are collected into R(c,F 0c)R(c,F_0 c). Left-naturality corresponds to the definition of substitution for the introduction rule. The isomorphism property corresponds to the β\beta and η\eta equalities.

This theorem is usually not explicitly invoked in initiality theorems for type theories, but gives an explanation for why the “dogma” of introduction and elimination rules is so effective in practice.

Examples

  1. Decategorifying to the poset case, we get that if a function f:ABf : A \to B represents a “relational profunctor” RR , i.e. a subset RA×BR \subseteq A \times B that is downward closed in AA and upper closed in BB, then ff is monotone.
  2. Consider the cartesian product functor, which can be defined by saying that it represents the profunctor R ×:C 2R_{\times} : C^2 C C defined by
    R ×(a,(b 1,b 2))=C(a,b 1)×C(a,b 2) R_{\times}\big(a,(b_1,b_2)\big) = C(a,b_1) \times C(a,b_2)

whose action is defined as R ×(f,(g,h))(k,l)=(gkf,hlf)R_{\times}(f,(g,h))(k,l) = (g \circ k \circ f, h \circ l \circ f). Then the universal property of the product functor ×:C 2C\times : C^2 \to C is encapsulated in the natural isomorphism α a,b 1,b 2:R ×(a,(b 1,b 2))C(a,b 1×b 2)\alpha_{a,b_1,b_2} : R_{\times}(a,(b_1,b_2)) \Rightarrow C(a,b_1\times b_2). By the Yoneda lemma, the inverse of α\alpha can be reconstructed from its action on the identity, which in this case gives us the two projections: (π 1,π 2)=α b 1×b 2,b 1,b 2 1(id)(\pi_1,\pi_2) = \alpha^{-1}_{b_1\times b_2, b_1,b_2}(id).

Then, by the above theorem, the action of ×\times on functions is equal to:

f×g=α(fπ 1,gπ 2)f \times g = \alpha(f \circ \pi_1, g \circ \pi_2)

References

A similar theorem, but for presenting adjoint functors without defining RR first is given (and generalized to the internal setting) in

Last revised on February 19, 2024 at 17:05:25. See the history of this page for a list of all contributions to it.