Proposition [efr-NZ0X]

Let \mathbb {C} be a 2-category and let C,D : \mathcal {T}_\mathsf {PsCat} \to \mathbb {C} be pseudocategories, represented as models of the theory. Then a pseudonatural transformation F: C \to D which is strict on c,d,e and the limit projections \pi ^i_j is equivalently a pseudomorphism between the pseudocategories.

Now let (M,C), (N,D) : \mathcal {T}_\mathsf {Act} \to \mathbb {C} be pseudomonoid actions. Then a pseudonatural transformation F_m, F_c which preserves the product projections strictly is equivalently a pair of a pseudomorphism F_m : M \to N and a functor F_c: C \to D which is pseudolinear with respect to the action F_m(-) \cdot = of M on D.

Proof

Both of these are essentially a matter of unwinding the definitions. Let us start with pseudocategories. The requirement that F is strict on the product projections amounts to requiring that F_{C_2} : C_2 \to D_2 is given strictly as the pullback F_1 \times _{F_0} F_1, and not merely up to 2-isomorphism. With this, \mu is just a naturality transformation for m, and \epsilon is a naturality transformation for e. Note that since every map in \mathcal {T}_\mathsf {PsCat} is induced from m, e, c,d and the pullback structure, this means the other naturality transformations are determined by \mu , \epsilon

The composite m'(1_{F_1} \times \mu ) \mu (1 \times _{C_0} m) is the naturality transformation for the map m (1 \times m), and analogously for the composite m'(\mu \times 1_{F_1})\mu (m \times _{C_0} 1). Hence the hexagon is a pseudonaturality coherence for the 2-cell \alpha . Analogously the two squares can be obtained as coherence 2-cells. Conversely, these suffice to make F a pseudonatural transformation, again since all the other 2-cells are generated by \alpha , \rho ,\lambda .

Now let us look at pseudomonoid actions. As above, such a pseudonatural transformation is determined by the functors F_m: M \to N and F_c: C \to D plus some 2-cells involving these and their products. As a special case of the above when C_0, D_0 = * we find that the restriction F_m of the pseudonatural transformation to the pseudomonoid part is equivalently a strong monoidal functor. Now the required lineator l: \cdot _D (F_m \times F_c) \to F_m(\cdot ) is a naturality square for the multiplication map \cdot \in \mathcal {T}_\mathsf {Act}. As above this determines all the other naturality transformations because all the other maps are generated from \cdot (and the pseudomonoid structure) using the product structure. Also analogously to the above argument, the coherence pentagon is a pseudonaturality coherence for the natural isomorphism \mu , and the coherence triangle for \eta .

Context

\mathsf {\mathbb Para} for a general 2-category [efr-GZH4]

We are now almost ready to prove:

Theorem [efr-I897]

Let \mathbb {C} be a 2-category which admits pullbacks, products and comma objects. Then there is a functor \mathsf {\mathbb Para}: \mathsf {Act}(\mathbb {C}) \to \mathsf {PsCat}(\mathbb {C}) from the 2-category of pseudomonoid actions and pseudolinear maps to the 2-category of pseudocategories and pseudofunctors, with \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0 = \mathcal {C} and \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 = \mathcal {M} \times \mathcal {C} \downarrow \mathcal {C}. This functor preserves strict maps, limits, and filtered colimits.

The main ingredient missing is a characterization of the respective notions of pseudomorphism in terms of the limit sketches. This we do now:

Proposition [efr-NZ0X]

Let \mathbb {C} be a 2-category and let C,D : \mathcal {T}_\mathsf {PsCat} \to \mathbb {C} be pseudocategories, represented as models of the theory. Then a pseudonatural transformation F: C \to D which is strict on c,d,e and the limit projections \pi ^i_j is equivalently a pseudomorphism between the pseudocategories.

Now let (M,C), (N,D) : \mathcal {T}_\mathsf {Act} \to \mathbb {C} be pseudomonoid actions. Then a pseudonatural transformation F_m, F_c which preserves the product projections strictly is equivalently a pair of a pseudomorphism F_m : M \to N and a functor F_c: C \to D which is pseudolinear with respect to the action F_m(-) \cdot = of M on D.

Proof

