nLab doubly indexed category

Contents

Contents

Idea

Informally a doubly indexed category is a unitary lax double functor F: atF : \mathbb{C}^\top \to \mathbf{\mathbb{C}at}, where the latter is the proarrow equipment of categories, functors, profunctors and natural transformations.

Formally, it is a right \mathbb{C}-module, i.e. it’s a right action of the double category \mathbb{C}.

With this name, they were defined by David Jaz Myers in his book on categorical system theory.

Definition

Definition

Let =C 1s,tC 0\mathbb{C} = \mathbf{C}_1 \overset{s,t}\rightrightarrows \mathbf{C}_0 be a double category, presented as a pseudomonad in Span(Cat)\mathbf Span(Cat). A doubly indexed category over \mathbb{C} is a right \mathbb{C}-module, meaning it consists of a functor π:FC 0\pi : \mathbf F \to C_0 together with a map *:C 1× C 0FF* : \mathbf{C}_1 \times_{C_0} \mathbf{F} \to \mathbf{F} over C 0\mathbf{C}_0, satisfying the laws of unitality and functoriality of a module.

The reason one can see this data as given by a unitary lax double functor F: atF : \mathbb{C}^\top \to \mathbf{\mathbb{C}at} is the following. First, the data of the functor π:FC 0\pi: \mathbf F \to C_0 in itself is equivalent to that of a unitary lax 2-functor into Prof\mathbf{Prof}, i.e. a displayed category (see there for an explanation). This means objects of \mathbb{C} are sent to categories (the fibers of π\pi) while horizontal maps (tight maps) in \mathbb{C} act ‘profunctorially’ on them. This assignment is unitary and lax.

Then the action ** gives, for each vertical morphism (loose maps) in \mathbb{C}, a functor. Explicitly, if f:xyf: x \to y is a vertical map in \mathbb{C}, and a:F(x)=π 1(x)a : F(x) = \pi^{-1}(x), then F(f)(a)=f*a:F(y)F(f)(a) = f * a : F(y).

This part of the action is strict, or at least pseudofunctorial.

Examples

One of the central exampls of doubly indexed category is given by the ‘self double-indexing’ any finitely complete category C\mathbf{C} induces. Specifically, it’s the action C/\mathbf{C}/- of Span(C)\mathbf{Span(C)}.

It is defined as follows:

  1. An object x:Cx : \mathbf{C} is sent to the slice category C/x\mathbf{C}/x
  2. A morphism f:xyf:x \to y is sent to the profunctor C/f:C/x op×C/yC\mathbf{C}/f: \mathbf{C}/x^{\mathrm{op}} \times \mathbf{C}/y \to \mathbf{C} that sends maps p:axp : a \to x, q:byq:b \to y to the set of maps h:abh:a \to b that make the square commute:
    C/f(p,q):={a h b p q x f y} \mathbf{C}/f(p, q) := \left\{ \begin{matrix} \ a & \overset{h}\to & b\ \\ p \downarrow && \downarrow q\\ x & \overset{f}\to & y\end{matrix} \right\}

    The laxator is defined by sending squares on f:xyf:x \to y and g:yzg:y \to z agreeing on their yy boundary to the obvious composite square lying over f;g:xzf;g : x \to z (thus forgetting the middle boundary). One can see this assignment is unitary, as C/1 x\mathbf{C}/1_x is exactly C/x(,=)\mathbf{C}/x(-,=) (the identity profunctor on C / x \mathbf{C}/x ).

  3. A span xlsryx \overset{l}\leftarrow s \overset{r}\to y is sent to the pull-push functor r *l *:C/xC/yr_* l^* : \mathbf{C}/x \to \mathbf{C}/y which, on a map p:axp : a \to x, acts first by pullback along ll and then post-composition it with rr:
    C/(l,r)(p)=σ rl *p \mathbf{C}/(l, r)(p) = \sigma_r l^*p
  4. On squares, it can be defined as…

References

Exposition:

Actions of double categories are central in some approaches to dependent optics?:

Created on December 12, 2022 at 21:40:03. See the history of this page for a list of all contributions to it.