Proposition [efr-002Z]

Let \mathcal {M} act on \mathcal {C}, and consider the double category \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}). Consider the underlying directed graph (internal to categories) \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 \rightrightarrows \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0. We have:

  1. \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0 = \mathcal {C}
  2. This square exhibits \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 as the comma object \mathcal {M} \times \mathcal {C} \downarrow _{\mathcal {C}} \mathcal {C}:

Proof

The first claim is a straightforward consequence of the definition.

To see the second claim, let us first look at the objects. These are exactly morphisms in the bicategory \mathsf {Para}_\mathcal {M}(\mathcal {C}), which, according to our definition, is obtained by applying the 2-Grothendieck construction to the action \mathcal {C}: B\mathcal {M} \to \mathsf {Cat}. The objects of this bicategory are therefore exactly the objects of \mathcal {C}, and a morphism X \to Y consists of an object of \mathcal {M} and a map M \cdot X \to Y. In other words, a morphism is a quadruple (X,Y,M,\phi : M \cdot X \to Y). Clearly this is exactly what an object of the comma category is.

Similarly, the morphisms of the comma category consist of triples of morphisms X \to X', Y \to Y', M \to M' making the obvious square commute. On the other hand, the morphisms of \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 are, by definition, pairs X \to X', Y \to Y' in \mathcal {C} = \mathsf {Para}_\mathcal {M}(\mathcal {C})_* and a 2-cell filling the resulting square. But, since \mathsf {Para}_\mathcal {M}(\mathcal {C}) is locally discretely fibred over B\mathcal {M}, such a 2-cell is exactly a 2-cell in B\mathcal {M}, i.e a morphism in \mathcal {M}, which is compatible with the square. After unwinding the definitions, this compatibility is equivalent to making the square considered before commute. This finishes the proof.

Context

Locally Graded Categories as Fibrations [efr-KR2F]

There is also a para construction for enriched categories (say enriched in \mathcal {M}), where a parametrized morphism is defined in the evident curried way as a map P \to \mathcal {C}(A,B) in \mathcal {M}.

The natural generalization of enrichment and actions is the notion of locally \mathcal {M} graded category.

Definition Locally graded category [efr-002I]

Let \mathcal {M} be a monoidal category. Recall that we may equip the presheaf category [\mathcal {M}^\mathrm {op}, \mathsf {Set}] with the monoidal structure of Day convolution. A locally graded \mathcal {M}-category is a category enriched in [\mathcal {M}^\mathrm {op}, \mathsf {Set}]

Equivalently, a locally graded \mathcal {M}-category consists of

  1. A collection of objects
  2. For each pair of objects X,Y and M \in \mathcal {M}, a collection of M-morphisms \mathcal {C}_M(X,Y)
  3. For each morphism M' \to M, a function \mathcal {C}_{M'}(X,Y) \to \mathcal {C}_M(X,Y)
  4. A composition operation \mathcal {C}_{M}(X,Y) \times \mathcal {C}_{M'}(Y,Z) \to \mathcal {C}_{M \otimes M'}(X,Z)
  5. For each object X, an identity morphism in \mathcal {C}_{I_\mathcal {M}}(X,X)
  6. Satisfying evident laws

Locally graded categories were introduced by Wood in Reference [locally-graded-cats], under the name large \mathcal {M}-categories. The original motivation was to consider large presheaves on \mathcal {M} and use these to describe \mathcal {M}-enriched categories with possibly large hom-objects. We have not given much thought to size issues yet---our definition above should possibly be called "locally small locally graded categories". This is sufficient for us, since they capture all the \mathcal {M}-enriched categories and the locally small \mathcal {M}-actegories (as we will see in a bit,) which is what we're after.

The notion of locally graded categories turns out to be somewhat unhelpful in defining \mathsf {Para}(-), since the locally graded category corresponding to an category with an action is (a bicategorical version of) the \mathsf {Para}-construction applied to that case. Nevertheless, this does conceptually simplify certain things.

Proposition [efr-002J]

Recall that the Yoneda embedding \mathcal {M} \hookrightarrow [\mathcal {M}^\mathrm {op},\mathsf {Set}] is strong monoidal. Hence it induces a functor from \mathcal {M}-categories to locally \mathcal {M}-graded categories, which carries \mathcal {C} to a locally graded category with \mathcal {C}_M(X,Y) = \mathcal {M}(M, \mathcal {C}(X,Y))

There is really nothing to show here. In the case of an actegory, conceptually we have the same idea---we want to define \mathcal {C}_M(X,Y) = \mathcal {C}(M \bullet X, Y)---but there is a bit more work to do to see that this comes together into a locally graded category. We begin with the following alternative description of locally graded categories:

Proposition [efr-002T]

Let \mathcal {C} be a locally \mathcal {M}-graded category. Consider the collection of categories \int _M \mathcal {C}_M(X,Y), given by taking the category of elements of the presheaf M \mapsto \mathcal {C}_M(X,Y) for each X,Y. These form the hom-categories of a bicategory \int \mathcal {C}, with a canonical pseudofunctor to the delooping B\mathcal {M}. Conversely, given a bicategory with a pseudofunctor \mathcal {D} \to B\mathcal {M} so that each functor \mathcal {D}(X,Y) \to B\mathcal {M}(*,*) = \mathcal {M} is a discrete fibration, the presheaves classifying those discrete fibrations form a locally \mathcal {M}-graded category.

Moreover, if \mathcal {C}, \mathcal {D} are two locally graded categories, a pseudofunctor \int \mathcal {C} \to \int \mathcal {D} over B\mathcal {M} which preserves Cartesian 2-cells is equivalent to an enriched functor \mathcal {C} \to \mathcal {D}

Proof

It suffices to observe that the category of elements construction is monoidal as a functor from [\mathcal {M}^\mathrm {op},\mathsf {Set}] to (\mathsf {Cat}_{/\mathcal {M}}), if the former is equipped with Day convolution and the latter is equipped with the monoidal structure given by \mathcal {A}, \mathcal {B} \mapsto (\mathcal {A} \times \mathcal {B} \to \mathcal {M} \times \mathcal {M} \xrightarrow {\otimes _\mathcal {M}} \mathcal {M}). This implies that, forgetting the projection to \mathcal {M}, we obtain a category enriched in \mathsf {Cat} with the Cartesian product, i.e a 2-category. The fact that the enrichment factors through the above monoidal structure is clearly exactly what it means for this 2-category to carry a pseudofunctor to B\mathcal {M}.

Conversely, given such a bicategory over B\mathcal {M}, this corresponds to a category weakly enriched in the subcategory of \mathsf {Cat}_{/\mathcal {M}} spanned by the discrete fibrations. But this subcategory is (equivalent to) a 1-category, so after observing that the inverse of the category of elements construction (taking fibers) must also be monoidal, we get an ordinary enriched category in [\mathcal {M}^\mathrm {op},\mathsf {Set}]

(Another way of thinking about this last point is to say that, after taking fibers, we are "weakly enriched" in a monoidal 1-category, so the coherence 2-cells implied by the "weak" in "weakly enriched" must be identities)

From here, we will abuse terminology and freely refer to a category over B\mathcal {M} which is locally a discrete fibration as a locally graded category.

The idea now is that an action of \mathcal {M} can equivalently be described as a pseudofunctor B\mathcal {M} \to \mathsf {Cat}, and taking the 2-Grothendieck construction of this (in a suitable sense) will give us the locally graded category corresponding to this action.

Proposition [efr-002O]

Let \mathcal {M} be a monoidal category. Then an action of \mathcal {M} is equivalently a pseudofunctor C: B\mathcal {M} \to \mathsf {Cat}, where C(*) is the category which this is an action on.

