\(\infty \)-Cosmoi

1.5 Change of base

“Change of base,” first considered by Eilenberg and Kelly in [ EK66 ] , refers to a systematic procedure by which enrichment over one category \({\mathord {\mathcal{V}}}\) is converted into enrichment over another category \({\mathord {\mathcal{W}}}\). This will be applied in §1.6 to convert an \(\infty \)-cosmos into a simpler structure. For a cartesian closed category \({\mathord {\mathcal{V}}}\), there is a 2-category \({{\mathord {\mathcal{V}}}}\text{-}{\mathord {\mathcal{Cat}}}\) of \({\mathord {\mathcal{V}}}\)-categories, \({\mathord {\mathcal{V}}}\)-functors, and \({\mathord {\mathcal{V}}}\)-natural transformations. The first main result, appearing as Proposition 1.5.4, gives conditions under which a functor \(T \colon {\mathord {\mathcal{V}}}\to {\mathord {\mathcal{W}}}\) between cartesian closed categories induces a change-of-base 2-functor \(T_* \colon {{\mathord {\mathcal{V}}}}\text{-}{\mathord {\mathcal{Cat}}} \to {{\mathord {\mathcal{W}}}}\text{-}{\mathord {\mathcal{Cat}}}\).

As the context we are working in here is less general than the one considered by Eilenberg and Kelly — our base categories are cartesian closed while theirs are closed symmetric monoidal — we take a shortcut which covers all of our examples and is easier to explain. In general, all that is needed to produce a change of base 2-functor is a lax monoidal functor between symmetric monoidal categories, but the lax monoidal functors we encounter between cartesian closed categories are in fact finite-product-preserving, so we content ourselves with explicating the results in that case instead.

However, lax monoidal functors exist in Mathlib already, so we briefly recall the definition.

Definition 1.5.1
#

A (lax) monoidal functor between cartesian closed categories \({\mathord {\mathcal{V}}}\) and \({\mathord {\mathcal{W}}}\) is a functor \(T \colon {\mathord {\mathcal{V}}}\to {\mathord {\mathcal{W}}}\) equipped with natural transformations