Both of these are essentially a matter of unwinding the definitions. Let us start with pseudocategories. The requirement that F is strict on the product projections amounts to requiring that F_{C_2} : C_2 \to D_2 is given strictly as the pullback F_1 \times _{F_0} F_1, and not merely up to 2-isomorphism. With this, \mu is just a naturality transformation for m, and \epsilon is a naturality transformation for e. Note that since every map in \mathcal {T}_\mathsf {PsCat} is induced from m, e, c,d and the pullback structure, this means the other naturality transformations are determined by \mu , \epsilon

The composite m'(1_{F_1} \times \mu ) \mu (1 \times _{C_0} m) is the naturality transformation for the map m (1 \times m), and analogously for the composite m'(\mu \times 1_{F_1})\mu (m \times _{C_0} 1). Hence the hexagon is a pseudonaturality coherence for the 2-cell \alpha . Analogously the two squares can be obtained as coherence 2-cells. Conversely, these suffice to make F a pseudonatural transformation, again since all the other 2-cells are generated by \alpha , \rho ,\lambda .

Now let us look at pseudomonoid actions. As above, such a pseudonatural transformation is determined by the functors F_m: M \to N and F_c: C \to D plus some 2-cells involving these and their products. As a special case of the above when C_0, D_0 = * we find that the restriction F_m of the pseudonatural transformation to the pseudomonoid part is equivalently a strong monoidal functor. Now the required lineator l: \cdot _D (F_m \times F_c) \to F_m(\cdot ) is a naturality square for the multiplication map \cdot \in \mathcal {T}_\mathsf {Act}. As above this determines all the other naturality transformations because all the other maps are generated from \cdot (and the pseudomonoid structure) using the product structure. Also analogously to the above argument, the coherence pentagon is a pseudonaturality coherence for the natural isomorphism \mu , and the coherence triangle for \eta .

Remark [efr-T667]

This characterization of the notions of pseudomorphism cannot help but seem a little ad hoc. The basic idea here seems to go back to Power in Reference [power-enriched-lawvere]. After constructing an enriched Lawvere theory (which is just a special kind of limit sketch) corresponding to any finitary enriched monad, he notes that in the \mathsf {Cat}-enriched case the pseudomorphisms of monad algebras correspond to exactly those pseudonatural transformations which preserve the products strictly.

An elegant theory which generalizes this basic idea has recently been developed by Bourke, Ko, and Varkor in Reference [varkor-bourke-ko-sketches] (as we mentioned briefly before). Their theory involves decorating the sketch with a set of tight morphisms, which the transformations must be strictly natural with respect to. Beyond developing a general theory of this (not specialized to a few examples as above,) they also show how to construct the categories of (op)lax homomorphisms, and develop a commutativity of internalization principle for their models. This could be profitably applied in our case to understand better, for example, the implied notion of monoidal triple category, but we will not pursue this here.

Proof Proof of Theorem [efr-I897] [efr-0BHI]

First recall that \mathsf {Mod}(\mathcal {T},\mathbb {C}) can be identified with the subcategory of [\mathbb {C}^\mathrm {op}, \mathsf {Mod}(\mathcal {T})] spanned by the levelwise representable presheaves. Note that for \mathcal {T} = \mathcal {T}_\mathsf {PsCat}, it suffices to verify representability for C_0,C_1 \in \mathcal {T}_\mathsf {PsCat}, since the rest are pullbacks of these, and pullbacks of representable presheaves are again representable since \mathbb {C} admits pullbacks.

Postcomposition with the previously-constructed functor \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) = \mathsf {Act}(\mathsf {Cat}) \to \mathsf {PsCat}(\mathsf {Act}) = \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) gives a functor [\mathbb {C}^\mathrm {op},\mathsf {Mod}(\mathcal {T}_\mathsf {Act})] \to [\mathbb {C}^\mathrm {op},\mathsf {Mod}(\mathcal {T}_\mathsf {PsCat})]. Clearly this functor preserves representability (again, since limits of representable functors are representable). This gives the desired functor \mathsf {Mod}_s(\mathcal {T}_\mathsf {Act}, \mathbb {C}) \to \mathsf {Mod}_s(\mathcal {T}_\mathsf {PsCat}, \mathbb {C}).

