diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 4a5735e..54fdc2d 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -6,21 +6,22 @@ % the current file can be a simple sequence of \input. Otherwise It % can start with a \section or \chapter for instance. +\chapter{\texorpdfstring{$\infty$}{Infinity}-Cosmoi} + \section{Overview} -Following \cite{RiehlVerity:2022eo}, from which this document was excerpted, we aim to develop the basic theory of $\infty$-categories in a model independent fashion using a common axiomatic framework that is satisfied by a variety of models. In contrast with prior ``analytic'' treatments of the theory of $\infty$-categories {\textendash} in which the central categorical notions are defined in reference to the coordinates of a particular model {\textendash} our approach is ``synthetic,'' proceeding from definitions that can be interpreted simultaneously in many models to which our proofs then apply. +Following \cite{RiehlVerity:2022eo}, from which this document was excerpted, we aim to develop the basic theory of $\infty$-categories in a model independent fashion using a common axiomatic framework that is satisfied by a variety of models. In contrast with prior ``analytic'' treatments of the theory of $\infty$-categories --- in which the central categorical notions are defined in reference to the coordinates of a particular model --- our approach is ``synthetic,'' proceeding from definitions that can be interpreted simultaneously in many models to which our proofs then apply. To achieve this, our strategy is not to axiomatize what infinite-dimensional categories \emph{are}, but rather to axiomatize the categorical ``universe'' in which they \emph{live}. This motivates the notion of an $\infty$-\emph{cosmos}, which axiomatizes the universe in which $\infty$-categories live as objects.\footnote{Metaphorical allusions aside, our $\infty$-cosmoi resemble the fibrational cosmoi of Street \cite{Street:1974ec}.} So that theorem statement about $\infty$-cosmoi suggest their natural interpretation, we recast $\infty$-\emph{category} as a technical term, to mean an object in some (typically fixed) $\infty$-cosmos. Several common models of $(\infty,1)$-cat\-e\-go\-ries\footnote{Quasi-categories, complete Segal spaces, Segal categories, and 1-complicial sets (naturally marked quasi-categories) all define the \texorpdfstring{$\infty$}{infinity}-categories in an \texorpdfstring{$\infty$}{infinity}-cosmos.} are $\infty$-categories in this sense, but our $\infty$-categories also include certain models of $(\infty,n)$-categories\footnote{$n$-quasi-categories, $\Theta_n$-spaces, iterated complete Segal spaces, and $n$-complicial sets also define the \texorpdfstring{$\infty$}{infinity}-categories in an \texorpdfstring{$\infty$}{infinity}-cosmos, as do saturated (n\'{e}e weak) complicial sets, a model for \texorpdfstring{$(\infty,\infty)$}{(infinity,infinity)}-categories.} as well as fibered versions of all of the above. Thus each of these objects are $\infty$-cat\-e\-go\-ries in our sense and our theorems apply to all of them.\footnote{There is a sense, however, in which many of our definitions are optimized for those \texorpdfstring{$\infty$}{infinity}-cosmoi whose objects are \texorpdfstring{$(\infty,1)$}{(infinity,1)}-categories. A good illustration is provided by the notion of \emph{discrete \texorpdfstring{$\infty$}{infinity}-category}. % introduced in Definition \ref{defn:discrete}. In the \texorpdfstring{$\infty$}{infinity}-cosmoi of \texorpdfstring{$(\infty,1)$}{(infinity,1)}-categories, the discrete \texorpdfstring{$\infty$}{infinity}-categories are the \texorpdfstring{$\infty$}{infinity}-groupoids, but this is not true for the \texorpdfstring{$\infty$}{infinity}-cosmoi of \texorpdfstring{$(\infty,n)$}{(infinity,n)}-categories.} This usage of the term ``$\infty$-categories'' is meant to interpolate between the classical one, which refers to any variety of weak infinite-dimensional categories, and the common one, which is often taken to mean quasi-categories or complete Segal spaces. - Much of the development of the theory of $\infty$-categories takes place not in the full $\infty$-cosmos but in a quotient that we call the \emph{homotopy 2-category}, the name chosen because an $\infty$-cosmos is something like a category of fibrant objects in an enriched model category and the homotopy 2-category is then a categorification of its homotopy category. The homotopy 2-category is a strict 2-category {\textendash} like the 2-category of categories, functors, and natural transformations\footnote{In fact this is another special case: there is an \texorpdfstring{$\infty$}{infinity}-cosmos whose objects are ordinary categories and its homotopy 2-category is the usual category of categories, functors, and natural transformations. This 2-category is as old as category theory itself, introduced in Eilenberg and Mac Lane's foundational paper \cite{EilenbergMaclane:1945gt}.} {\textendash} and in this way the foundational proofs in the theory of $\infty$-categories closely resemble the classical foundations of ordinary category theory except that the universal properties they characterize, e.g., when a functor between $\infty$-categories defines a cartesian fibration, are slightly weaker than in the familiar case of strict 1-categories. + Much of the development of the theory of $\infty$-categories takes place not in the full $\infty$-cosmos but in a quotient that we call the \emph{homotopy 2-category}, the name chosen because an $\infty$-cosmos is something like a category of fibrant objects in an enriched model category and the homotopy 2-category is then a categorification of its homotopy category. The homotopy 2-category is a strict 2-category --- like the 2-category of categories, functors, and natural transformations\footnote{In fact this is another special case: there is an \texorpdfstring{$\infty$}{infinity}-cosmos whose objects are ordinary categories and its homotopy 2-category is the usual category of categories, functors, and natural transformations. This 2-category is as old as category theory itself, introduced in Eilenberg and Mac Lane's foundational paper \cite{EilenbergMaclane:1945gt}.} --- and in this way the foundational proofs in the theory of $\infty$-categories closely resemble the classical foundations of ordinary category theory except that the universal properties they characterize, e.g., when a functor between $\infty$-categories defines a cartesian fibration, are slightly weaker than in the familiar case of strict 1-categories. There are many alternate choices we could have made in selecting the axioms of an $\infty$-cosmos. One of our guiding principles, admittedly somewhat contrary to the setting of homotopical higher category theory, was to allow us to work as strictly as possible, with the aim of shortening and simplifying proofs. As a consequence of these choices, the $\infty$-categories in an $\infty$-cosmos and the functors and natural transformations between them assemble into a 2-category rather than a bicategory. To help us achieve this counterintuitive strictness, each $\infty$-cosmos comes with a specified class of maps between $\infty$-categories called \emph{isofibrations}. The isofibrations have no homotopy-theoretic meaning, as any functor between $\infty$-categories is equivalent to an isofibration with the same codomain. However, isofibrations permit us to consider strictly commutative diagrams between $\infty$-cat\-e\-go\-ries and allow us to require that the limits of such diagrams satisfy a universal property up to simplicially enriched isomorphism. Neither feature is essential for the development of $\infty$-category theory. Similar proofs carry through to a weaker setting, at the cost of more time spent considering coherence of higher cells. An $\infty$-cosmos is a particular sort of \emph{simplicially enriched category} with certain \emph{simplicially enriched limits}. While the notion of simplicially enriched category currently exists in Mathlib, simplicially enriched limits do not, so in \S\ref{sec:enriched-limits} we first introduce the prerequisite notions of simplicially enriched limits that will be required to state the definition of an $\infty$-cosmos in \S\ref{sec:cosmos}. - \subsection*{Acknowledgments} The authors of this blueprint are particularly indebted to: \begin{itemize} @@ -29,6 +30,266 @@ \section{Overview} \item Pietro Monticone, who created a template for blueprint-driven formalization projects in Lean, from which this repository was forked. \end{itemize} +\section{Simplicial sets}\label{sec:simplicial-sets} + +Before introducing an axiomatic framework that allows us to develop $\infty$-cat\-e\-gory theory in general, we first consider one model in particular: \emph{quasi-cat\-e\-go\-ries}, which were introduced in 1973 by Boardman and Vogt \cite{BoardmanVogt:1973hi} in their study of homotopy coherent diagrams. Ordinary 1-categories give examples of quasi-categories via the construction of Definition \ref{defn:nerve}. Joyal first undertook the task of extending 1-category theory to quasi-category theory in \cite{Joyal:2002qk} and \cite{Joyal:2008tq} and in several unpublished draft book manuscripts. The majority of the results in this section are due to him. + + +\begin{ntn}[the simplex category]\label{ntn:simplex-cat} Let $\Del$ denote the \textbf{simplex category} of finite nonempty ordinals $[n] = \{0 <1 <\cdots < n\}$ and order-preserving maps. These include in particular the +\[ +\begin{tikzcd}[row sep=tiny, column sep=small] +\text{elementary~face~operators} & {[n-1]} \arrow[r, tail, "{\face^i}"] & {[n]} & {0 \leq i \leq n} \\ +\text{elementary~degeneracy~operators} & {[n+1]} \arrow[r, two heads, "{\degen^i}"] & {[n]} & {0 \leq i \leq n } +\end{tikzcd} +\] +whose images, respectively, omit and double up on the element $i \in [n]$. Every morphism in $\Del$ factors uniquely as an epimorphism followed by a monomorphism; these epimorphisms, the \textbf{degeneracy operators}, decompose as composites of elementary degeneracy operators, while the monomorphisms, the \textbf{face operators}, decompose as composites of elementary face operators. + +The category of \textbf{simplicial sets} is the category $\sSet \coloneq \Set^{\Del\op}$ of pre\-sheaves on the simplex category. We write $\Delta[n]$ for the \textbf{standard $n$-simplex} the simplicial set represented by $[n] \in \Del$, and $\Lambda^k[n]\subset\partial\Delta[n] \subset \Delta[n]$ for its $k$-\textbf{horn} and \textbf{boundary sphere}, respectively. The sphere $\partial\Delta[n]$ is the simplicial subset generated by the codimension-one faces of the $n$-simplex, while the horn $\Lambda^k[n]$ is the further simplicial subset that omits the face opposite the vertex $k$. + +Given a simplicial set $X$, it is conventional to write $X_n$ for the set of $n$-\textbf{sim\-plices}, defined by evaluating at $[n] \in \Del$. By the Yoneda lemma, each $n$-simplex $x \in X_n$ corresponds to a map of simplicial sets $x \colon \Delta[n] \to X$. Accordingly, we write $x \cdot \face^i$ for the $i$th face of the $n$-simplex, an $(n-1)$-simplex classified by the composite map +\[ +\begin{tikzcd} +\Delta[n-1] \arrow[r, "\face^i"] & \Delta[n] \arrow[r, "x"] & X. +\end{tikzcd} +\] The right action of the face operator defines a map $X_n \xrightarrow{\cdot\face^i} X_{n-1}$. Geometrically, $x\cdot \face^i$ is the ``face opposite the vertex $i$'' in the $n$-simplex $x$. +\end{ntn} + +The category of simplicial sets, as a presheaf category, is very well-behaved: it is cartesian closed and has all small limits and colimits. Instances of these facts currently appear in Mathlib. The definition of a quasi-category can be found there as well. + +\begin{defn}[quasi-category]\label{defn:quasi-category} A \textbf{quasi-category} is a simplicial set $A$ in which any \textbf{inner horn} can be extended to a simplex, solving the displayed lifting problem: + \begin{equation}\label{eq:qcat-defn} + \begin{tikzcd} + \Lambda^k[n] \arrow[r] \arrow[d, hook] & A \\ \Delta[n] \arrow[ur, dashed] + \end{tikzcd} \qquad \text{for}\ \ n \geq 2,\ 0 < k < n. + \end{equation} + \end{defn} + + Quasi-categories were first introduced by Boardman and Vogt \cite{BoardmanVogt:1973hi} under the name ``weak Kan complexes,'' a \textbf{Kan complex} being a simplicial set admitting extensions as in \eqref{eq:qcat-defn} along all horn inclusions $n \geq 1, 0 \leq k \leq n$. Since any topological space can be encoded as a Kan complex,\footnote{The total singular complex construction defines a functor from topological spaces to simplicial sets that is an equivalence on their respective homotopy categories --- weak homotopy types of spaces correspond to homotopy equivalence classes of Kan complexes \cite[\S II.2]{Quillen:1967ha}. The left adjoint %constructed by Exercise \ref{exc:nerve-constructions} + ``geometrically realizes'' a simplicial set as a topological space.} + in this way spaces provide examples of quasi-categories. + + Categories also provide examples of quasi-categories via the nerve construction. + + \begin{defn}[nerve]\label{defn:nerve} The category $\Cat$ of 1-categories embeds fully faithfully into the category of simplicial sets via the \textbf{nerve} functor. An $n$-simplex in the nerve of a 1-category $C$ is a sequence of $n$ composable arrows in $C$, or equally a functor $\Bbbn +\catone \to C$ from the ordinal category $\Bbbn +\catone \coloneq [n]$ with objects $0,\ldots, n$ and a unique arrow $i \to j$ just when $i \leq j$. + \end{defn} + + The map $[n] \mapsto \Bbbn +\catone$ defines a fully faithful embedding $\Del\inc\Cat$. From this point of view, the nerve functor can be described as a ``restricted Yoneda embedding'' which carries a category $C$ to the restriction of the representable functor $\hom(-,C)$ to the image of this inclusion. This is an instance of a more general family of ``nerve-type constructions.'' %are described in Exercise \ref{exc:nerve-constructions}. + + \begin{rmk}\label{rmk:nerve-2-coskeletal} + The nerve of a category $C$ is \textbf{2-coskeletal} as a simplicial set, meaning that every sphere $\partial\Delta[n] \to C$ with $n \geq 3$ is filled uniquely by an $n$-simplex in $C$, or equivalently that the nerve is canonically isomorphic to the right Kan extension of its restriction to 2-truncated simplicial sets.\footnote{The equivalence between these two perspectives is non-obvious and makes use of Reedy category theory (see \cite[\S C.4-5]{RiehlVerity:2022eo}), which does not currently exist in Mathlib.}% (see Definition \ref{defn:sk-cosk}). + Note a sphere $\partial\Delta[2] \to C$ extends to a 2-simplex if and only if that arrow along its diagonal edge is the composite of the arrows along the edges in the inner horn $\Lambda^1[2] \subset \partial\Delta[2] \to C$. The simplices in dimension 3 and above witness the associativity of the composition of the path of composable arrows found along their \textbf{spine}, the 1-skeletal simplicial subset formed by the edges connecting adjacent vertices. In fact, as suggested by the proof of Proposition \ref{prop:nerve-qcat}, any simplicial set in which inner horns admit \emph{unique} fillers is isomorphic to the nerve of a 1-category.% (see Exercise \ref{exc:nerve-characterization}). + \end{rmk} + + We decline to introduce explicit notation for the nerve functor, preferring instead to identify 1-categories with their nerves. As we shall discover the theory of 1-categories extends to $\infty$-categories modeled as quasi-categories in such a way that the restriction of each $\infty$-categorical concept along the nerve embedding recovers the corresponding 1-categorical concept. For instance, the standard simplex $\Delta[n]$ is isomorphic to the nerve of the ordinal category $\Bbbn +1$, and we frequently adopt the latter notation --- writing $\catone \coloneq \Delta[0]$, $\cattwo \coloneq \Delta[1]$, $\catthree \coloneq \Delta[2]$, and so on --- to suggest the correct categorical intuition. + + To begin down this path, we must first verify the implicit assertion that has just been made. A proof of the following result will appear in Mathlib soon. + + \begin{prop}[nerves are quasi-categories]\label{prop:nerve-qcat} Nerves of categories are quasi-categories. + \end{prop} + \begin{proof} + Via the isomorphism $C \cong \cosk_2C$ from Remark \ref{rmk:nerve-2-coskeletal} and the associated adjunction $\sk_2 \dashv \cosk_2$ of, %\ref{defn:sk-cosk}, + the required lifting problem displayed below-left transposes to the one displayed below-right: + \[ + \begin{tikzcd} + \Lambda^k[n] \arrow[d, hook] \arrow[r] & C \cong \cosk_2C & \arrow[d, phantom, "\leftrightsquigarrow"] & \sk_2\Lambda^k[n] \arrow[r] \arrow[d, hook] & C \\ \Delta[n] \arrow[ur, dashed] & & ~ & \sk_2\Delta[n] \arrow[ur, dashed] + \end{tikzcd} + \] + The functor $\sk_2$ replaces a simplicial set by its \textbf{2-skeleton}, the simplicial subset generated by the simplices of dimension at most two. For $n \geq 4$, the inclusion $\sk_2\Lambda^k[n]\inc\sk_2\Delta[n]$ is an isomorphism, in which case the lifting problems on the right admit (unique) solutions. So it remains only to solve the lifting problems on the left in the cases $n=2$ and $n=3$. + + To that end consider + \[ + \begin{tikzcd} + \Lambda^1[2] \arrow[r] \arrow[d, hook] & C & \Lambda^1[3] \arrow[d, hook] \arrow[r] & C & \Lambda^2[3] \arrow[r] \arrow[d, hook] & C \\ \Delta[2] \arrow[ur, dashed] & & \Delta[3] \arrow[ur, dashed] & & \Delta[3] \arrow[ur, dashed] + \end{tikzcd} + \] + An inner horn $\Lambda^1[2] \to C$ defines a composable pair of arrows in $C$; an extension to a 2-simplex exists precisely because any composable pair of arrows admits a (unique) composite. + + An inner horn $\Lambda^1[3] \to C$ specifies the data of three composable arrows in $C$, as displayed in the following diagram, together with the composites $gf$, $hg$, and $(hg)f$. + \[ + \begin{tikzcd} + & c_1\arrow[dr, "hg"] \\ c_0 \arrow[ur, "f"] \arrow[dr, "gf"'] \arrow[rr, "(hg)f" near end] & & c_3 \\ & c_2 \arrow[ur, "h"'] \arrow[from=uu, crossing over, "g"' near end] + \end{tikzcd} + \] + Because composition is associative, the arrow $(hg)f$ is also the composite of $gf$ followed by $h$, which proves that the 2-simplex opposite the vertex $c_1$ is present in $C$; by 2-coskeletality, the 3-simplex filling this boundary sphere is also present in $C$. The filler for a horn $\Lambda^2[3] \to C$ is constructed similarly. + \end{proof} + + We now turn to the homotopy category functor. The following definitions and results are not currently in Mathlib but will appear there soon. + + \begin{defn}[homotopy relation on 1-simplices] + A parallel pair of 1-sim\-plices $f,g$ in a simplicial set $X$ are \textbf{homotopic} if there exists a 2-simplex whose boundary takes either of the following forms\footnote{The symbol ``$\!\!\!\!\!\begin{tikzcd}[ampersand replacement=\&, sep=small] ~\arrow[r, equals] \& ~ \end{tikzcd}\!\!\!\!\!$'' is used in diagrams to denote a degenerate simplex or an identity arrow.} + \begin{equation}\label{eq:1-simp-htpy} + \begin{tikzcd}[row sep=small, column sep=small] + & y \arrow[dr, equals] & && & x \arrow[dr, "f"] \\ x \arrow[ur, "f"] \arrow[rr, "g"'] & & y & & x \arrow[ur, equals] \arrow[rr, "g"'] & & y + \end{tikzcd} + \end{equation} + or if $f$ and $g$ are in the same equivalence class generated by this relation. + \end{defn} + + In a quasi-category, the relation witnessed by either of the types of 2-simplex on display in \eqref{eq:1-simp-htpy} is an equivalence relation and these equivalence relations coincide. + + \begin{lem}[homotopic 1-simplices in a quasi-category]\label{lem:1-simp-htpy} Parallel 1-sim\-plices $f$ and $g$ in a quasi-category are homotopic if and only if there exists a 2-simplex of any or equivalently all of the forms displayed in \eqref{eq:1-simp-htpy}. + \end{lem} + % \begin{proof} + % Exercise \ref{exc:1-simp-htpy}. + % \end{proof} + + \begin{defn}[{the homotopy category \cite[\S2.4]{GabrielZisman:1967cf}}]\label{defn:homotopy-cat} + By 1-truncating, any simplicial set $X$ has an underlying reflexive directed graph with the 0-simplices of $X$ defining the objects and the 1-simplices defining the arrows: + \[ + \begin{tikzcd} + X_1 \arrow[r, shift left=.75em, "\cdot\face^1"] \arrow[r, shift right=.75em, "\cdot\face^0"'] & X_0, \arrow[l, "\cdot\degen^0" description] + \end{tikzcd} + \] + By convention, the source of an arrow $f \in X_1$ is its 0th face $f \cdot \face^1$ (the face opposite 1) while the target is its 1st face $f \cdot \face^0$ (the face opposite 0). The \textbf{free category} on this reflexive directed graph has $X_0$ as its object set, degenerate 1-simplices serving as identity morphisms, and nonidentity morphisms defined to be finite directed paths of nondegenerate 1-simplices. The \textbf{homotopy category} $\ho{X}$ of $X$ is the quotient of the free category on its underlying reflexive directed graph by the congruence\footnote{A binary relation $\sim$ on parallel arrows of a 1-category is a \textbf{congruence} if it is an equivalence relation that is closed under pre- and post-composition: if $f \sim g$ then $hfk \sim hgk$.} generated by imposing a composition relation $h = g \circ f$ witnessed by 2-simplices + \[ + \begin{tikzcd}[row sep=small, column sep=small] + & x_1 \arrow[dr, "g"] \\ x_0 \arrow[ur, "f"] \arrow[rr, "h"'] & & x_2 + \end{tikzcd} + \] + This relation implies in particular that homotopic 1-simplices represent the same arrow in the homotopy category. + \end{defn} + + The homotopy category of the nerve of a 1-category is isomorphic to the original category, as the 2-simplices in the nerve witness all of the composition relations satisfied by the arrows in the underlying reflexive directed graph. Indeed, the natural isomorphism $\ho{C} \cong C$ forms the counit of an adjunction, embedding $\Cat$ as a reflective subcategory of $\sSet$. + + \begin{prop}\label{prop:ho-nerve-adjunction} The nerve embedding admits a left adjoint, namely the functor which sends a simplicial set to its homotopy category: + \[ + \begin{tikzcd}[column sep=huge] + \Cat \arrow[r, start anchor=353, end anchor=190, bend right, hook'] \arrow[r, phantom, "\bot"] & \sSet \arrow[l, start anchor=170, end anchor=7, bend right, "\ho"' pos=.48] + \end{tikzcd} + \] + \end{prop} + + The adjunction of Proposition \ref{prop:ho-nerve-adjunction} exists for formal reasons, via results which have already been formalized in Mathlib, %(see Exercise \ref{exc:nerve-constructions}), + once the category $\Cat$ is known to be cocomplete. A proof of this fact does not currently exist in Mathlib, however, and in fact the adjunction between the homotopy category and the nerve can be used to construct colimits of categories, as it embeds $\Cat$ as a reflective subcategory of a cocomplete category (see \cite[4.5.16]{Riehl:2016cc}). Thus, the approach that is currently being formalized instead gives a direct proof. + + \begin{proof} + For any simplicial set $X$, there is a natural map from $X$ to the nerve of its homotopy category $\ho{X}$; since nerves are 2-coskeletal, it suffices to define the map $\sk_2X \to \ho{X}$, and this is given immediately by the construction of Definition \ref{defn:homotopy-cat}. Note that the quotient map $X \to \ho{X}$ becomes an isomorphism upon applying the homotopy category functor and is already an isomorphism whenever $X$ is the nerve of a category. Thus the adjointness follows %from Lemma \ref{lem:RARI-construction} or + by direct verification of the triangle equalities. + \end{proof} + + The homotopy category of a quasi-category admits a simplified description. + + \begin{lem}[the homotopy category of a quasi-category]\label{lem:htpy-cat-of-qcat} If $A$ is a quasi-category then its \textbf{homotopy category} $\ho{A}$ has + \begin{itemize} + \item the set of 0-simplices $A_0$ as its objects + \item the set of homotopy classes of 1-simplices $A_1$ as its arrows + \item the identity arrow at $a \in A_0$ represented by the degenerate 1-simplex $a \cdot \degen^0 \in A_1$ + \item a composition relation $h = g \circ f$ in $\ho{A}$ between the homotopy classes of arrows represented by any given 1-simplices $f,g,h \in A_1$ if and only if there exists a 2-simplex with boundary + \[ + \begin{tikzcd}[row sep=small, column sep=small] + & a_1 \arrow[dr, "g"] \\ a_0 \arrow[ur, "f"] \arrow[rr, "h"'] & & a_2 + \end{tikzcd} + \] + \end{itemize} + \end{lem} + % \begin{proof} + % Exercise \ref{exc:htpy-cat-of-qcat}. + % \end{proof} + + \begin{defn}[isomorphism in a quasi-category]\label{defn:isomorphism} A 1-simplex in a quasi-category is an \textbf{isomorphism}\footnote{Joyal refers to these maps as ``isomorphisms'' while Lurie refers to them as ``equivalences.'' We prefer, wherever possible, to use the same term for $\infty$-categorical concepts as for the analogous 1-categorical ones.} just when it represents an isomorphism in the homotopy category. By Lemma \ref{lem:htpy-cat-of-qcat} this means that $f \colon a \to b$ is an isomorphism if and only if there exists a 1-simplex $f^{-1} \colon b \to a$ together with a pair of 2-simplices + \[ + \begin{tikzcd}[row sep=small, column sep=small] + & b \arrow[dr, "f^{-1}", dashed] & & & & a \arrow[dr, "f"] \\ a \arrow[ur, "f"] \arrow[rr, equals] & & a & & b \arrow[ur, "f^{-1}", dashed] \arrow[rr, equals] & & b + \end{tikzcd} + \] + \end{defn} + + The properties of the isomorphisms in a quasi-category are somewhat technical to prove and will likely be a pain to formalize (see \cite[\S D]{RiehlVerity:2022eo}). Here we focus on a few essential results, which are more easily obtainable. + + %most easily proved by arguing in a closely related category where simplicial sets have the additional structure of a ``marking'' on a specified subset of the 1-simplices; maps of these so-called \emph{marked simplicial sets} must then preserve the markings (see Definition \ref{defn:marked-sset}). For instance, each quasi-category has a \emph{natural marking}, where the marked 1-simplices are exactly the isomorphisms (see Definition \ref{defn:natural-marking}). Since the property of being an isomorphism in a quasi-category is witnessed by the presence of 2-simplices with a particular boundary, every map between quasi-categories preserves isomorphisms, inducing a map of the corresponding naturally marked quasi-categories. Because marked simplicial sets seldom appear outside of the proofs of certain combinatorial lemmas about the isomorphisms in quasi-categories, we save the details for Appendix \ref{app:sset}. + +% Let us now motivate the first of several results proven using marked techniques. A quasi-category $A$ is defined to have extensions along all \emph{inner horns}. But when the initial or final edges, respectively, of an outer horn +% $\Lambda^0[2] \to A$ or $\Lambda^2[2] \to A$ map to isomorphisms in $A$, then a filler + % \[ +% \begin{tikzcd}[row sep=small, column sep=small] +% & a_1 \arrow[dr, dashed, "hf^{-1}"] & & & & a_1 \arrow[dr, "g", "\simeq"'] \\ a_0 \arrow[ur, "f", "\simeq"'] \arrow[rr, "h"'] & & a_2 & & a_0 \arrow[ur, dashed, "g^{-1}h"] \arrow[rr, "h"'] & & a_2 + % \end{tikzcd} + % \] + % should intuitively exist. The higher-dimensional ``special outer horns'' behave similarly: + + +% \begin{prop}[special outer horn filling]\label{prop:special-outer-horn} +% Any quasi-category $A$ admits fillers for those outer horns +% \[ +% \begin{tikzcd} +% \Lambda^0[n] \arrow[d, hook] \arrow[r, "g"] & A & & \Lambda^n[n] \arrow[d, hook] \arrow[r, "h"] & A \\ \Delta[n] \arrow[ur, dashed] & & & \Delta[n] \arrow[ur, dashed] +% \end{tikzcd} \qquad \text{for}\ \ n \geq 1 +% \] +% in which the edges $g\vert_{\fbv{0,1}}$ and $h\vert_{\fbv{n-1,n}}$ are isomorphisms.\footnote{In the case $n=1$, no condition is needed on the horns; degenerate 1-simplices define the required lifts.} +% \end{prop} + + % The proof of Proposition \ref{prop:special-outer-horn} requires clever combinatorics, due to Joyal, and is deferred to Proposition \ref{prop:special-outer-horn-filling}. Here, we enjoy its myriad consequences. Immediately: + + % \begin{cor}\label{cor:qcat-is-kan} A quasi-category is a Kan complex if and only if its homotopy category is a groupoid. + % \end{cor} + % \begin{proof} + % If the homotopy category of a quasi-category is a groupoid, then all of its 1-simplices are isomorphisms, and Proposition \ref{prop:special-outer-horn} then implies that all inner and outer horns have fillers. Thus, the quasi-category is a Kan complex. Conversely, in a Kan complex, all outer horns can be filled and in particular fillers for the horns displayed in Definition \ref{defn:isomorphism} can be used to construct left and right inverses for any 1-simplex, which can be rectified to a single two-sided inverse by Lemma \ref{lem:htpy-cat-of-qcat}. + % \end{proof} + + % A quasi-category contains $A$ a canonical \textbf{maximal sub Kan complex}$\coreop{A}$, the simplicial subset spanned by those 1-simplices that are isomorphisms. + + Just as the arrows in a quasi-category $A$ are represented by simplicial maps $ \cattwo \to A$ whose domain is the nerve of the free-living arrow, the isomorphisms in a quasi-category can be represented by diagrams $\iso \to A$ whose domain, called the \textbf{homotopy coherent isomorphism}, is the nerve of the free-living isomorphism: + + + \begin{cor}\label{cor:coherent-iso} An arrow $f$ in a quasi-category $A$ is an isomorphism if and only if it extends to a homotopy coherent isomorphism + \[ + \begin{tikzcd} \cattwo \arrow[r, "f"] \arrow[d, hook] & A \\ \iso \arrow[ur, dashed] + \end{tikzcd} + \] + \end{cor} +% \begin{proof} +% If $f$ is an isomorphism, the map $f \colon \cattwo \to A$ lands in the maximal sub Kan complex contained in $A$: +% \[ +% \begin{tikzcd} \cattwo \arrow[r, "f"] \arrow[d, hook] & A^\simeq \subset A \\ \iso \arrow[ur, dashed] +% \end{tikzcd} +%% By Exercise \ref{exc:ar-to-iso-extension}, the inclusion $\cattwo\inc\iso$ can be expressed as a sequential composite of pushouts of outer horn inclusions. Since $A^\simeq$ is a Kan complex, this shows that the required extension exists and in fact lands in $A^\simeq \subset A$. + % \end{proof} + + \begin{rmk} +If this result proves too annoying to formalize without the general theory of ``special-outer horn filling,'' we might instead substitute a finite model of the homotopy coherent isomorphism for $\iso$. + \end{rmk} + + + + Quasi-categories define the fibrant objects in a model structure due to Joyal. We use the term \emph{isofibration} to refer to the fibrations between fibrant objects in this model structure, which admit the following concrete description. + + \begin{defn}[isofibration]\label{defn:qcat-isofibration} A simplicial map $f \colon A \to B$ between quasi-categories is an \textbf{isofibration} if it lifts against the inner horn inclusions, as displayed below-left, and also against the inclusion of either vertex into the free-living isomorphism $\iso$.\footnote{The free-living isomorphism is the 0-coskeletal simplicial set on two vertices, or equally the nerve of the free-living isomorphism of categories.} + \[ + \begin{tikzcd} + \Lambda^k[n] \arrow[d, hook] \arrow[r] & A \arrow[d, two heads, "f"] & & \catone \arrow[d, hook] \arrow[r] & A \arrow[d, two heads, "f"] \\ \Delta[n] \arrow[ur, dashed] \arrow[r] & B & & \iso \arrow[ur, dashed] \arrow[r] & B + \end{tikzcd} + \] + To notationally distinguish the isofibrations, we depict them as arrows ``$\fib$'' with two heads. +\end{defn} + +We now introduce the weak equivalences and trivial fibrations between fibrant objects in the Joyal model structure. + +\begin{defn}[equivalences of quasi-categories]\label{defn:qcat-equiv} A map $f \colon A \to B$ between quasi-categories is an \textbf{equivalence} if it extends to the data of a ``homotopy equivalence'' with the free-living isomorphism $\iso$ serving as the interval: that is, if there exist maps $g \colon B \to A$, + \[ + \begin{tikzcd} & A & & & B \\ A \arrow[ur, equals] \arrow[dr, "gf"'] \arrow[r, "\alpha"] & A^\iso \arrow[u, "\ev_0"'] \arrow[d, "\ev_1"] & \text{and} & B \arrow[dr, equals] \arrow[r, "\beta"] \arrow[ur, "fg"] & B^\iso \arrow[u, "\ev_0"'] \arrow[d, "\ev_1"] \\ & A & & & B + \end{tikzcd} + \] + We write ``$\we$'' to decorate equivalences and $A \simeq B$ to indicate the presence of an equivalence $A \we B$. + \end{defn} + + \begin{rmk}\label{rmk:qcat-htpy-cat-equiv} If $f \colon A \to B$ is an equivalence of quasi-categories, then the functor $\ho{f} \colon \ho{A} \to \ho{B}$ is an equivalence of categories, where the data displayed above defines an equivalence inverse $\ho{g} \colon \ho{B} \to \ho{A}$ and natural isomorphisms encoded by the composite\footnote{Note that $\ho(A^\iso) \ncong (\ho{A})^\iso$ in general. Objects in the latter are homotopy classes of isomorphisms in $A$, while objects in the former are homotopy coherent isomorphisms, given by a specified 1-simplex in $A$, a specified inverse 1-simplex, together with an infinite tower of coherence data indexed by the nondegenerate simplices in $\iso$.} functors + \[ \begin{tikzcd} \ho{A} \arrow[r, "\ho{\alpha}"] & \ho(A^\iso) \arrow[r] & (\ho{A})^\iso & \ho{B} \arrow[r, "\ho{\beta}"] & \ho(B^\iso) \arrow[r] & (\ho{B})^\iso \end{tikzcd} + \] + \end{rmk} + + \begin{defn}\label{defn:qcat-trivial-fib} A map $f \colon X \to Y$ between simplicial sets is a \textbf{trivial fibration} if it admits lifts against the boundary inclusions for all simplices + \begin{equation}\label{eq:qcat-trivial-fib} + \begin{tikzcd}\partial\Delta[n] \arrow[r] \arrow[d, hook] & X \arrow[d, two heads, "\sim"', "f"] \\ \Delta[n] \arrow[r] \arrow[ur, dashed] & Y + \end{tikzcd} \qquad \text{for}\ \ n \geq 0 + \end{equation} + We write ``$\trvfib$'' to decorate trivial fibrations. + \end{defn} + + \begin{rmk}\label{rmk:mono-trivi-fib-lifting} The simplex boundary inclusions $\partial\Delta[n]\inc\Delta[n]$ ``cellularly generate'' the monomorphisms of simplicial sets (see Definition \ref{defn:cellular-generation} and Lem\-ma \ref{lem:mono}). Hence the dual of Lemma \ref{lem:fib-closure} implies that trivial fibrations lift against any monomorphism between simplicial sets. In particular, it follows that any trivial fibration $X \trvfib Y$ is a split epimorphism. + \end{rmk} + + The notation ``$\trvfib$'' is suggestive: the trivial fibrations between quasi-cat\-e\-go\-ries are exactly those maps that are both isofibrations and equivalences. This can be proven by a relatively standard although rather technical argument in simplicial homotopy theory \cite[D.5.6]{RiehlVerity:2022eo}. + \section{Enriched limits}\label{sec:enriched-limits} A simplicially enriched category---commonly called a ``simplicial category'' for short---is a category that is enriched over the cartesian monoidal category of simplicial sets. We recall the definition, which already exists in Mathlib. @@ -104,6 +365,7 @@ \section{\texorpdfstring{$\infty$}{Infinity}-Cosmoi}\label{sec:cosmos} There are a variety of models of infinite-dimensional categories for which the category of ``$\infty$-categories,'' as we call them, and ``$\infty$-functors'' between them is enriched over quasi-categories and admits classes of isofibrations, equivalences, and trivial fibrations satisfying certain properties that are familiar from abstract homotopy theory, forming a \emph{category of fibrant objects} \`{a} la Brown \cite{Brown:1973ah}. In particular, the use of isofibrations in diagrams guarantees that their strict limits are equivalence invariant, so we can take advantage of up-to-isomorphism universal properties and strict functoriality of these constructions while still working ``homotopically.'' This motivates the following axiomatization: + \begin{defn}[$\infty$-cosmos]\label{defn:cosmos} An $\infty$-\textbf{cosmos} $\cK$ is a category that is enriched over quasi-categories,\footnote{This is to say $\cK$ is a simplicially enriched category (see Definition \ref{defn:simplicial-category}) whose hom spaces are all quasi-categories.} meaning in particular that\begin{itemize} \item its morphisms $f \colon A \to B$ define the vertices of a quasi-category denoted $\Fun(A,B)$ and referred to as a \textbf{functor space}, \end{itemize} @@ -126,8 +388,492 @@ \section{\texorpdfstring{$\infty$}{Infinity}-Cosmoi}\label{sec:cosmos} Put more concisely, one might say that an $\infty$-cosmos is a ``quasi-cat\-e\-go\-ri\-cal\-ly enriched category of fibrant objects.'' %(see Definition \ref{defn:cat-of-fib-obj} and Example \ref{ex:cosmos-as-cat-of-fib-obj}). -\begin{con}[$\infty$-category, as a technical term]Henceforth, we recast $\infty$-\textbf{category} as a technical term to refer to an object in an arbitrary ambient $\infty$-cosmos. Similarly, we use the term $\infty$-\textbf{functor} {\textendash} or more commonly the elision ``\textbf{functor}'' {\textendash} to refer to a morphism $f \colon A \to B$ in an $\infty$-cosmos. This explains why we refer to the quasi-category $\Fun(A,B)$ between two $\infty$-categories in an $\infty$-cosmos as a ``functor space'': its vertices are the ($\infty$-)functors from $A$ to $B$. +\begin{con}[$\infty$-category, as a technical term]Henceforth, we recast $\infty$-\textbf{category} as a technical term to refer to an object in an arbitrary ambient $\infty$-cosmos. Similarly, we use the term $\infty$-\textbf{functor} --- or more commonly the elision ``\textbf{functor}'' --- to refer to a morphism $f \colon A \to B$ in an $\infty$-cosmos. This explains why we refer to the quasi-category $\Fun(A,B)$ between two $\infty$-categories in an $\infty$-cosmos as a ``functor space'': its vertices are the ($\infty$-)functors from $A$ to $B$. \end{con} \begin{rmk} The underlying category $\cK_0$ of an $\infty$-cosmos $\cK$ is the category whose objects are the $\infty$-categories in $\cK$ and whose morphisms are the $0$-arrows, i.e., the vertices in the functor spaces. In all of the examples to appear in what follows, this recovers the expected category of $\infty$-categories in a particular model and functors between them. \end{rmk} + +The following theorem should be quite difficult to formalize: + +\begin{prop}[the $\infty$-cosmos of quasi-categories]\label{prop:qcat-cosmos} The full subcategory $\qCat\subset\sSet$ of quasi-categories defines an $\infty$-cosmos in which the isofibrations, equivalences, and trivial fibrations coincide with the classes already bearing these names. +\end{prop} + + +Two further examples fit into a common paradigm: both arise as full subcategories of the $\infty$-cosmos of quasi-categories and inherit their $\infty$-cosmos structures from this inclusion (see Lemma \cite[6.1.4]{RiehlVerity:2022eo}), but it is also instructive, and ultimately takes less work, to describe the resulting $\infty$-cosmos structures directly. + +\begin{prop}[the $\infty$-cosmos of categories]\label{prop:cat-cosmos} +The category $\Cat$ of 1-cat\-e\-go\-ri\-es defines an $\infty$-cosmos whose isofibrations are the \textbf{isofibrations}: functors satisfying the displayed right lifting property: +\[ +\begin{tikzcd} +\catone \arrow[d, hook] \arrow[r] & A \arrow[d, "f", two heads] \\ \iso \arrow[r] \arrow[ur, dashed] & B +\end{tikzcd} +\] +The equivalences are the equivalences of categories and the trivial fibrations are \textbf{surjective equivalences}: equivalences of categories that are also surjective on objects. +\end{prop} +\begin{proof} +It is well-known that the 2-category of categories is complete (and in fact also cocomplete) as a $\Cat$-enriched category (see %Definition \ref{defn:enriched-completeness} or + \cite{Kelly:1989eo}). The categorically enriched category of categories becomes a quasi-categorically enriched category by applying the nerve functor to the hom-categories (see \S\ref{sec:change-of-base}). Since the nerve functor is a right adjoint, it follows formally that these 2-categorical limits become simplicially enriched limits. In particular, as proscribed in Proposition \ref{prop:cob-adjunction}, the cotensor of a category $A$ by a simplicial set $U$ is defined to be the functor category $A^{\ho{U}}$. This completes the verification of axiom \ref{itm:cosmos-limits}. + +Since the class of isofibrations is characterized by a right lifting property, %Lemma \ref{lem:fib-closure} implies that + the isofibrations are closed under all of the limit constructions of \ref{defn:cosmos}\ref{itm:cosmos-isofib} except for the last two. %and by Exercise \ref{exc:degenerate-leibniz}, + For these, the Leibniz closure subsumes the closure under exponentiation. + +To verify that isofibrations of categories $f \colon A \fib B$ are stable under forming Leibniz cotensors with monomorphisms of simplicial sets $i \colon U \inc V$, we must solve the lifting problem below-left +\[ +\begin{tikzcd} \catone \arrow[r, "s"] \arrow[d, hook, "j"'] & A^{\ho{V}} \arrow[d, "{\ho{i}\leib\pwr f}"] \arrow[dr, phantom, "\leftrightsquigarrow"] & \ho{U} \times \iso \cup_{\ho{U}} \ho{V} \arrow[r, "{\langle \alpha, s\rangle}"] \arrow[d, hook, "\ho{i} \leib\times j"'] & A \arrow[d, two heads, "f"] \\ \iso \arrow[ur, dashed, "\gamma"] \arrow[r, "{\langle \beta, \alpha \rangle}"'] & B^{\ho V} \times_{B^{\ho U}} A^{\ho U} & \ho{V} \times \iso \arrow[r, "\beta"'] \arrow[ur, dashed, "\gamma"'] & B +\end{tikzcd} +\] +which transposes to the lifting problem above-right, which we can solve by hand. Here the map $\beta$ defines a natural isomorphism between $fs \colon \ho{V} \to B$ and a second functor. Our task is to lift this to a natural isomorphism $\gamma$ from $s$ to another functor that extends the natural isomorphism $\alpha$ along $\ho{i} \colon \ho{U} \to \ho{V}$. Note this functor $\ho{i}$ need not be an inclusion, but it is injective on objects, which is enough. + +We define the components of $\gamma$ by cases. If an object $v \in \ho{V}$ is equal to $i(u)$ for some $u \in \ho{U}$ define $\gamma_{i(u)} \coloneq \alpha_u$; otherwise, use the fact that $f$ is an isofibration to define $\gamma_v$ to be any lift of the isomorphism $\beta_v$ to an isomorphism in $A$ with domain $s(v)$. The data of the map $\gamma \colon \ho{V} \times \iso \to A$ also entails the specification of the functor $\ho{V} \to A$ that is the codomain of the natural isomorphism $\gamma$. On objects, this functor is given by $v \mapsto \cod(\gamma_v)$. On morphisms, this functor defined in the unique way that makes $\gamma$ into a natural transformation: +\[ (k \colon v \to v') \mapsto \gamma_{v'} \circ s(k) \circ \gamma_v^{-1}.\] + +This completes the proof that $\Cat$ defines an $\infty$-cosmos. Since the nerve of a functor category, such as $A^\iso$, is isomorphic to the exponential between their nerves, the equivalences of categories coincide with the equivalences of Definition \ref{defn:qcat-equiv}. It follows that the equivalences in the $\infty$-cosmos of categories coincide with equivalences of categories, and since the surjective equivalences are the intersection of the equivalences and the isofibrations, this completes the proof. +\end{proof} + +Similarly: + +\begin{prop}[the $\infty$-cosmos of Kan complexes]\label{prop:kan-cosmos} The category $\Kan$ of Kan complexes defines an $\infty$-cosmos whose isofibrations are the \textbf{Kan fibrations}: maps that lift against all horn inclusions $\Lambda^k[n] \inc \Delta[n]$ for $n \geq 1$ and $0 \leq k \leq n$. +\end{prop} + +Several consequences of the $\infty$-cosmos axioms are mentioned in \cite[\S 1.2]{RiehlVerity:2022eo}. For now, we focus on just one. + +By a Yoneda-style argument, the ``homotopy equivalence'' characterization of the equivalences in the $\infty$-cosmos of quasi-categories of Definition \ref{defn:qcat-equiv} extends to an analogous characterization of the equivalences in any $\infty$-cosmos: + +\begin{lem}[equivalences are homotopy equivalences]\label{lem:equiv-htpy-equiv} +A map $f \colon A \to B$ between $\infty$-categories in an $\infty$-cosmos $\cK$ is an equivalence if and only if it extends to the data of a ``homotopy equivalence'' with the free-living isomorphism $\iso$ serving as the interval: that is, if there exist maps $g \colon B \to A$ +\begin{equation}\label{eq:htpy-equiv} +\begin{tikzcd} & A & & & B \\ A \arrow[ur, equals] \arrow[dr, "gf"'] \arrow[r, "\alpha"] & A^\iso \arrow[u, two heads, "\sim", "\ev_0"'] \arrow[d, two heads, "\sim"', "\ev_1"] & \text{and} & B \arrow[dr, equals] \arrow[r, "\beta"] \arrow[ur, "fg"] & B^\iso \arrow[u, two heads, "\sim", "\ev_0"'] \arrow[d, two heads, "\sim"', "\ev_1"] \\ & A & & & B +\end{tikzcd} +\end{equation} +in the $\infty$-cosmos. +\end{lem} +\begin{proof} +By hypothesis, if $f \colon A \to B$ defines an equivalence in the $\infty$-cosmos $\cK$ then the induced map on post-composition $f_* \colon \Fun(B,A) \we \Fun(B,B)$ is an equivalence of quasi-categories in the sense of Definition \ref{defn:qcat-equiv}. Evaluating the inverse equivalence $\tilde{g} \colon \Fun(B,B) \we \Fun(B,A)$ and homotopy $\tilde{\beta} \colon \Fun(B,B) \to \Fun(B,B)^\iso$ at the 0-arrow $\id_B \in \Fun(B,B)$, we obtain a 0-arrow $g \colon B \to A$ together with an isomorphism $\beta \colon \iso\to\Fun(B,B)$ from the composite $fg$ to $\id_B$. By the defining universal property of the cotensor \eqref{eq:cotensor-defn}, this isomorphism internalizes to define the map $\beta \colon B \to B^\iso$ in $\cK$ displayed on the right of \eqref{eq:htpy-equiv}. + +Now the hypothesis that $f$ is an equivalence also provides an equivalence of quasi-categories $f_* \colon \Fun(A,A) \we \Fun(A,B)$, and the map $\beta f \colon A \to B^\iso$ represents an isomorphism in $\Fun(A,B)$ from $fgf$ to $f$. Since $f_*$ is an equivalence, we conclude from Remark \ref{rmk:qcat-htpy-cat-equiv} that $\id_A$ and $gf$ are isomorphic in the quasi-category $\Fun(A,A)$: explicitly, such an isomorphism may be defined by applying the inverse equivalence $\tilde{h} \colon \Fun(A,B) \to \Fun(A,A)$ and composing with the components at $\id_A, gf \in \Fun(A,A)$ of the isomorphism $\tilde{\alpha} \colon \Fun(A,A) \to \Fun(A,A)^\iso$ from $\id_{\Fun(A,A)}$ to $\tilde{h}f_*$. Now by Corollary \ref{cor:coherent-iso} this isomorphism is represented by a map $\iso \to \Fun(A,A)$ from $\id_A$ to $gf$, which internalizes to a map $\alpha \colon A \to A^\iso$ in $\cK$ displayed on the left of \eqref{eq:htpy-equiv}. + +The converse is easy: the simplicial cotensor construction commutes with $\Fun(X,-)$, so a homotopy equivalence \eqref{eq:htpy-equiv} induces a homotopy equivalence of quasi-categories as in Definition \ref{defn:qcat-equiv}. +\end{proof} + + +Many, though not all, of the $\infty$-cosmoi we encounter ``in the wild'' satisfy an additional axiom: + +\begin{defn}[cartesian closed $\infty$-cosmoi]\label{defn:closed-cosmos} An $\infty$-cosmos $\cK$ is \textbf{cartesian closed} if the product bifunctor +$- \times -\colon \cK \times \cK \to \cK$ extends to a simplicially enriched two-variable adjunction +\[ \Fun(A \times B,C) \cong \Fun(A,C^B) \cong \Fun(B,C^A)\] +in which the right adjoints $(-)^A \colon \cK \to \cK$ preserve isofibrations for all $A \in \cK$. +\end{defn} + +For instance, the $\infty$-cosmos of quasi-categories is cartesian closed, with the exponentials defined as (special cases of) simplicial cotensors. This is one of the reasons that we use the same notation for cotensor and for exponential. Note in this case the functor spaces and the exponentials coincide. The same is true for the cartesian closed $\infty$-cosmoi of categories and of Kan complexes. In general, the functor space from $A$ to $B$ is the ``underlying quasi-category'' of the exponential $B^A$ whenever it exists. % (see Remark \ref{rmk:underlying-internal-hom}). + +\section{Change of base}\label{sec:change-of-base} + +``Change of base,'' first considered by Eilenberg and Kelly in \cite{EilenbergKelly:1966cc}, refers to a systematic procedure by which enrichment over one category $\cV$ is converted into enrichment over another category $\cW$. This will be applied in \S\ref{sec:htpy-2-cat} to convert an $\infty$-cosmos into a simpler structure. +%Corollary \ref{cor:V-cat-2-cat} notes that + For a cartesian closed category $\cV$, there is a 2-category $\eCat{\cV}$ of $\cV$-categories, $\cV$-functors, and $\cV$-natural transformations. The first main result, appearing as Proposition \ref{prop:change-of-base}, gives conditions under which a functor $T \colon \cV \to \cW$ between cartesian closed categories induces a change-of-base 2-functor $T_* \colon \eCat{\cV} \to \eCat{\cW}$. + +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 \emph{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. + +\begin{defn}\label{defn:lax-monoidal} A \textbf{(lax) monoidal functor} between cartesian closed categories $\cV$ and $\cW$ is a functor $T \colon \cV \to \cW$ 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. +\end{defn} + +\begin{defn} A \textbf{(lax) monoidal natural transformation} between monoidal functors between cartesian closed categories $T,U \colon \cV \to \cW$ is given by a natural transformation $\theta \colon T \To U$ so that the pasting diagrams commute +\[ +\begin{tikzcd}[row sep=large, column sep=2.3em] \cV \times \cV \arrow[r, "T\times T", bend left] \arrow[r, "U \times U"', bend right] \arrow[r, phantom, "\scriptstyle\Downarrow\theta\times\theta"] \arrow[dr, phantom, "\scriptstyle\Downarrow\phi\quad" pos=.7] \arrow[d, "\times"'] & \cW \times \cW \arrow[d, "\times"] \arrow[dr, phantom, "="] & \cV \times \cV \arrow[r, "T\times T"] \arrow[dr, phantom, "\scriptstyle\quad\Downarrow\phi" pos=.3] \arrow[d, "\times"'] & \cW \times \cW \arrow[d, "\times"] & \catone \arrow[r, "1"] \arrow[dr, bend right, "1"'] & \cV \arrow[d, bend right, "T"'] \arrow[d, bend left, "U"] \arrow[d, phantom, "\scriptstyle\To" pos=.6, "\scriptstyle\theta" pos=.4] \arrow[dr, phantom, "="] & \catone \arrow[r, "1"] \arrow[dr, "1"'] & \arrow[d, "U"] \cV \\ \cV \arrow[r, "U"'] & \cW & +\cV \arrow[r, "T", bend left] \arrow[r, "U"', bend right] \arrow[r, phantom, "\scriptstyle\Downarrow\theta"] & \cW &\arrow[ur, phantom, "\scriptstyle\Uparrow\phi_0\quad\quad" pos=.75] & \cW &~\arrow[ur, phantom, "\scriptstyle\Uparrow\phi_0" pos=.85] & \cW +\end{tikzcd} +\] +\end{defn} + +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 \cV \to \cW$ between cartesian closed categories \textbf{preserves finite products} just when the natural maps defined for any $u,v \in \cV$ +\[ T(u \times v) \isoto Tu \times Tv \qquad \text{and} \qquad T1 \isoto 1\] +are isomorphisms. These maps satisfy the duals of the coherence conditions mentioned in Definition \ref{defn:lax-monoidal} and make $T$ into a \textbf{strong monoidal functor} between the cartesian closed categories $\cV$ and $\cW$. The inverse isomorphisms then provide the structure maps of Definition \ref{defn:lax-monoidal}. Moreover, any natural transformation between product-preserving functors is automatically a monoidal natural transformation. + +For example: + + +\begin{ex}\label{ex:lax-u-set} Since representable functors preserve products, for any cartesian closed category $\cV$, the underlying set functor $(-)_0 \colon \cV \to \Set$ is product-preserving +\end{ex} + +\begin{ex}\label{ex:strong-free} In a cartesian closed category $\cV$, 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} \Set \arrow[r, "{\amalg_{-} 1}"] & \cV +\end{tikzcd} +\] is finite-product-preserving. +\end{ex} + +A finite-product-preserving functor may be used to change the base as follows + +\begin{prop}\label{prop:change-of-base} A finite-product-preserving functor $T \colon \cV \to \cW$ between cartesian closed categories induces a change-of-base 2-functor \[ \begin{tikzcd} \eCat{\cV} \arrow[r, "T_*"] & \eCat{\cW}\, . \end{tikzcd}\] +\end{prop} + +An early observation along these lines was first stated as \cite[II.6.3]{EilenbergKelly:1966cc}, with the proof left to the reader. We adopt the same tactic and leave the diagram chases to the reader or to \cite[4.2.4]{Cruttwell:2008rr} and instead just give the construction of the change-of-base 2-functor, which is the important thing. + +\begin{proof} Let $\cC$ be a $\cV$-category and define a $\cW$-category $T_*\cC$ to have the same objects and to have mapping objects $T_*\cC(x,y) \coloneq T\cC(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_*\cC$ is a $\cW$-category. + +If $F \colon \cC \to \cD$ is a $\cV$-functor, then we define a $\cW$-functor $T_*F \colon T_*\cC \to T_*\cD$ to act on objects by $c \in\cC \mapsto Fc \in \cD$ 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 $\cW$-functorial. It is evident from this definition that $T_*(GF) = T_*G \cdot T_*F$. + +Finally, let $\alpha \colon F \To G$ be a $\cV$-natural transformation between $\cV$-functors $F,G \colon \cC\to \cD$ and define a $\cW$-natural transformation $T_*\alpha \colon T_* F \To 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 $\cW$-natural. + +It remains to verify this assignment is functorial for both horizontal and vertical composition of enriched natural transformations. %Consulting Definition \ref{defn:V-cat-2-cat}, we see that + 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 \To 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. +\end{proof} + + +\begin{rmk}\label{rmk:change-of-base-2-fun} In fact, the ``change of base'' procedure $\cV \mapsto \eCat{\cV}$ is \emph{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-cat\-e\-go\-ries, 2-functors, and 2-natural transformations. See \cite[\S 4.3]{Cruttwell:2008rr} for a discussion and proof. +\end{rmk} + + +As an immediate consequence of the 2-functoriality of Remark \ref{rmk:change-of-base-2-fun}: + +\begin{prop}\label{prop:change-of-base-adjunction} 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"] & \eCat{\cV} \arrow[r, bend left=20, start anchor=10, end anchor=170, "F_*"] \arrow[r, phantom, "\bot"] & \eCat{\cW} \arrow[l, bend left=20, start anchor=190, end anchor=-10, "U_*"] +\end{tikzcd} +\] +\end{prop} +\begin{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 \ref{rmk:change-of-base-2-fun}. The 2-functor $\cV \mapsto \eCat{\cV}$ then carries the adjunction displayed on the left to the adjunction displayed on the right. +\end{proof} + +As a special case: + +\begin{cor}\label{cor:free-underlying-2-adj} For any cartesian closed category $\cV$ with coproducts, the underlying category construction and free category construction define adjoint 2-functors +\[ +\pushQED{\qed} +\begin{tikzcd}[column sep=large] +\Cat \arrow[r, bend left=20, hook, start anchor=10, end anchor=170] \arrow[r, phantom, "\bot"] & \eCat{\cV} \arrow[l, bend left=20, start anchor=190, end anchor=-10, "(-)_0"] +\end{tikzcd} \qedhere +\popQED +\] +\end{cor} + + +In light of Proposition \ref{prop:change-of-base-adjunction} and results to follow, an adjunction between cartesian closed categories whose left adjoint preserves finite products provides a \textbf{change-of-base adjunction}. While Proposition \ref{prop:change-of-base-adjunction} 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. + + +\begin{lem}\label{lem:enriched-cob-adjunction} +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 $\cV$-enriched adjunction between the $\cV$-categories $\cV$ and $U_*\cW$; i.e., there exists a $\cV$-natural isomorphism $U\cW(Fv,w) \cong \cV(v,Uw)$. +\end{lem} +\begin{proof} +The internal action $U_{a,b} \colon U\cW(a,b) \to \cV(Ua,Ub)$ of the $\cV$-functor $U \colon U_*\cW \to \cV$ is defined by the transpose of the map $U\ev \colon U\cW(a,b) \times Ua \to Ub$ defined by applying $U$ to the counit of the cartesian closure adjunction of $\cW$. The $\cV$-functoriality of this map follows from naturality of evaluation in a cartesian closed category. + %\eqref{eq:ev-ev-square} + + +By the $\cV$-functoriality of $U \colon U_*\cW \to \cV$, 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 $\cV$-natural in $w \in U_*\cW$ for all $v \in \cV$. By a general result about enriching adjoints, % Remark \ref{rmk:enriching-adjoints}, + to construct a compatible $\cV$-enrichment of $F$, we need only demonstrate that this map in an isomorphism in $\cV$. + +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 $\cW$-functor $F \colon F_*\cV \to \cW$, which is defined similarly to the $\cV$-functor $U \colon U_*\cW \to \cV$. + +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 \id_\cV \To UF$ is a \emph{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. % (see Exercise \ref{exc:product-preservation-is-monoidal}). + The other diagram chase is similar. +\end{proof} + +\begin{prop}\label{prop:cob-adjunction} +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 $\cC$ is co/tensored as a $\cW$-cat\-e\-gory, $U_*\cC$ is co/tensored as $\cV$-category with the co/tensor of $c \in \cC$ by $v \in \cV$ defined by +\[ v \otimes c \coloneq Fv \otimes c \qquad \text{and} \qquad c^v \coloneq c^{Fv}.\] +\end{prop} +\begin{proof} +Suppose $\cC$ admits cotensors as a $\cW$-category. To verify that $U_*\cC$ admits cotensors as a $\cV$-category we must supply an isomorphism +\[ U\cC(x,c^{Fv}) \cong (U\cC(x,c))^v\] in $\cV$ that is $\cV$-natural in $x$. By the enriched Yoneda lemma, we can extract this isomorphism from an isomorphism \[ \cV(u,U\cC(x,c^{Fv})) \cong \cV(u,(U\cC(x,c))^v)\] that is $\cV$-natural in $u \in \cV$. To that end, by composing the $\cV$-natural isomorphisms of Lemma \ref{lem:enriched-cob-adjunction}, the enriched natural isomorphisms arising from the cartesian closed structure on $\cV$ and on $U_*\cW$, and the isomorphisms that characterize the cotensor on $\cC$ and express the fact that $F$ preserves binary products, we have: +\begin{align*} \cV(u,U\cC(x,c^{Fv})) &\cong U\cW(Fu, \cC(x,c^{Fv})) \cong U\cW(Fu, \cC(x,c)^{Fv}) \\ &\cong U\cW(Fu \times Fv, \cC(x,c)) \cong U\cW(F(u \times v), \cC(x,c)) \\ &\cong \cV(u \times v, U\cC(x,c)) \cong \cV(u, (U\cC(x,c))^v). \qedhere\end{align*} +\end{proof} + + + +This theory of change of base is all well and good from the compound noun perspective on enriched categories, but an additional concern arises from the adjectival point of view. If the finite-product-preserving functor $T \colon \cV \to \cW$ commutes with the underlying set functors for $\cV$ and $\cW$ up to natural isomorphism, then by the 2-functoriality of Remark \ref{rmk:change-of-base-2-fun}, the change-of-base 2-functor $T_* \colon \eCat{\cV} \to \eCat{\cW}$ also preserves the underlying categories up to natural isomorphism. This happens in particular in the following setting. + +\begin{lem}\label{lem:right-of-monoidal-adj-ucats} Consider a finite-product-preserving 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} +\] +Then change of base along the right adjoint respects the underlying categories: +\[ +\begin{tikzcd}[sep=1.5 em] \eCat{\cW} \arrow[rr, "U_*"] \arrow[dr, "{(-)_0}"'] & & \eCat{\cV} \arrow[dl, "(-)_0"] \\ & \Cat +\end{tikzcd} +\] +\end{lem} +\begin{proof} +Let $\cC$ be a $\cW$ category. Then the hom-set in the underlying category of $U_*\cC$ from $x$ to $y$ is isomorphic to the corresponding hom-set +\[ U_*\cC(x,y)_0 \cong \cV(1, U\cC(x,y))_0 \cong \cW(F1,\cC(x,y))_0 \cong \cW(1,\cC(x,y))_0 \cong \cC(x,y)_0\] +in the underlying category of $\cC$ and moreover this isomorphism respects the composition and identities in the underlying categories. Thus $\cC_0 \cong U\cC_0$. A similar argument shows that change of base along $U$ respects underlying functors and natural transformations. +\end{proof} + + +%\begin{lem}\label{lem:pro-normal-monoidal} The change-of-base 2-functor induced by a finite-product-preserving functor $T \colon \cV \to \cW$ between cartesian closed categories preserves underlying categories, if and only if, for each $v \in \cV$ the composite function on hom-sets +%\[ +%\begin{tikzcd} \cV(1,v)_0 \arrow[r, "T"] & \cW(T1,Tv)_0 \arrow[r, "- \circ \cong"] & \cW(1,Tv)_0 +%\end{tikzcd} +%\] is a bijection. +%\end{lem} +%\begin{proof} +%The displayed function defines the component at $v \in \cV$ of the unique monoidal natural transformation from the underlying set-functor for $\cV$ to the composite of $T$ with the underlying set functor for $\cW$. By the 2-functoriality of Remark \ref{rmk:change-of-base-2-fun}, if it defines a monoidal natural isomorphism, then it induces a 2-natural isomorphism between the underlying category 2-functor $(-)_0 \colon \eCat{\cV} \to \Cat$ and the composite of the change-of-base 2-functor $T_* \colon \eCat{\cV} \to\eCat{\cW}$ with the underlying category 2-functor $(-)_0 \colon \eCat{\cW} \to \Cat$. + +%Conversely, this condition is necessary for the underlying category of the $\cW$-category $T_*\cV$ to coincide with the underlying category of the cartesian closed category $\cV$. +%\end{proof} + +%One situation in which the condition of Lemma \ref{lem:pro-normal-monoidal} is automatic is when the lax monoidal functor is the right adjoint of a monoidal adjunction. The proof, originally given in \cite{Kelly:1974da}, is by a short diagram chase. + +The general theory of change-of-base will be applied in the following case the next section. + + +\begin{ex}\label{ex:nerve-ho-change-of-base} +Both adjoints of the adjunction +\[ +\begin{tikzcd}[column sep=large] +\sSet \arrow[r, bend left=20, start anchor=10, end anchor=170, "\ho"] \arrow[r, phantom, "\bot"] & \Cat \arrow[l, bend left=20, start anchor=190, end anchor=-10, hook'] +\end{tikzcd} +\] of Proposition \ref{prop:ho-nerve-adjunction} preserve finite products. Hence, Proposition \ref{prop:change-of-base-adjunction} induces a change-of-base adjunction defined by the 2-functors +\[ +\begin{tikzcd}[column sep=large] + \sCat \arrow[r, bend left=20, start anchor=7, end anchor=170, "\ho_*"] \arrow[r, phantom, "\bot"] &\twoCat\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. By Lemma \ref{lem:right-of-monoidal-adj-ucats}, 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 $\ho \colon \sSet \to \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. +\end{ex} + + +\section{The homotopy 2-category}\label{sec:htpy-2-cat} + +Small 1-categories define the objects of a strict 2-category $\Cat$ of categories, functors, and natural transformations. Many basic categorical notions --- those defined in terms of categories, functors, and natural transformations --- can be defined internally to the 2-category $\Cat$. This suggests a natural avenue for generalization: reinterpreting these same definitions in a generic 2-category using its objects in place of small categories, its 1-cells in place of functors, and its 2-cells in place of natural transformations. + +A significant portion of the theory of $\infty$-cat\-e\-go\-ries in any fixed $\infty$-cosmos can be developed by following exactly this outline, working internally to a 2-category that we refer to as the \emph{homotopy 2-category} that we associate to any $\infty$-cosmos. The homotopy 2-category of an $\infty$-cosmos is a quotient of the full $\infty$-cosmos, replacing each quasi-categorical functor space by its homotopy category. Surprisingly, this rather destructive quotienting operation preserves quite a lot of information. This said, we caution the reader against becoming overly seduced by homotopy 2-categories, which are more of a technical convenience for reducing the complexity of our arguments than a fundamental notion of $\infty$-category theory. + +Paralleling our discussion of simplicial categories in Definition \ref{defn:simplicial-category} and Digression \ref{dig:simplicial-cat}, there are two perspectives on the notion of a 2-category, which can be understood equally as: +\begin{enumerate} +\item\label{itm:strict-bicategory} ``two-dimensional'' categories, with objects; \textbf{1-cells}, whose boundary are given by a pair of objects; and \textbf{2-cells}, whose boundary are given by a parallel pair of 1-cells between a pair of objects --- together with partially defined composition operations governed by this boundary data +\item or as categories enriched over $\Cat$. +\end{enumerate} + +Both notions exist in Mathlib in some form. The notion \ref{itm:strict-bicategory} is called a \emph{strict bicategory} and is defined as a special case of a bicategory, in which the associators and unitors are identities (converted into 2-cells). The general notion of enriched category can be specialized to the case of enriching over the cartesian monoidal category of categories, but the connection between these notions remains to be explored. + +\begin{prop} There is an equivalence between categories enriched in categories and strict bicategories. In particular, each can be converted into the other. +\end{prop} + +The homotopy 2-category is most efficiently defined as a category enriched in $\Cat$ by applying the theory of change-of-base developed in \S\ref{sec:change-of-base}. The homotopy 2-category for the $\infty$-cosmos of quasi-categories was first introduced by Joyal in his work on the foundations of quasi-category theory \cite{Joyal:2008tq}. + +\begin{defn}[homotopy 2-category]\label{defn:homotopy-2-cat} Let $\cK$ be an $\infty$-cosmos. Its \textbf{homotopy 2-category} is the 2-category $\h\cK$ whose +\begin{itemize} +\item objects are the objects $A, B$ of $\cK$, i.e., the $\infty$-categories;\item 1-cells $f \colon A \to B$ are the 0-arrows in the functor space $\Fun(A,B)$, i.e., the $\infty$-functors; and +\item 2-cells $\begin{tikzcd} A \arrow[r, start anchor=15, end anchor=165, bend left, "f"] \arrow[r, start anchor=345, end anchor=195, bend right, "g"'] \arrow[r, phantom, "{\scriptstyle\Downarrow \alpha}"] & B\end{tikzcd}$ are homotopy classes of 1-simplices in $\Fun(A,B)$, which we call \textbf{$\infty$-natural transformations}. +\end{itemize} +Put another way $\h\cK$ is the 2-category with the same objects as $\cK$ and with hom-categories defined by +\[ \hFun(A,B) \coloneq \ho(\Fun(A,B)),\] +that is, $\hFun(A,B)$ is the homotopy category of the quasi-category $\Fun(A,B)$. +\end{defn} + +\begin{defn}[underlying category of a 2-category]\label{defn:underlying-cat-of-2cat} +The \textbf{underlying category} of a 2-category is defined by simply forgetting its 2-cells. Note that an $\infty$-cosmos $\cK$ and its homotopy 2-category $\h\cK$ share the same underlying category $\cK_0$ of $\infty$-categories and $\infty$-functors in $\cK$. +\end{defn} + +By Lemma \ref{lem:right-of-monoidal-adj-ucats}: + +\begin{lem} The underlying category of the homotopy 2-category of an $\infty$-cosmos is isomorphic to the underlying category of the $\infty$-cosmos. \qed +\end{lem} + +We elaborate on the connection between data in the homotopy 2-category and data in the $\infty$-cosmos. + +\begin{lem}\label{lem:invertible-2-cell}$\quad$ + \begin{enumerate} + \item\label{itm:2-cell-as-functor} Every 2-cell $\begin{tikzcd} A \arrow[r, start anchor=15, end anchor=165, bend left, "f"] \arrow[r, start anchor=345, end anchor=195, bend right, "g"'] \arrow[r, phantom, "\scriptstyle\Downarrow\alpha"] & B \end{tikzcd}$ in the homotopy 2-category of an $\infty$-cosmos is represented by a map of quasi-categories as below-left or equivalently by a functor as below-right + \[ + \begin{tikzcd}[sep=small] & \catone+\catone \arrow[dl, hook'] \arrow[dr, "{(f,g)}"] & & & ~ & A \arrow[rr, "\name{\alpha}"] \arrow[dr, "{(g,f)}"'] & & B^\cattwo \arrow[dl, "{(p_1,p_0)}", two heads] \\ \cattwo \arrow[rr, "{\alpha}"'] && \Fun(A,B) &\arrow[ur, phantom, "\leftrightsquigarrow"] & && B \times B + \end{tikzcd} + \] + and two such maps represent the same 2-cell if and only if they are homotopic as 1-simplices in $\Fun(A,B)$. + \item\label{itm:2-iso-as-functor} Every invertible 2-cell $ \begin{tikzcd}[column sep=large] A \arrow[r, start anchor=18, end anchor=162, bend left=20, "f"] \arrow[r, start anchor=342, end anchor=198, bend right=20, "g"'] \arrow[r, phantom, "\scriptstyle\cong\Downarrow\alpha"] & B \end{tikzcd}$ + in the homotopy 2-category of an $\infty$-cosmos is represented by a map of quasi-categories as below-left or equivalently by a functor as below-right + \[ + \begin{tikzcd}[sep=small] & \catone+\catone \arrow[dl, hook'] \arrow[dr, "{(f,g)}"] & & & ~ & A \arrow[rr, "\name{\alpha}"] \arrow[dr, "{(g,f)}"'] & & B^\iso \arrow[dl, "{(p_1,p_0)}", two heads] \\ \iso \arrow[rr, "{\alpha}"'] && \Fun(A,B) &\arrow[ur, phantom, "\leftrightsquigarrow"] & && B \times B + \end{tikzcd} + \] and two such maps represent the same invertible 2-cell if and only if their common restrictions along $\cattwo \inc \iso$ are homotopic as 1-simplices in $\Fun(A,B)$. + \end{enumerate} + \end{lem} + + The notion of homotopic 1-simplices referenced here is defined in Lemma \ref{lem:1-simp-htpy}. Since the 2-cells in the homotopy 2-category are referred to as $\infty$-natural transformations, we refer to the invertible 2-cells in the homotopy 2-category as \textbf{$\infty$-natural isomorphisms}. + + \begin{proof} + The statement \ref{itm:2-cell-as-functor} records the definition of the 2-cells in the homotopy 2-category and the universal property \eqref{eq:cotensor-defn} of the simplicial cotensor. For \ref{itm:2-iso-as-functor}, a 2-cell in the homotopy 2-category is \textbf{invertible} if and only if it defines an isomorphism in the appropriate hom-category $\hFun(A,B)$. By Corollary \ref{cor:coherent-iso} it follows that each invertible 2-cell $\alpha$ is represented by a homotopy coherent isomorphism ${\alpha} \colon \iso \to \Fun(A,B)$, which similarly internalizes to define a functor $\name{\alpha} \colon A \to B^\iso$. + \end{proof} + + %Change of base is an operation that applies to enriched functors as well as enriched categories, as can be directly verified in the case of greatest interest. + +% \begin{lem}\label{lem:cosmological-2-fun} Any simplicial functor $F \colon \cK \to \cL$ between $\infty$-cosmoi induces a 2-functor $F \colon \h\cK \to \h\cL$ between their homotopy 2-categories. + % \end{lem} + %\begin{proof} + % The action of the induced 2-functor $F \colon \h\cK \to \h\cL$ on objects and 1-cells is given by the corresponding action of $F \colon \cK \to \cL$; recall an $\infty$-cosmos and its homotopy 2-category have the same underlying 1-category. Each 2-cell in $\h\cK$ is represented by a 1-simplex in $\Fun(A,B)$ which is mapped via + % \[ + % \begin{tikzcd}[column sep=large, inner sep=0pt] \Fun(A,B) \arrow[r, "F"] & \Fun(FA,FB) + % \end{tikzcd} + % \] + %\vspace{-4ex} + %\[ + % \begin{tikzcd}[column sep=large, inner sep=0pt] A \arrow[r, start anchor=15, end anchor=165, bend left, "f"] \arrow[r, start anchor=345, end anchor=195, bend right, bend right, "g"'] \arrow[r, phantom, "{\scriptstyle\Downarrow \alpha}"] & B\arrow[r, maps to] & FA \arrow[r, start anchor=15, end anchor=165, bend left, "Ff"] \arrow[r, start anchor=345, end anchor=195, bend right, bend right, "Fg"'] \arrow[r, phantom, "{\scriptstyle\Downarrow F\alpha}"] & FB + % \end{tikzcd} + %\] + % to a 1-simplex representing a 2-cell in $\h\cL$. Since the action $F \colon \Fun(A,B) \to \Fun(FA,FB)$ on functor spaces defines a morphism of simplicial sets, it preserves faces and degeneracies. In particular, homotopic 1-simplices in $\Fun(A,B)$ are carried to homotopic 1-simplices in $\Fun(FA,FB)$ so the action on 2-cells just described is well-defined. The 2-functoriality of these mappings follows from the simplicial functoriality of the original mapping. + %\end{proof} + + We now begin to relate the simplicially enriched structures of an $\infty$-cosmos to the 2-cat\-e\-go\-ri\-cal structures in its homotopy 2-category by proving that homotopy 2-categories inherit products from their $\infty$-cosmoi that satisfy a 2-cat\-e\-go\-ri\-cal universal property. To illustrate, recall that the terminal $\infty$-category $1 \in \cK$ has the universal property $\Fun(X,1) \cong \catone$ for all $X \in \cK$. Applying the homotopy category functor we see that $1 \in \h\cK$ has the universal property $\hFun(X,1) \cong \catone$ for all $X \in \h\cK$, which is expressed by saying that the $\infty$-category $1$ defines a \textbf{2-terminal object} in the homotopy 2-category. This 2-categorical universal property has both a 1-dimensional and a 2-dimensional aspect. Since $\hFun(X,1)\cong \catone$ is a category with a single object, there exists a unique morphism $X \to 1$ in $\cK$, and since $\hFun(X,1)\cong\catone$ has only a single morphism, the only 2-cells in $\h\cK$ with codomain 1 are identities. + + \begin{prop}[cartesian (closure)]\label{prop:htpy-2-cat-closure} + $\quad$ + \begin{enumerate} + \item The homotopy 2-category of any $\infty$-cosmos has 2-categorical products. + \item\label{itm:cart-closed} The homotopy 2-category of a cartesian closed $\infty$-cosmos is cartesian closed as a 2-category. + \end{enumerate} + \end{prop} + \begin{proof} + While the functor $\ho\colon\sSet \to \Cat$ only preserves finite products, the restricted functor $\ho\colon\qCat\to\Cat$ preserves \emph{all} products on account of the simplified description of the homotopy category of a quasi-category given in Lemma \ref{lem:htpy-cat-of-qcat}. Thus for any set $I$ and family of $\infty$-categories $(A_i)_{i \in I}$ in $\cK$, the homotopy category functor carries the isomorphism of functor spaces to an isomorphism of hom-categories + \[ \begin{tikzcd}[column sep=small] \Fun(X,\prod_{i \in I} A_i) \arrow[r, "\cong"] & \prod_{i \in I} \Fun(X,A_i) & \arrow[r, maps to, "\ho"] & ~ & \hFun(X,\prod_{i \in I} A_i) \arrow[r, "\cong"] & \prod_{i \in I} \hFun(X,A_i). + \end{tikzcd} + \] + This proves that the homotopy 2-category $\h\cK$ has products whose universal properties have both a 1- and 2-dimensional component, as described in the empty case for terminal objects above. + + If $\cK$ is a cartesian closed $\infty$-cosmos, then for any triple of $\infty$-categories $A,B,C \in \cK$ there exist exponential objects $C^A, C^B \in \cK$ characterized by natural isomorphisms + \[ \Fun(A \times B, C) \cong \Fun(A, C^B) \cong \Fun(B,C^A).\] Passing to homotopy categories we have natural isomorphisms + \[ \hFun(A \times B, C) \cong \hFun(A, C^B) \cong \hFun(B,C^A),\] which demonstrates that $\h\cK$ is cartesian closed as a 2-category: functors $A \times B \to C$ transpose to define functors $A \to C^B$ and $B \to C^A$, and natural transformations transpose similarly. + \end{proof} + + There is a standard definition of \emph{isomorphism} between two objects in any 1-category, preserved by any functor. Similarly, there is a standard definition of \emph{equivalence} between two objects in any 2-category, preserved by any 2-functor: + + \begin{defn}[equivalence]\label{defn:2-cat-equiv} An \textbf{equivalence} in a 2-category is given by + \begin{itemize} + \item a pair of objects $A$ and $B$; + \item a pair of 1-cells $f \colon A \to B$ and $g \colon B \to A$; and + \item a pair of invertible 2-cells + \[ + \begin{tikzcd}[column sep=large] + A \arrow[r, bend left=25, equals] \arrow[r, bend right=25, "gf"'] \arrow[r, phantom, "{\scriptstyle\cong\Downarrow\alpha}"] & A & \text{and} & B \arrow[r, bend right=25, equals] \arrow[r, bend left=25, "fg"] \arrow[r, phantom, "{\scriptstyle\cong\Downarrow\beta}"] & B + \end{tikzcd} + \] + \end{itemize} + When $A$ and $B$ are \textbf{equivalent}, we write $A \simeq B$ and refer to the 1-cells $f$ and $g$ as \textbf{equivalences}, denoted by ``$\we$.'' + \end{defn} + + In the case of the homotopy 2-category of an $\infty$-cosmos we have a competing definition of equivalence from \ref{defn:cosmos}: namely a 1-cell $f \colon A \we B$ that induces an equivalence $f_* \colon \Fun(X,A) \we \Fun(X,B)$ on functor spaces --- or equivalently, by Lemma \ref{lem:equiv-htpy-equiv}, a homotopy equivalence defined relative to the interval $\iso$. Crucially, all three notions of equivalence coincide: + + \begin{thm}[equivalences are equivalences]\label{thm:equiv-are-equiv} In any $\infty$-cosmos $\cK$, the following are equivalent and characterize what it means for a functor $f \colon A \to B$ between $\infty$-categories to define an \textbf{equivalence}. + \begin{enumerate} + \item\label{itm:rep-equiv} For all $X \in \cK$, the post-composition map $f_* \colon \Fun(X,A) \we \Fun(X,B)$ defines an equivalence of quasi-categories. + \item\label{itm:2cat-equiv} There exists a functor $g \colon B \to A$ and natural isomorphisms $\alpha \colon \id_A \cong gf$ and $\beta \colon fg \cong \id_B$ in the homotopy 2-category. + \item\label{itm:htpy-equiv} There exists a functor $g \colon B \to A$ and maps + \[ + \begin{tikzcd} & A & & & B \\ A \arrow[ur, equals] \arrow[dr, "gf"'] \arrow[r, "\alpha"] & A^\iso \arrow[u, two heads, "\sim", "\ev_0"'] \arrow[d, two heads, "\sim"', "\ev_1"] &\text{and} & B \arrow[dr, equals] \arrow[r, "\beta"] \arrow[ur, "fg"] & B^\iso \arrow[u, two heads, "\sim", "\ev_0"'] \arrow[d, two heads, "\sim"', "\ev_1"] \\ & A & & & B + \end{tikzcd} + \] in the $\infty$-cosmos $\cK$. + \end{enumerate} + \end{thm} + + As an illustrative comparison of 2-categorical and quasi-categorical techniques, rather than appealing to Lemma \ref{lem:equiv-htpy-equiv} to prove \ref{itm:rep-equiv}$\Leftrightarrow$\ref{itm:htpy-equiv}, we re-prove it. + \begin{proof} + For \ref{itm:rep-equiv}$\To$\ref{itm:2cat-equiv}, if the induced map $f_* \colon \Fun(X,A) \we \Fun(X,B)$ defines an equivalence of quasi-categories then the functor $f_* \colon \hFun(X,A) \we \hFun(X,B)$ defines an equivalence of categories, by Remark \ref{rmk:qcat-htpy-cat-equiv}. In particular, the equialence $f_* \colon \hFun(B,A) \we \hFun(B,B)$ is essentially surjective so there exists $g \in \hFun(B,A)$ and an isomorphism $\beta \colon fg \cong \id_B \in \hFun(B,B)$. Now since $f_* \colon \hFun(A,A) \we \hFun(A,B)$ is fully faithful, the isomorphism $\beta f \colon fgf \cong f \in \hFun(A,B)$ can be lifted to define an isomorphism $\alpha^{-1} \colon gf \cong \id_A \in \hFun(A,A)$. This defines the data of a 2-categorical equivalence in Definition \ref{defn:2-cat-equiv}. + + To see that \ref{itm:2cat-equiv}$\To$\ref{itm:htpy-equiv} recall from Lemma \ref{lem:invertible-2-cell} that the natural isomorphisms $\alpha \colon \id_A \cong gf$ and $\beta \colon fg \cong \id_B$ in $\h\cK$ are represented by maps $\alpha \colon A \to A^\iso$ and $\beta \colon B \to B^\iso$ in $\cK$ as in \eqref{eq:htpy-equiv}. + + Finally, \ref{itm:htpy-equiv}$\To$\ref{itm:rep-equiv} since $\Fun(X,-)$ carries the data of \ref{itm:htpy-equiv} to the data of an equivalence of quasi-categories as in Definition \ref{defn:qcat-equiv}. + \end{proof} + + It is hard to overstate the importance of Theorem \ref{thm:equiv-are-equiv} for the work that follows. The categorical constructions that we introduce for $\infty$-categories, $\infty$-func\-tors, and $\infty$-natural transformations are invariant under 2-cat\-e\-go\-ri\-cal equivalence in the homotopy 2-category and the universal properties we develop similarly characterize 2-categorical equivalence classes of $\infty$-cat\-e\-go\-ries. Theorem \ref{thm:equiv-are-equiv} then asserts that such constructions are ``homotopically correct'': both invariant under equivalence in the $\infty$-cosmos and precisely identifying equivalence classes of objects. + + + The equivalence invariance of the functor space in the codomain variable is axiomatic, but equivalence invariance in the domain variable is not.\footnote{The functor $\Fun(A,-)$ is a \emph{cosmological functor}, preserving all of the structure of Definition \ref{defn:cosmos}. Cosmological functors then preserve a large class of cosmological notions, including equivalences. These results, however, %Lemma \ref{lem:cosmoi-functors-pres-equiv} does + do not apply to $\Fun(-,B)$ since this functor is not cosmological.} Nor is it evident how this could be proven from either \ref{itm:rep-equiv} or \ref{itm:htpy-equiv} of Theorem \ref{thm:equiv-are-equiv}. But using \ref{itm:2cat-equiv} and 2-categorical techniques, there is now a short proof. + + \begin{cor}\label{cor:equiv-invar-fun} Equivalences of $\infty$-categories $A' \we A$ and $B \we B'$ induce an equivalence of functor spaces $\Fun(A,B) \we \Fun(A',B')$. + \end{cor} + \begin{proof} + The representable simplicial functors $\Fun(A,-)\colon \cK \to \qCat$ and $\Fun(-,B)\colon \cK\op \to \qCat$ induce 2-functors $\Fun(A,-)\colon\h\cK\to\h\qCat$ and $\Fun(-,B)\colon\h\cK\op\to\h\qCat$, which preserve the 2-cat\-e\-go\-ri\-cal equivalences of Definition \ref{defn:2-cat-equiv}. By Theorem \ref{thm:equiv-are-equiv} this is what we wanted to show. + \end{proof} + + There is also a standard 2-categorical notion of an isofibration, defined in the statement of Proposition \ref{prop:isofib-define-isofib}. %and elaborated upon in Definition \ref{defn:2cat-isofibration}. + We now show that any isofibration in an $\infty$-cosmos defines an isofibration in its homotopy 2-category. + + \begin{prop}[isofibrations are isofibrations]\label{prop:isofib-define-isofib} An isofibration $p \colon E \fib B$ in an $\infty$-cosmos $\cK$ also defines an \textbf{isofibration} in the homotopy 2-category $\h\cK$: given any invertible 2-cell as displayed below-left abutting to $B$ with a specified lift of one of its boundary 1-cells through $p$, there exists an invertible 2-cell abutting to $E$ with this boundary 1-cell as displayed below-right that whiskers with $p$ to the original 2-cell. + \[ + \begin{tikzcd} X \arrow[r, "e"] \arrow[dr, bend right, "b"'] & E \arrow[d, two heads, "p"] \arrow[dl, phantom, "{\scriptstyle\cong\Downarrow\beta}" near start] &\arrow[d, phantom, "="] & X \arrow[rr, start anchor=15, end anchor=165, bend left=20, "e"] \arrow[rr, start anchor=345, end anchor=195, bend right=20, "\bar{e}"', dashed] \arrow[rr, phantom, "{\scriptstyle\cong\Downarrow\gamma}"] && E \arrow[d, two heads, "p"] \\ ~ & B & ~ & & & B + \end{tikzcd} + \] + \end{prop} + \begin{proof} The universal property of the statement says that the functor \[p_* \colon \hFun(X,E) \fib \hFun(X,B)\] is an isofibration of categories in the sense defined in Proposition \ref{prop:cat-cosmos}. By axiom \ref{defn:cosmos}\ref{itm:cosmos-isofib}, since $p \colon E \fib B$ is an isofibration in $\cK$, the induced map $p_* \colon \Fun(X,E) \fib \Fun(X,B)$ is an isofibration of quasi-categories. So it suffices to show that the functor $\ho \colon \qCat\to \Cat$ carries isofibrations of quasi-categories to isofibrations of categories. + + So let us now consider an isofibration $p \colon E \fib B$ between quasi-categories. By Corollary \ref{cor:coherent-iso}, every isomorphism $\beta$ in the homotopy category $\ho{B}$ of the quasi-category $B$ is represented by a simplicial map $\beta \colon \iso \to B$. By Definition \ref{defn:qcat-isofibration}, the lifting problem + \[ + \begin{tikzcd} + \catone \arrow[r, "e"] \arrow[d, hook] & E \arrow[d, two heads, "p"] \\ \iso \arrow[ur, dashed, "\gamma"] \arrow[r, "\beta"'] & B + \end{tikzcd} + \] + can be solved, and the map $\gamma \colon \iso \to E$ so produced represents a lift of the isomorphism from $\ho{B}$ to an isomorphism in $\ho{E}$ with domain $e$. + \end{proof} + + \begin{con}[on isofibrations in homotopy 2-categories] Since the converse to Proposition \ref{prop:isofib-define-isofib} does not hold, there is a potential ambiguity when using the term ``isofibration'' to refer to a map in the homotopy 2-category of an $\infty$-cosmos. We adopt the convention that when we declare a map in $\h\cK$ to be an isofibration we always mean this is the stronger sense of defining an isofibration in $\cK$. This stronger condition gives us access to the 2-categorical lifting property of Proposition \ref{prop:isofib-define-isofib} and also to homotopical properties axiomatized in Definition \ref{defn:cosmos}, which ensure that the strictly defined limits of \ref{defn:cosmos}\ref{itm:cosmos-limits} are automatically equivalence invariant constructions (see \cite[6.2.8,\S C.1]{RiehlVerity:2022eo}). %\S\ref{sec:fib-obj} and Proposition \ref{prop:flexible-homotopical}). + \end{con} + + We conclude this chapter with a final definition that can be extracted from the homotopy 2-category of an $\infty$-cosmos. The 1- and 2-cells in the homotopy 2-category from the terminal $\infty$-category $1 \in \cK$ to a generic $\infty$-category $A \in \cK$ define the objects and morphisms in the homotopy category of the $\infty$-category $A$. + + \begin{defn}[homotopy category of an $\infty$-category]\label{defn:htpy-cat-of-infinity-cat} The \textbf{homotopy category} of an $\infty$-category $A$ in an $\infty$-cosmos $\cK$ is defined to be the homotopy category of its underlying quasi-category, that is: + \[ \ho A \coloneq \hFun(1,A) \coloneq \ho(\Fun(1,A)).\] + \end{defn} + + As we shall discover, homotopy categories generally inherit ``derived'' analogues of structures present at the level of $\infty$-categories. %An early example of this appears in Proposition \ref{prop:induced-adjunctions}\ref{itm:adj-htpy-cat}. diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex index 3847bc8..74589ba 100644 --- a/blueprint/src/macros/common.tex +++ b/blueprint/src/macros/common.tex @@ -39,16 +39,37 @@ %enriched (i.e. all large) categories. \newcommand{\ec}[1]{{\mathord{\mathcal{#1}}}} \newcommand{\cA}{\ec{A}} +\newcommand{\cC}{\ec{C}} +\newcommand{\cD}{\ec{D}} \newcommand{\cK}{\ec{K}} +\newcommand{\cL}{\ec{L}} +\newcommand{\cV}{\ec{V}} +\newcommand{\cW}{\ec{W}} \newcommand{\Cat}{\ec{Cat}} +\newcommand{\Kan}{\ec{Kan}} \newcommand{\qCat}{\ec{QCat}} +\newcommand{\Set}{\ec{Set}} \newcommand{\sSet}{\ec{sSet}} - -\newcommand{\Del}{\mbfDelta} +\newcommand{\twoCat}{2\text{-}\Cat} +\newcommand{\sCat}{\sSet\text{-}\Cat} +\newcommand{\eCat}[1]{{#1}\text{-}\Cat}%for enriched categories % Various hom notations. \newcommand{\qop}[1]{{\mathord{\mathsf{#1}}}} \newcommand{\Fun}{\qop{Fun}}%mapping spaces in cosmoi +\newcommand{\ho}{\qop{h}} +\newcommand{\hFun}{\qop{hFun}}%hom categories in homotopy 2-categories +\newcommand{\core}{\qop{core}}%not cosmological +\newcommand{\coreop}[1]{{{#1}^\simeq}}%for core as an operator + +\newcommand{\catfour}{{\Bbbfour}}%texdoc unimath-symbols.pdf +\newcommand{\catthree}{{\Bbbthree}}%texdoc unimath-symbols.pdf +\newcommand{\cattwo}{{\Bbbtwo}} +\newcommand{\catone}{{\Bbbone}} +\newcommand{\catn}{{\mathbb{n}}} +\newcommand{\catnone}{{\catn\!+\!\catone}} +\newcommand{\catntwo}{{\catn\!+\!\cattwo}} +\newcommand{\iso}{{\BbbI}} %arrows; cheap version of \we and \trvfib \makeatletter @@ -68,17 +89,42 @@ \newcommand{\fib}{\twoheadrightarrow} \newcommand{\we}{\xrightarrow{{\smash{\mathlower{0.8}{\sim}}}}} \newcommand{\trvfib}{\dhxrightarrow{{\smash{\mathlower{0.8}{\sim}}}}} +\newcommand{\To}{\Rightarrow}%2-cells +\newcommand{\isoto}{\xrightarrow{{\smash{\mathlower{0.8}{\cong}}}}} +\newcommand{\inc}{\hookrightarrow} + +%1-cells induced from 2-cells +\newcommand{\name}[1]{{\ulcorner{#1}\urcorner}} + % Elementary operators in the theory of (stratified) simplicial sets. \newcommand{\face}{\delta} \newcommand{\degen}{\sigma} +\newcommand{\fbv}[1]{\{{#1}\}} + % Duals / Superscripted postfix ops -\newcommand{\op}{^{\mathord{\text{\rm op}}}} -\newcommand{\co}{^{\mathord{\text{\rm co}}}} -\newcommand{\coop}{^{\mathord{\text{\rm coop}}}} +\newcommand{\op}{^{\mathord{\textup{op}}}} +\newcommand{\co}{^{\mathord{\textup{co}}}} +\newcommand{\coop}{^{\mathord{\textup{coop}}}} % General operations on maps etc. +\newcommand{\cosk}{\textup{cosk}} +\newcommand{\cod}{\textup{cod}} +\newcommand{\dom}{\textup{dom}} +\newcommand{\ev}{\textup{ev}} \newcommand{\id}{\textup{id}} +\newcommand{\sk}{\textup{sk}} + + +%###trial notation for the homotopy 2-category +\newcommand{\h}{\mathfrak{h}} + +% Leibniz... +% ... for binary operators like join and product +\newcommand{\leib}[1]{\mathbin{\widehat{#1}}} +% ... for prefix operators like lim, colim and decalage. +\newcommand{\uleib}[1]{\widehat{#1}} +\newcommand{\pwr}{\pitchfork} diff --git a/blueprint/src/macros/print.tex b/blueprint/src/macros/print.tex index 668fec1..1d05a10 100644 --- a/blueprint/src/macros/print.tex +++ b/blueprint/src/macros/print.tex @@ -26,4 +26,7 @@ \NewDocumentCommand{\proves}{m} {\clist_map_inline:nn{#1}{\vphantom{\ref{##1}}}% \ignorespaces} -\ExplSyntaxOff \ No newline at end of file +\ExplSyntaxOff + +% +\newcommand{\Del}{\mbfDelta} diff --git a/blueprint/src/macros/web.tex b/blueprint/src/macros/web.tex index ceee975..8f8df0b 100644 --- a/blueprint/src/macros/web.tex +++ b/blueprint/src/macros/web.tex @@ -2,4 +2,6 @@ % the web version. Of course they should have a corresponding % version in macros/print.tex. % Typically the printed version could have more fancy decorations. -% This will probably be a very short file. \ No newline at end of file +% This will probably be a very short file. + +\newcommand{\Del}{\Delta} diff --git a/blueprint/src/print.pdf b/blueprint/src/print.pdf index b7bd6ba..ccf28a8 100644 Binary files a/blueprint/src/print.pdf and b/blueprint/src/print.pdf differ diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index cc06987..227a534 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -10,7 +10,7 @@ % It is otherwise a very minimal preamble (you should probably at least % add cleveref and tikz-cd). -\documentclass{amsart} +\documentclass{amsbook} \usepackage{geometry} @@ -24,7 +24,7 @@ \input{macros/common} \input{macros/print} -\title{\texorpdfstring{$\infty$}{Infinity}-Cosmoi} +\title{\texorpdfstring{$\infty$}{Infinity}-Cosmoi for Lean} \author{Emily Riehl} \author{Dominic Verity}