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.
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
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}}}\)
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:
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
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
between coproducts of the terminal object \(1\), which proves that the functor
is finite-product-preserving.
A finite-product-preserving functor may be used to change the base as follows:
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
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.
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
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
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
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:
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.
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:
Any adjunction between cartesian closed categories whose left adjoint preserves finite products induces a change-of-base 2-adjunction
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.
For any cartesian closed category \({\mathord {\mathcal{V}}}\) with coproducts, the underlying category construction and free category construction define adjoint 2-functors
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.
Any adjunction comprised of finite-product-preserving functors between cartesian closed categories
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)\).
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
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
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:
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:
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.
Given an adjunction between cartesian closed categories
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
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
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
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:
The general theory of change-of-base will be applied in the following case the next section.
Both adjoints of the adjunction
of Proposition 1.2.26 preserve finite products. Hence, Proposition 1.5.6 induces a change-of-base adjunction defined by the 2-functors
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.