nLab internal profunctor




For any category SS with pullbacks, it is easy to define the notion of category in SS, and the definition of an internal functor between such is similarly straightforward. But it is not so obvious how to define presheaves on internal categories, because they must land in the ambient category SS.

The solution lies in thinking of presheaves on an ordinary category CC, and more generally profunctors CDC ⇸ D, as giving sets equipped with an action of the arrows of C,DC,D, i.e. as their categories of elements.


Here is the slick definition: let SS be a category with pullbacks. Then the bicategory Prof(S)Prof(S) of internal categories, profunctors and transformations in SS is defined to be Mod(Span(S))Mod(Span(S)), the category of monads and bimodules in Span(S)Span(S), the bicategory of spans in SS.

So an internal profunctor CDC ⇸ D between internal categories CC and DD is a bimodule from CC to DD. An internal presheaf on CC is a right CC-module, or equivalently a bimodule C1C ⇸ 1, where 11 is the discrete category on the terminal object of SS (as long as SS has one, of course).

An internal presheaf in SS is the same thing as an internal diagram in SS.


Recall that an internal category CC in SS is a monad in Span(S)Span(S), and so has an underlying span (s,t):C 1C 0(s,t) : C_1 \rightrightarrows C_0. Given C,DCat(S)C,D \in Cat(S), a bimodule H:CDH : C ⇸ D must be given by a span H:C 0HD 0H : C_0 \leftarrow H \to D_0, together with a right action HCHH \circ C \to H of CC and a left action DHHD \circ H \to H of DD that are compatible in the sense described at module over a monad.

Composition of spans is given by pullback, so the action of CC on HH is given by a morphism of spans H r:C 1× C 0HHH_r : C_1 \times_{C_0} H \to H, where the pullback is

C 1× C 0H H C 1 t C 0 \array{ C_1 \times_{C_0} H & \to & H \\ \downarrow & & \downarrow \\ C_1 & \underset{t}{\to} & C_0 }

To say that H rH_r is a morphism of spans is to require that

C 1× C 0H H C 1 s C 0 \array{ C_1 \times_{C_0} H & \to & H \\ \downarrow & & \downarrow \\ C_1 & \underset{s}{\to} & C_0 }

commutes. This action must satisfy unit and associativity axioms expressing functoriality of the corresponding presheaf. Similarly, H :H× D 0D 1HH_\ell : H \times_{D_0} D_1 \to H, where the pullback is along ss, so that this represents a copresheaf. Finally, compatibility of the two actions represents bifunctoriality of the profunctor.

Last revised on May 12, 2023 at 15:39:03. See the history of this page for a list of all contributions to it.