\begin{tikzcd}  \cV \times \cV \arrow[r, "T\times T"] \arrow[dr, phantom, "\scriptstyle\Downarrow\phi"] \arrow[d, "\times"'] & \cW \times \cW \arrow[d, "\times"] & \catone \arrow[r, "1"] \arrow[dr, "1"'] & \cV \arrow[d, "T"] \\ \cV \arrow[r, "T"'] & \cW  &\arrow[ur, phantom, "\scriptstyle\Uparrow\phi_0" pos=.85] & \cW
\end{tikzcd}

so that the evident associativity and unit diagrams commute.

Except in a special case that we now introduce, the maps \(\phi \) and \(\phi _0\) are to be regarded as part of the structure of a lax monoidal functor, rather than a property the functor \(T\) enjoys.

Recall that a functor \(T \colon {\mathord {\mathcal{V}}}\to {\mathord {\mathcal{W}}}\) between cartesian closed categories preserves finite products just when the natural maps defined for any \(u,v \in {\mathord {\mathcal{V}}}\)

\[ T(u \times v) \rightsquigarrow Tu \times Tv \qquad \text{and} \qquad T1 \rightsquigarrow 1 \]

are isomorphisms. These maps satisfy the duals of the coherence conditions mentioned in Definition 1.5.1 and make \(T\) into a strong monoidal functor between the cartesian closed categories \({\mathord {\mathcal{V}}}\) and \({\mathord {\mathcal{W}}}\). The inverse isomorphisms then provide the structure maps of Definition 1.5.1.

For example:

Example 1.5.2
#

Since representable functors preserve products, for any cartesian closed category \({\mathord {\mathcal{V}}}\), the underlying set functor \((-)_0 \colon {\mathord {\mathcal{V}}}\to {\mathord {\mathcal{Set}}}\) is product-preserving

Example 1.5.3
#

In a cartesian closed category \({\mathord {\mathcal{V}}}\), finite products distribute over arbitrary coproducts. In particular, for any sets \(X\) and \(Y\) there is an isomorphism

\[ \amalg _{X \times Y} 1 \cong (\amalg _X 1) \times (\amalg _Y 1) \]

between coproducts of the terminal object \(1\), which proves that the functor

\begin{tikzcd}  \mathcal{S}et \arrow[r, "{\amalg_{-} 1}"] & \cV
\end{tikzcd}

is finite-product-preserving.

A finite-product-preserving functor may be used to change the base as follows:

Proposition 1.5.4

A finite-product-preserving functor \(T \colon {\mathord {\mathcal{V}}}\to {\mathord {\mathcal{W}}}\) between cartesian closed categories induces a change-of-base 2-functor

\begin{tikzcd}  {\cV}\text{-}\mathcal{C}at \arrow[r, "T_*"] & {\cW}\text{-}\mathcal{C}at\, . \end{tikzcd}

An early observation along these lines was first stated as [ EK66 , II.6.3 ] , with the proof left to the reader. We adopt the same tactic and leave the diagram chases to the reader or to [ Cru08 , 4.2.4 ] and instead just give the construction of the change-of-base 2-functor, which is the important thing. The construction of a \({\mathord {\mathcal{W}}}\)-category \(T_*{\mathord {\mathcal{C}}}\) from a \({\mathord {\mathcal{V}}}\)-category \({\mathord {\mathcal{C}}}\) exists in Mathlib in the more general setting of a lax monoidal functor \(T\), but change of base for enriched functors or natural transformations has not been formalized.

Proof

Let \({\mathord {\mathcal{C}}}\) be a \({\mathord {\mathcal{V}}}\)-category and define a \({\mathord {\mathcal{W}}}\)-category \(T_*{\mathord {\mathcal{C}}}\) to have the same objects and to have mapping objects \(T_*{\mathord {\mathcal{C}}}(x,y) :=T{\mathord {\mathcal{C}}}(x,y)\). The composition and identity maps are given by the composites

\begin{tikzcd} [column sep=small] T\cC(y,z)\times T\cC(x,y) \arrow[r, "\cong"] & T(\cC(y,z) \times \cC(x,y)) \arrow[r, "T\circ"] & T\cC(x,z) & 1 \arrow[r, "\cong"] & T1 \arrow[r, "T\id_x"] & T\cC(x,x)
\end{tikzcd}

which make use of the inverses of the natural maps that arise when a finite-product-preserving functor is applied to a finite product. A straightforward diagram chase verifies that \(T_*{\mathord {\mathcal{C}}}\) is a \({\mathord {\mathcal{W}}}\)-category.

If \(F \colon {\mathord {\mathcal{C}}}\to {\mathord {\mathcal{D}}}\) is a \({\mathord {\mathcal{V}}}\)-functor, then we define a \({\mathord {\mathcal{W}}}\)-functor \(T_*F \colon T_*{\mathord {\mathcal{C}}}\to T_*{\mathord {\mathcal{D}}}\) to act on objects by \(c \in {\mathord {\mathcal{C}}}\mapsto Fc \in {\mathord {\mathcal{D}}}\) and with internal action on arrows defined by

\begin{tikzcd}  T\cC(x,y) \arrow[r, "TF_{x,y}"] & T\cD(Fx,Fy) \end{tikzcd}

Again, a straightforward diagram chase verifies that \(T_*F\) is \({\mathord {\mathcal{W}}}\)-functorial. It is evident from this definition that \(T_*(GF) = T_*G \cdot T_*F\).

Finally, let \(\alpha \colon F \Rightarrow G\) be a \({\mathord {\mathcal{V}}}\)-natural transformation between \({\mathord {\mathcal{V}}}\)-functors \(F,G \colon {\mathord {\mathcal{C}}}\to {\mathord {\mathcal{D}}}\) and define a \({\mathord {\mathcal{W}}}\)-natural transformation \(T_*\alpha \colon T_* F \Rightarrow T_*G\) to have components

\begin{tikzcd}  1 \arrow[r, "\cong"] & T1 \arrow[r, "T\alpha_c"] & T\cD(Fc, Gc)\end{tikzcd}

Another straightforward diagram chase verifies that \(T_*\alpha \) is \({\mathord {\mathcal{W}}}\)-natural.

It remains to verify this assignment is functorial for both horizontal and vertical composition of enriched natural transformations. The component of \(T_*(\beta \cdot \alpha )\) is defined by the top-horizontal composite below while the component of the vertical composite of \(T_*\alpha \) with \(T_*\beta \colon T_*G \Rightarrow T_*H\) is defined by the bottom composite:

\begin{tikzcd}  1 \arrow[r, "\cong"] \arrow[dr, "\cong"'] & T1 \arrow[r, "T(\beta_c\times \alpha_c)"] & T(\cD(Gc, Hc) \times \cD(Fc, Gc)) \arrow[r, "T\circ"] & T\cD(Fc,Hc) \\ & T1 \times T1 \arrow[u, "\cong"'] \arrow[r, "T\beta_c \times T\alpha_c"'] & T\cD(Gc,Hc) \times T\cD(Fc,Gc) \arrow[u, "\cong"']  \end{tikzcd}

The square commutates by the naturality of the isomorphism \(T(u \times v) \cong Tu \times Tv\), while the triangle commutes because 1 is terminal, so the inverses of the displayed isomorphisms form a commutative triangle. The argument for functoriality of horizontal composites is similar.

Remark 1.5.5
#

In fact, the “change of base” procedure \({\mathord {\mathcal{V}}}\mapsto {{\mathord {\mathcal{V}}}}\text{-}{\mathord {\mathcal{Cat}}}\) is itself a 2-functor from the 2-category of cartesian closed categories, finite-product-preserving functors, and natural transformations to the 2-category of 2-categories, 2-functors, and 2-natural transformations. See [ Cru08 , § 4.3 ] for a discussion and proof.

As an immediate consequence of the 2-functoriality of Remark 1.5.5:

Proposition 1.5.6

Any adjunction between cartesian closed categories whose left adjoint preserves finite products induces a change-of-base 2-adjunction

\begin{tikzcd} [column sep=large]
\cV \arrow[r, bend left=20, "F"] \arrow[r, phantom, "\bot"] & \cW \arrow[l, bend left=20, "U"] \arrow[r, phantom, "\rightsquigarrow"] & {\cV}\text{-}\mathcal{C}at \arrow[r, bend left=20, start anchor=10, end anchor=170,  "F_*"] \arrow[r, phantom, "\bot"] & {\cW}\text{-}\mathcal{C}at \arrow[l, bend left=20, start anchor=190, end anchor=-10,  "U_*"]
\end{tikzcd}
Proof

Of course right adjoints always preserve products, so the adjoint pair of functors \(F \dashv U\) defines an adjunction in the 2-category of cartesian closed categories and finite-product-preserving functors described in Remark 1.5.5. The 2-functor \({\mathord {\mathcal{V}}}\mapsto {{\mathord {\mathcal{V}}}}\text{-}{\mathord {\mathcal{Cat}}}\) then carries the adjunction displayed on the left to the adjunction displayed on the right.

As a special case we have a free-forgetful adjunction between \({\mathord {\mathcal{Cat}}}\) and \({{\mathord {\mathcal{V}}}}\text{-}{\mathord {\mathcal{Cat}}}\). Some pieces of this are in the enriched categories folder of Mathlib.

Corollary 1.5.7

For any cartesian closed category \({\mathord {\mathcal{V}}}\) with coproducts, the underlying category construction and free category construction define adjoint 2-functors

\begin{tikzcd} [column sep=large]
  \mathcal{C}at \arrow[r, bend left=20, hook, start anchor=10, end anchor=170] \arrow[r, phantom, "\bot"] & {\cV}\text{-}\mathcal{C}at \arrow[l, bend left=20, start anchor=190, end anchor=-10, "(-)_0"]
\end{tikzcd}

In light of Proposition 1.5.6 and results to follow, an adjunction between cartesian closed categories whose left adjoint preserves finite products provides a change-of-base adjunction. While Proposition 1.5.6 permits the change of base along either adjoint of a finite-product-preserving adjunction, the next series of results reveal that change of base along the right adjoint is somewhat better behaved.

Lemma 1.5.8

Any adjunction comprised of finite-product-preserving functors between cartesian closed categories

\begin{tikzcd} [column sep=large]
\cV \arrow[r, bend left=20, "F"] \arrow[r, phantom, "\bot"] & \cW \arrow[l, bend left=20, "U"]  \arrow[r, phantom, "\rightsquigarrow"] & \cV \arrow[r, bend left=20, start anchor=20, end anchor=170, "F"] \arrow[r, phantom, "\bot"] & U_*\cW \arrow[l, bend left=20, start anchor=190, end anchor=-15, "U"]  \end{tikzcd}

defines a \({\mathord {\mathcal{V}}}\)-enriched adjunction between the \({\mathord {\mathcal{V}}}\)-categories \({\mathord {\mathcal{V}}}\) and \(U_*{\mathord {\mathcal{W}}}\); i.e., there exists a \({\mathord {\mathcal{V}}}\)-natural isomorphism \(U{\mathord {\mathcal{W}}}(Fv,w) \cong {\mathord {\mathcal{V}}}(v,Uw)\).

Proof

The internal action \(U_{a,b} \colon U{\mathord {\mathcal{W}}}(a,b) \to {\mathord {\mathcal{V}}}(Ua,Ub)\) of the \({\mathord {\mathcal{V}}}\)-functor \(U \colon U_*{\mathord {\mathcal{W}}}\to {\mathord {\mathcal{V}}}\) is defined by the transpose of the map \(U\textup{ev}\colon U{\mathord {\mathcal{W}}}(a,b) \times Ua \to Ub\) defined by applying \(U\) to the counit of the cartesian closure adjunction of \({\mathord {\mathcal{W}}}\). The \({\mathord {\mathcal{V}}}\)-functoriality of this map follows from naturality of evaluation in a cartesian closed category.

By the \({\mathord {\mathcal{V}}}\)-functoriality of \(U \colon U_*{\mathord {\mathcal{W}}}\to {\mathord {\mathcal{V}}}\), the map

\begin{tikzcd}  U\cW(Fv,w) \arrow[r, "U_{Fv,w}"] & \cV(UFv,Uw) \arrow[r, "{- \circ \eta_v}"] & \cV(v,Uw)
\end{tikzcd}

is \({\mathord {\mathcal{V}}}\)-natural in \(w \in U_*{\mathord {\mathcal{W}}}\) for all \(v \in {\mathord {\mathcal{V}}}\). By a general result about enriching adjoints, to construct a compatible \({\mathord {\mathcal{V}}}\)-enrichment of \(F\), we need only demonstrate that this map in an isomorphism in \({\mathord {\mathcal{V}}}\).

We do this by constructing an explicit inverse, namely

\begin{tikzcd} 
\cV(v,Uw) \arrow[r, "\eta"] & UF\cV(v,Uw) \arrow[r, "U(F_{v,Uw})"] & U\cW(Fv,FUw) \arrow[r, "\epsilon_w \circ -"] & U\cW(Fv,w)
\end{tikzcd}

where the middle map is defined by applying the unenriched functor \(U\) to the action map from the \({\mathord {\mathcal{W}}}\)-functor \(F \colon F_*{\mathord {\mathcal{V}}}\to {\mathord {\mathcal{W}}}\), which is defined similarly to the \({\mathord {\mathcal{V}}}\)-functor \(U \colon U_*{\mathord {\mathcal{W}}}\to {\mathord {\mathcal{V}}}\).

The proof that these maps are inverses involves a pair of diagram chases, the first of which demonstrates that the top-right composite reduces to the left-bottom composite, which is the identity:

\begin{tikzcd} 
\cV(v,Uw) \arrow[r, "\eta"] \arrow[ddrr, "\eta_{Uw}\circ-"'] & UF\cV(v,Uw) \arrow[r, "U(F_{v,Uw})"] \arrow[dr, "UF_{v, Uw}" description] & U\cW(Fv,FUw) \arrow[r, "\epsilon_w \circ -"] \arrow[d, "U_{Fv,FUw}"] & U\cW(Fv,w) \arrow[d, "U_{Fv,w}"] \\ & & \cV(UFv,UFUw) \arrow[r, "U\epsilon_w \circ -"]  \arrow[d, "-\circ \eta_v"]& \cV(UFv,Uw) \arrow[d, "-\circ \eta_v"] \\ & & \cV(v,UFUw) \arrow[r, "U\epsilon_w\circ-"] & \cV(v,Uw)
\end{tikzcd}

The only subtle point is the commutativity of the trapezoidal region, which expresses the fact that \(\eta \colon \textup{id}_{\mathord {\mathcal{V}}}\Rightarrow UF\) is a closed natural transformation between product-preserving functors between cartesian closed categories. This region commutes because the transposed diagram does:

\begin{tikzcd}  \cV(v,Uw) \times v\arrow[d, "\eta \times \eta_v"'] \arrow[r, equals] &  \cV(v,Uw) \times v \arrow[d, "\eta"']  \arrow[r, "\ev"] & Uw \arrow[d, "\eta_{Uw}"] \\  UF\cV(v,Uw)\times UFv  \arrow[r, "\cong"] & UF(\cV(v,UW)\times v) \arrow[r, "UF\ev"] & UFUw
\end{tikzcd}

the right-hand square by naturality, and the left-hand square because any naturally transformation between product-preserving functors is automatically a monoidal natural transformation. The other diagram chase is similar.

Proposition 1.5.9

Given an adjunction between cartesian closed categories

\begin{tikzcd} [column sep=large]
\cV \arrow[r, bend left=20, "F"] \arrow[r, phantom, "\bot"] & \cW \arrow[l, bend left=20, "U"]   \end{tikzcd}

whose left adjoint preserves finite products then if \({\mathord {\mathcal{C}}}\) is co/tensored as a \({\mathord {\mathcal{W}}}\)-category, \(U_*{\mathord {\mathcal{C}}}\) is co/tensored as \({\mathord {\mathcal{V}}}\)-category with the co/tensor of \(c \in {\mathord {\mathcal{C}}}\) by \(v \in {\mathord {\mathcal{V}}}\) defined by

\[ v \otimes c :=Fv \otimes c \qquad \text{and} \qquad c^v :=c^{Fv}. \]
Proof

Suppose \({\mathord {\mathcal{C}}}\) admits cotensors as a \({\mathord {\mathcal{W}}}\)-category. To verify that \(U_*{\mathord {\mathcal{C}}}\) admits cotensors as a \({\mathord {\mathcal{V}}}\)-category we must supply an isomorphism

\[ U{\mathord {\mathcal{C}}}(x,c^{Fv}) \cong (U{\mathord {\mathcal{C}}}(x,c))^v \]

in \({\mathord {\mathcal{V}}}\) that is \({\mathord {\mathcal{V}}}\)-natural in \(x\). By the enriched Yoneda lemma, we can extract this isomorphism from an isomorphism

\[ {\mathord {\mathcal{V}}}(u,U{\mathord {\mathcal{C}}}(x,c^{Fv})) \cong {\mathord {\mathcal{V}}}(u,(U{\mathord {\mathcal{C}}}(x,c))^v) \]

that is \({\mathord {\mathcal{V}}}\)-natural in \(u \in {\mathord {\mathcal{V}}}\). To that end, by composing the \({\mathord {\mathcal{V}}}\)-natural isomorphisms of Lemma 1.5.8, the enriched natural isomorphisms arising from the cartesian closed structure on \({\mathord {\mathcal{V}}}\) and on \(U_*{\mathord {\mathcal{W}}}\), and the isomorphisms that characterize the cotensor on \({\mathord {\mathcal{C}}}\) and express the fact that \(F\) preserves binary products, we have:

\begin{align*} {\mathord {\mathcal{V}}}(u,U{\mathord {\mathcal{C}}}(x,c^{Fv})) & \cong U{\mathord {\mathcal{W}}}(Fu, {\mathord {\mathcal{C}}}(x,c^{Fv})) \cong U{\mathord {\mathcal{W}}}(Fu, {\mathord {\mathcal{C}}}(x,c)^{Fv}) \\ & \cong U{\mathord {\mathcal{W}}}(Fu \times Fv, {\mathord {\mathcal{C}}}(x,c)) \cong U{\mathord {\mathcal{W}}}(F(u \times v), {\mathord {\mathcal{C}}}(x,c)) \\ & \cong {\mathord {\mathcal{V}}}(u \times v, U{\mathord {\mathcal{C}}}(x,c)) \cong {\mathord {\mathcal{V}}}(u, (U{\mathord {\mathcal{C}}}(x,c))^v). \qedhere \end{align*}

The general theory of change-of-base will be applied in the following case the next section.

Example 1.5.10

Both adjoints of the adjunction

\begin{tikzcd} [column sep=large]
s\mathcal{S}et \arrow[r, bend left=20, start anchor=10, end anchor=170, "\ho"] \arrow[r, phantom, "\bot"] & \mathcal{C}at \arrow[l, bend left=20, start anchor=190, end anchor=-10, hook']
\end{tikzcd}

of Proposition 1.2.26 preserve finite products. Hence, Proposition 1.5.6 induces a change-of-base adjunction defined by the 2-functors

\begin{tikzcd} [column sep=large]
s\mathcal{C}at  \arrow[r, bend left=20, start anchor=7, end anchor=170, "\ho_*"] \arrow[r, phantom, "\bot"] &2\text{-}\mathcal{C}at\arrow[l, bend left=20, start anchor=190, end anchor=-5, hook']
\end{tikzcd}

that act identically on objects and act by applying the homotopy category functor or nerve functor, respectively, on homs. The right adjoint, which builds a simplicially enriched category from a 2-category, respects the underlying category: the underlying category of objects and 1-cells is identified with the underlying category of objects and 0-arrows. In this case, the functor \({\mathord {\mathsf{h}}}\colon {\mathord {\mathcal{sSet}}}\to {\mathord {\mathcal{Cat}}}\) commutes with the underlying set functors, so in fact both adjoints preserve underlying categories, as is evident from direct computation. In particular, the homotopy 2-category of an \(\infty \)-cosmos has the same underlying 1-category. Since the nerve embedding is fully faithful, 2-categories can be identified as a full subcategory comprised of those simplicial categories whose hom spaces are nerves of categories.