By a 2-fibration we will always mean a 2-fibration in a weak sense, lying over a bicategory and classifying a pseudofunctor into bicategories (although our functors will always land in 1-categories). The correct notion of weak 2-fibration was first introduced by Buckley, Reference [buckley-2-fibrations]. (Recall that bifibration means a functor which is both a fibration and an opfibration, and so we can't use this word.)

As may be expected, the work of Buckley is extremely complicated, because he treats the full generality and thus must consider the tricategory of bicategories, and the class of trifunctors into it. We only care about actions on ordinary categories, and hence can restrict ourselves to the bicategory \mathsf {Cat}.

Recall that in the ordinary Grothendieck construction, there are actually two ways to turn a functor \mathcal {C}^\mathrm {op} \to \mathsf {Cat} into a category---we can either turn it into a fibration over \mathcal {C} or an opfibration over \mathcal {C}^\mathrm {op}. In the bicategorical case, there are two independent choices---we can be either contravariant or covariant both in the 1-cells and in the 2-cells. Somewhat annoyingly, the bicategorical structure usually put on \mathsf {Para} corresponds to being covariant in the 1-cells but contravariant in the 2-cells, forcing us to deal with this sort of "mixed-variance fibration" (\mathrm {co} \mathsf {Para}, consisting instead of morphisms X \to M \bullet Y, instead has the 2-cells going in the opposite direction, so there's no help there).

Definition [efr-002U]

Let p: \mathcal {D} \to \mathcal {C} be a homomorphism of bicategories. We say p is

  1. A (-,-)-fibration if it is a weak 2-fibration in the sense of Buckley
  2. A (+,-)-fibration if the 1-cell dual \mathcal {C}^\mathrm {op} \to \mathcal {D}^\mathrm {op} is a (-,-)-fibration. Recall that \mathcal {C}^\mathrm {op}(X,Y) = \mathcal {C}^\mathrm {op}(Y,X), i.e \mathcal {C}^\mathrm {op} inverts the direction of the 1-cells but not the 2-cells.
  3. A (-,+)-fibration if the 2-cell dual \mathcal {C}^\mathrm {co} \to \mathcal {D}^\mathrm {co} is a (-,-)-fibration. Recall that \mathcal {C}^\mathrm {co}(X,Y) = \mathcal {C}(X,Y)^\mathrm {op}
  4. A (+,+)-fibration if the bidual \mathcal {C}^{\mathrm {co} \mathrm {op}} \to \mathcal {D}^{\mathrm {co} \mathrm {op}} is a (-,-)-fibration.

Note that the way these correspond to functors from the various duals of \mathcal {D} into bicategories is somewhat unintuitive! By the work of Buckley, (-,-)-fibrations classify functors \mathcal {D}^{\mathrm {co} \mathrm {op}} \to \mathsf {BiCat}. Given for example a (+,-)-fibration, it has a dual (-,-)-fibration which, of course, classifies a functor \mathcal {D}^\mathrm {co} \to \mathsf {BiCat}. But the values of this functor are not the fibers of the original functor, but the (1-cell) duals---after postcomposing with the (-)^\mathrm {op} functor \mathsf {BiCat}^\mathrm {co} \to \mathsf {BiCat}, we are left with a functor \mathcal {D} \to \mathsf {BiCat}.

Proposition [efr-002N]

There is an equivalence of bicategories between

  1. (+,-)-fibrations \mathcal {C} \to B\mathcal {M} which are locally discrete fibrations.
  2. Pseudofunctors B\mathcal {M} \to \mathsf {Cat}
  3. Actions of \mathcal {M}

Proof

The latter two are equivalent almost by definition, see eg Reference [actegories-amthematician-capucci-gavranovic].

By Definition [efr-002U], clearly pseudofunctors B\mathcal {M} \to \mathsf {Cat} are equivalent to some subcategory of the (+.-)-fibrations. But a fibration classifies a pseudofunctor into 1-categories if and only if its fibers are equivalent to 1-categories, if and only if the hom-categories of the fibers are equivalent to discrete categories. Since the hom-categories of the fibers are the fibers of \mathcal {C}(X,Y) \to B\mathcal {M}(*,*), this is true if and only if these fibrations are discrete, concluding the proof.

Hence, we have characterized both the actions of and the enrichments in \mathcal {M} as subcategories of the locally graded \mathcal {M}-categories.

Let us observe first that, as discussed above, the locally graded \mathcal {M}-category corresponding to an action or enrichment is really a bicategorical version of \mathsf {Para}

Proposition [efr-002V]

Let \mathcal {C} be enriched in \mathcal {M}. Then this corresponds to a bicategory over B\mathcal {M}. Denote it \mathsf {Para}^\mathcal {M}(\mathcal {C}). The objects are the same as \mathcal {C}, and a morphism consists of a tuple M \in \mathcal {M}, M \to \mathcal {C}(X,Y) \in \mathcal {M}.

Let \mathcal {C} carry an action of \mathcal {M}. This corresponds to a bicategory of B\mathcal {M}. Denote it \mathsf {Para}_\mathcal {M}(\mathcal {C}). The objects are the same as \mathcal {C}, and a morphism X \to Y consists of a tuple M \in \mathcal {M}, X \to M \cdot Y.

This will serve as a definition of the bicategory of parametrized maps. From this we can easily describe a double category of parametrized maps, which we will denote \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})

Proposition [efr-002X]

Let \mathcal {C} \to B\mathcal {M} be a locally graded category. Then the fiber \mathcal {C}_* over the unique object is equivalent to a 1-category. It consists of those morphisms which go to the identity in B\mathcal {M}, i.e the unit object I \in \mathcal {M}. We call such morphisms unparametrized.

Proposition [efr-002Y]

Let \mathcal {C} be a bicategory, and let \mathcal {C}_0 \to \mathcal {C} be an identity-on-objects functor from a 1-category. Then there is a pseudo double category where

  1. The objects are the objects of \mathcal {C}
  2. The vertical category is \mathcal {C}_0
  3. The horizontal category is \mathcal {C}
  4. A 2-cell is a 2-cell in \mathcal {C} filling the square

Definition [efr-002W]