Under the identification of \mathsf {Mod}(\mathcal {T},\mathbb {C}) with a subcategory of [\mathbb {C}^\mathrm {op} \times \mathcal {T}, \mathsf {Cat}], it is clear that the pseudonatural transformations of models correspond to those pseudonatural transformations which are strict on morphisms in \mathbb {C}^\mathrm {op}. This implies the full category \mathsf {Mod}_p(\mathbb {C}) of models and pseudonatural transformations can be identified with the subcategory of [\mathbb {C}^\mathrm {op},\mathsf {Mod}_p(\mathcal {T},\mathsf {Cat})] spanned by those 2-functors which come from models---that is, A: \mathbb {C}^\mathrm {op} \to \mathsf {Mod}_p(\mathcal {T}) = \mathsf {Mod}_p(\mathcal {T},\mathsf {Cat}) must factor over \mathsf {Mod}(\mathcal {T}) \hookrightarrow \mathsf {Mod}_p(\mathcal {T}).

(To be clear: the morphisms in [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T})] are strictly natural transformations between functors \mathbb {C}^\mathrm {op} \to \mathsf {Mod}_p(\mathcal {T}), but each component A(C) \to B(C) of such a natural transformation is a pseudonatural transformation of models).

Under this identification, it is clear that pseudofunctors correspond to those natural transformations in [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T}_\mathsf {PsCat})] which are valued in pseudofunctors, and analogously for pseudolinear morphisms and maps [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T}_\mathsf {Act})]. Hence it suffices to observe that the \mathsf {Cat}-valued version \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) \to \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) carries pseudolinear maps to pseudofunctors.

Note that \mathsf {\mathbb Para}: \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) \to \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) is given objectwise as a finite limit. Moreover, since the limit sketch of pseudocategories only involved finite limits, the class of pseudocategories is stable under filtered colimits in [\mathcal {T}_\mathsf {PsCat}, \mathsf {Cat}]. Hence \mathsf {\mathbb Para} commutes with filtered colimits, and is in particular accessible. Hence it admits a left adjoint L (M,C) \mapsto \operatorname {\mathrm {Hom}}_{\mathsf {Mod}(\mathcal {T}_\mathsf {Act})(L(-), (M,C))} where L: \mathcal {T}_\mathsf {PsCat}^\mathrm {op} \to [\mathcal {T}_\mathsf {Act},\mathsf {Cat}] is the restriction of the left adjoint of \mathsf {\mathbb Para}. Both forming the hom-category \operatorname {\mathrm {Hom}}(-, (M,C)) and precomposing with L are 2-functors, and as such preserve pseudonatural transformations. Thus it only remains to observe that \mathsf {\mathbb Para} also preserves the partial strictness property, but this clear.

We have not yet given any thought to functoriality in \mathbb {C}, but passing through the constructions, it is apparent that we have:

Proposition [efr-TY4G]

If \mathbb {C} \to \mathbb {D} is a 2-functor that preserves finite 2-limits, the square

commutes up to strict natural isomorphism. (In particular, the square involving the subcategories of strict homomorphisms also commutes up to natural isomorphism).

(It may seem wrong that, after working strictly all this time, this square commutes only up to natural isomorphism, but in fact that is the strict notion---the weak version of this statement would be that it commuted up to natural equivalence. Note that eg. the comma objects M \times C \downarrow C are only characterized up to isomorphism, so this is really the best we can hope for)

The main problem with Theorem [efr-I897] is that for many 2-categorical notions of interest, requiring (for example) the action \mathcal {M} \times \mathcal {C} \to \mathcal {C} to be a strict homomorphism of whatever structure under consideration is too strict to work, while working with the full category of pseudomorphisms prevents the pullbacks required for pseudocategories from existing. Thus for example, an internal pseudomonoid in \mathsf {MonCat}_s is a commutative monoidal category, which is far too strict for most purposes---generally speaking, symmetric monoidal categories can not be strictified into commutative ones.

In § [efr-ZRUZ], we will want to construct a symmetric monoidal "triple category"---that is, a symmetric monoidal pseudocategory in strict double categories. We will manage this via the preceding by noting that since \mathsf {Act}(\mathbb {C}) \to \mathsf {PsCat}(\mathbb {C}) preserves products, it carries (symmetric) pseudomonoids to pseudomonoids---in other words, we can apply the internalization the other way around, taking pseudomonoids in actions rather than actions in pseudomonoids. This works because strict products still exist in the category of pseudohomomorphisms, but for a more general categorical structure, we would be in trouble.