Let \mathcal {M} act on \mathcal {C}. Then we denote by \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) the double category given by Proposition [efr-002Y] applied to \mathsf {Para}_\mathcal {M}(\mathcal {C})_* \hookrightarrow \mathsf {Para}_\mathcal {M}(\mathcal {C}), where \mathsf {Para}_\mathcal {M}(\mathcal {C}) is the corresponding locally graded category as in Proposition [efr-002V], and (-)_* denotes the fiber over the basepoint as in Proposition [efr-002X].

Proposition [efr-002R]

Every vertical morphism f: x \to y in \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) has a companion, given by (I, x \cdot I \cong x \to y). A horizontal morphism (P, x \cdot P \to y) has a companion if and only if P \cong I.

Note that a (pseudo) double category with singleton vertical category is equivalent to a monoidal category. Thus we can state:

Proposition [efr-002K]

Let \mathcal {C}_(-) be locally graded over \mathcal {M}. Then there is a double category where

  1. The objects are the objects of \mathcal {C}
  2. The horizontal morphisms are morphisms of \mathcal {C} (with arbitrary grading)
  3. The vertical morphisms are the I-graded morphisms of \mathcal {C}
  4. A commutative square is a map M \to M' in \mathcal {M} so that one path around the square is the base-change of the other.

There is an obvious double functor \mathsf {Para}(\mathcal {C}) \to \mathcal {M} (the latter regarded as a double category with singleton vertical category).

Proof

Recall that, in a discrete opfibration p: \mathcal {E} \to \mathcal {M}, every morphism f: x \to y is given by base-change by p(f). Hence our definition of commutative square simply corresponds to a morphism in the bicategory describing \mathcal {C}.

So the proposition follows from the general statement that, given a discrete subcategory of a

Explicitly, for monoidal actions, we have:

Definition [efr-002M]

Let \mathcal {M} be a monoidal category acting on \mathcal {C}. Then \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}) is a pseudo double category where

  1. The objects are the objects of \mathcal {C}
  2. The vertical category is \mathcal {C}
  3. The horizontal morphisms X \to Y are tuples (P \in \mathcal {M}, P \cdot X \to Y)
  4. A 2-cell from (P,f): X \to Y to (P',f'): X' \to Y' with vertical boundary g: X \to X', h: Y \to Y' is a map P \to P' \in \mathcal {M} making the obvious diagram in \mathcal {C} commute.
  5. The vertical composition of 2-cells in merely composition in \mathcal {M}. The horizontal composition is given by tensoring objects and morphisms.

Proposition [efr-002L]

Let \mathcal {C}_(-) be a locally graded category given by an action \mathcal {M} \times \mathcal {C} \to \mathcal {C}. Then the category of horizontal morphisms \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 is given by the comma object of this cospan:

Proposition [efr-002Z]

Let \mathcal {M} act on \mathcal {C}, and consider the double category \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C}). Consider the underlying directed graph (internal to categories) \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 \rightrightarrows \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0. We have:

  1. \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0 = \mathcal {C}
  2. This square exhibits \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 as the comma object \mathcal {M} \times \mathcal {C} \downarrow _{\mathcal {C}} \mathcal {C}:

Proof

The first claim is a straightforward consequence of the definition.

To see the second claim, let us first look at the objects. These are exactly morphisms in the bicategory \mathsf {Para}_\mathcal {M}(\mathcal {C}), which, according to our definition, is obtained by applying the 2-Grothendieck construction to the action \mathcal {C}: B\mathcal {M} \to \mathsf {Cat}. The objects of this bicategory are therefore exactly the objects of \mathcal {C}, and a morphism X \to Y consists of an object of \mathcal {M} and a map M \cdot X \to Y. In other words, a morphism is a quadruple (X,Y,M,\phi : M \cdot X \to Y). Clearly this is exactly what an object of the comma category is.

Similarly, the morphisms of the comma category consist of triples of morphisms X \to X', Y \to Y', M \to M' making the obvious square commute. On the other hand, the morphisms of \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 are, by definition, pairs X \to X', Y \to Y' in \mathcal {C} = \mathsf {Para}_\mathcal {M}(\mathcal {C})_* and a 2-cell filling the resulting square. But, since \mathsf {Para}_\mathcal {M}(\mathcal {C}) is locally discretely fibred over B\mathcal {M}, such a 2-cell is exactly a 2-cell in B\mathcal {M}, i.e a morphism in \mathcal {M}, which is compatible with the square. After unwinding the definitions, this compatibility is equivalent to making the square considered before commute. This finishes the proof.

We will see that the \mathsf {Para} construction preserves pseudo-limits, which will allow us build a triple category where one of the directions is parametrized maps, by applying the \mathsf {Para} construction levelwise to a double category internal to actions.