1.2 Simplicial sets

Before introducing an axiomatic framework that allows us to develop $\infty $-category theory in general, we first consider one model in particular: quasi-categories, which were introduced in 1973 by Boardman and Vogt [ BV73 ] in their study of homotopy coherent diagrams. Ordinary 1-categories give examples of quasi-categories via the construction of Definition 1.2.15. Joyal first undertook the task of extending 1-category theory to quasi-category theory in [ Joy02 ] and [ Joy08 ] and in several unpublished draft book manuscripts. The majority of the results in this section are due to him.

Definition 1.2.1 the simplex category

✓

Let $\Delta $ denote the simplex category of finite nonempty ordinals $[n] = \{ 0 {\lt}1 {\lt}\cdots {\lt} n\} $ and order-preserving maps.

The maps in the simplex category include in particular:

Definition 1.2.2 elementary face maps

✓

The elementary face operators are the maps

$\begin{tikzcd} [row sep=tiny, column sep=small] {[n-1]} \arrow[r, tail, "{\face^i}"] & {[n]} & {0 \leq i \leq n} \end{tikzcd}$

whose images omit the element $i \in [n]$.

Definition 1.2.3 elementary degeneracy maps

✓

The elementary degeneracy operators are the maps

$\begin{tikzcd} [row sep=tiny, column sep=small] {[n+1]} \arrow[r, two heads, "{\degen^i}"] & {[n]} & {0 \leq i \leq n } \end{tikzcd}$

whose images double up on the element $i \in [n]$.

The following decomposition result is yet to be proven, though there are related results on the image factorization in the simplex category:

Proposition 1.2.4

Every morphism in $\Delta $ factors uniquely as an epimorphism followed by a monomorphism; these epimorphisms, the degeneracy operators, decompose as composites of elementary degeneracy operators, while the monomorphisms, the face operators, decompose as composites of elementary face operators.

Proof ▶

The image factorizations have been formalized but the canonical decompositions into elementary face and degeneracy operators remain to be done.

Definition 1.2.5 simplicial set

✓

A simplicial set is a presheaf on the simplex category.

Definition 1.2.6 the category of simplicial sets

✓

The category of simplicial sets is the category ${\mathord {\mathcal{sSet}}}:={\mathord {\mathcal{Set}}}^{\Delta ^{\mathord {\textup{op}}}}$ of presheaves on the simplex category.

Standard examples of simplicial sets include:

Definition 1.2.7 standard simplex

✓

We write $\Delta [n]$ for the standard $n$-simplex the simplicial set represented by $[n] \in \Delta $.

Definition 1.2.8 simplex boundary

✓

We write $\partial \Delta [n] \subset \Delta [n]$ for the boundary sphere of the $n$-simplex. The sphere $\partial \Delta [n]$ is the simplicial subset generated by the codimension-one faces of the $n$-simplex.

Definition 1.2.9 simplicial horn

✓

We write $\Lambda ^k[n] \subset \Delta [n]$ for the $k$-horn in the $n$-simplex. The horn $\Lambda ^k[n]$ is the further simplicial subset of $\partial \Delta [n]$ that omits the face opposite the vertex $k$, but it is defined as a subset of $\Delta [n]$.

Given a simplicial set $X$, it is conventional to write $X_n$ for the set of $n$-simplices, defined by evaluating at $[n] \in \Delta $. This is implemented as a scoped notation “_[n]” accessible with “open Simplicial” or “open scoped Simplicial.”

By the Yoneda lemma:

Lemma 1.2.10

✓

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 \delta ^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}$

Proof ▶

This is a special case of the Yoneda lemma.

The right action of the face operator defines a map $X_n \xrightarrow {\cdot \delta ^i} X_{n-1}$. Geometrically, $x\cdot \delta ^i$ is the “face opposite the vertex $i$” in the $n$-simplex $x$.

The category of simplicial sets, as a presheaf category, is very well-behaved:

Corollary 1.2.11

✓

The category of simplicial sets is complete.

Proof ▶

Presheaf categories are complete.

Corollary 1.2.12

✓

The category of simplicial sets is cocomplete.

Proof ▶

Presheaf categories are cocomplete.

Instances of these facts currently appear in Mathlib, which likely also knows that the category of simplicial sets is cartesian closed.

The definition of a quasi-category can be found in Mathlib as well.

Definition 1.2.13 quasi-category

✓

A quasi-category is a simplicial set $A$ in which any inner horn can be extended to a simplex, solving the displayed lifting problem:

$\begin{tikzcd} \Lambda^k[n] \arrow[r] \arrow[d, hook] & A \\ \Delta[n] \arrow[ur, dashed] \end{tikzcd}$

for n ≥2, 0 < k < n.

Quasi-categories were first introduced by Boardman and Vogt [ BV73 ] under the name “weak Kan complexes,” as they generalize the following notion:

Definition 1.2.14 Kan complex

✓

A Kan complex is a simplicial set admitting extensions as in 1.2.13 along all horn inclusions $n \geq 1, 0 \leq k \leq n$.

Since any topological space can be encoded as a Kan complex, ¹ in this way spaces provide examples of quasi-categories.

Categories also provide examples of quasi-categories via the nerve construction.

Definition 1.2.15 nerve

✓

The category ${\mathord {\mathcal{Cat}}}$ of 1-categories embeds fully faithfully into the category of simplicial sets via the 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 $[n]\to C$ from the ordinal category $[n]$ with objects $0,\ldots , n$ and a unique arrow $i \to j$ just when $i \leq j$.

Definition 1.2.16 nerve functor

✓

The map $[n] \mapsto [n]$ defines a fully faithful embedding $\Delta \hookrightarrow {\mathord {\mathcal{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.”

Proposition 1.2.17

✓

The nerve of a category $C$ is 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. ²

Proof ▶

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 spine, the 1-skeletal simplicial subset formed by the edges connecting adjacent vertices. In fact, as suggested by the proof of Proposition 1.2.18, any simplicial set in which inner horns admit unique fillers is isomorphic to the nerve of a 1-category. This characterization of nerves is not yet in Mathlib, however, we have proven the one-way result, namely that nerves of categories satisfy the “strict Segal condition” and this is used in the proof of 2-coskeletality.

In the book that is the primary source this text [ RV22 ] , as in much of the $\infty $-categories literature, 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 $[n]$, and we frequently adopt the latter notation — writing $[0]:=\Delta [0]$, $[1]:=\Delta [1]$, $[2]:=\Delta [2]$, and so on — to suggest the correct categorical intuition. However, Mathlib notates nerves explicitly, so at some point this document should be adapted to follow that convention.

To begin down this path, we must first verify the implicit assertion that has just been made. A proof of the following result, due to Johan Commelin, will appear in Mathlib soon (see Wombat.lean for now).

Proposition 1.2.18 nerves are quasi-categories

Nerves of categories are quasi-categories.

This is not the proof that was formalized but we include it for fun:

Proof ▶

Via the isomorphism $C \cong \textup{cosk}_2C$ from Proposition 1.2.17 and the associated adjunction $\textup{sk}_2 \dashv \textup{cosk}_2$ of, 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 $\textup{sk}_2$ replaces a simplicial set by its 2-skeleton, the simplicial subset generated by the simplices of dimension at most two. For $n \geq 4$, the inclusion $\textup{sk}_2\Lambda ^k[n]\hookrightarrow \textup{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.

We now turn to the homotopy category functor. The following definitions and results are not currently in Mathlib.

Definition 1.2.19 homotopy relation on 1-simplices

A parallel pair of 1-simplices $f,g$ in a simplicial set $X$ are homotopic if there exists a 2-simplex whose boundary takes either of the following forms ³

$\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}$

or if $f$ and $g$ are in the same equivalence class generated by this relation.

In a quasi-category, the relation witnessed by either of the types of 2-simplex on display in Definition 1.2.19 is an equivalence relation and these equivalence relations coincide.

Lemma 1.2.20 homotopic 1-simplices in a quasi-category

Parallel 1-simplices $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 Definition 1.2.19.

Proof ▶

A lengthy exercise in low-dimensional horn filling.

Definition 1.2.21

✓

By 1-truncating, any simplicial set $X$ has an underlying reflexive quiver or 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 \delta ^1$ (the face opposite 1) while the target is its 1st face $f \cdot \delta ^0$ (the face opposite 0).

Proposition 1.2.22

✓

The functor that carries a category to its underlying reflexive quiver has a left adjoint, defining the free category on a reflexive quiver:

$\begin{tikzcd} [column sep=huge] \mathcal{C}at \arrow[r, start anchor=353, end anchor=190, bend right, hook', "U"'] \arrow[r, phantom, "\bot"] & r\mathcal{Q}uiv \arrow[l, start anchor=170, end anchor=7, bend right, "F"' pos=.48] \end{tikzcd}$

Proof ▶

This has been formalized and is currently in the CatHasColimits branch of Mathlib.

Definition 1.2.23 the homotopy category [ GZ67 , § 2.4 ]

✓

The 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 homotopy category ${\mathord {\mathsf{h}}}{X}$ of $X$ is the quotient of the free category on its underlying reflexive directed graph by the congruence ⁴ 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}$

By soundness of the quotient construction:

Lemma 1.2.24

Homotopic 1-simplices in a simplicial set represent the same arrow in the homotopy category.

Proof ▶

This should be relatively straightforward.

Proposition 1.2.25

✓

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.

Proof ▶

This has been formalized and is currently in the CatHasColimits branch of Mathlib.

Indeed, the natural isomorphism ${\mathord {\mathsf{h}}}{C} \cong C$ forms the counit of an adjunction, embedding ${\mathord {\mathcal{Cat}}}$ as a reflective subcategory of ${\mathord {\mathcal{sSet}}}$.

Proposition 1.2.26

✓

The nerve embedding admits a left adjoint, namely the functor which sends a simplicial set to its homotopy category:

$\begin{tikzcd} [column sep=huge] \mathcal{C}at \arrow[r, start anchor=353, end anchor=190, bend right, hook'] \arrow[r, phantom, "\bot"] & s\mathcal{S}et \arrow[l, start anchor=170, end anchor=7, bend right, "\ho"' pos=.48] \end{tikzcd}$

The adjunction of Proposition 1.2.26 exists for formal reasons, via results which have already been formalized in Mathlib, once the category ${\mathord {\mathcal{Cat}}}$ is known to be cocomplete. A proof of this fact did not 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 ${\mathord {\mathcal{Cat}}}$ as a reflective subcategory of a cocomplete category (see [ Rie16 , 4.5.16 ] ). Thus, we instead formalized a direct proof.

Proof ▶

This has been formalized and is currently in the CatHasColimits branch of Mathlib.

For any simplicial set $X$, there is a natural map from $X$ to the nerve of its homotopy category ${\mathord {\mathsf{h}}}{X}$; since nerves are 2-coskeletal, it suffices to define the map $\textup{sk}_2X \to {\mathord {\mathsf{h}}}{X}$, and this is given immediately by the construction of Definition 1.2.23. Note that the quotient map $X \to {\mathord {\mathsf{h}}}{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 by direct verification of the triangle equalities.

By inspection:

Proposition 1.2.27

✓

The nerve functor is fully faithful.

Proof ▶

This has been formalized and is currently in the CatHasColimits branch of Mathlib.

As a corollary, it follows that ${\mathord {\mathcal{Cat}}}$ has colimits.

The homotopy category of a quasi-category admits a simplified description.

Lemma 1.2.28 the homotopy category of a quasi-category

If $A$ is a quasi-category then its homotopy category ${\mathord {\mathsf{h}}}{A}$ has

the set of 0-simplices $A_0$ as its objects
the set of homotopy classes of 1-simplices $A_1$ as its arrows
the identity arrow at $a \in A_0$ represented by the degenerate 1-simplex $a \cdot \sigma ^0 \in A_1$
a composition relation $h = g \circ f$ in ${\mathord {\mathsf{h}}}{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}$

Proof ▶

Another lengthy exercise in low-dimensional horn filling.

Later we will require either of the following results:

Lemma 1.2.29

$\quad $

The functor ${\mathord {\mathsf{h}}}\colon {\mathord {\mathcal{sSet}}}\to {\mathord {\mathcal{Cat}}}$ preserves finite products.
The functor ${\mathord {\mathsf{h}}}\colon {\mathord {\mathcal{QCat}}}\to {\mathord {\mathcal{Cat}}}$ preserves small products.

Proof ▶

For the first statement, preservation of the terminal object is by direct calculation. By Proposition 1.2.25, preservation of binary products is equivalent to the statement that the canonical map $N({\mathord {\mathcal{D}}}^{\mathord {\mathcal{C}}}) \to N({\mathord {\mathcal{D}}})^{N{\mathord {\mathcal{C}}}}$ involving nerves of categories is an isomorphism. On $n$-simplices, this is defined by uncurrying, which is bijection since ${\mathord {\mathcal{Cat}}}$ is cartesian closed.

For the second statement, we have a canonical comparison functor from the homotopy category of the products to the product of the homotopy categories. It follows from Lemma 1.2.28 that this is an isomorphism on underlying quivers, which suffices.

Definition 1.2.30 isomorphism in a quasi-category

A 1-simplex in a quasi-category is an isomorphism ⁵ just when it represents an isomorphism in the homotopy category. By Lemma 1.2.28 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}$

The properties of the isomorphisms in a quasi-category are somewhat technical to prove and will likely be a pain to formalize (see [ RV22 , § D ] ). Here we focus on a few essential results, which are more easily obtainable.

Definition 1.2.31

✓

The homotopy coherent isomorphism $I$, is the nerve of the free-living isomorphism.

Just as the arrows in a quasi-category $A$ are represented by simplicial maps $ [1]\to A$ whose domain is the nerve of the free-living arrow, the isomorphisms in a quasi-category can be represented by diagrams $I\to A$ whose domain is the homotopy coherent isomorphism:

Proposition 1.2.32

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}$

Remark 1.2.33

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 $I$.

Quasi-categories define the fibrant objects in a model structure due to Joyal. We use the term isofibration to refer to the fibrations between fibrant objects in this model structure, which admit the following concrete description.

Definition 1.2.34 isofibration

✓

A simplicial map $f \colon A \to B$ between quasi-categories is an 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 $I$.

$\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 “$\twoheadrightarrow $” with two heads.

We now introduce the weak equivalences and trivial fibrations between fibrant objects in the Joyal model structure.

Definition 1.2.35 equivalences of quasi-categories

A map $f \colon A \to B$ between quasi-categories is an equivalence if it extends to the data of a “homotopy equivalence” with the free-living isomorphism $I$ 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 “$\rightsquigarrow $” to decorate equivalences and $A \simeq B$ to indicate the presence of an equivalence $A \rightsquigarrow B$.

Lemma 1.2.36

If $f \colon A \to B$ is an equivalence of quasi-categories, then the functor ${\mathord {\mathsf{h}}}{f} \colon {\mathord {\mathsf{h}}}{A} \to {\mathord {\mathsf{h}}}{B}$ is an equivalence of categories, where the data displayed above defines an equivalence inverse ${\mathord {\mathsf{h}}}{g} \colon {\mathord {\mathsf{h}}}{B} \to {\mathord {\mathsf{h}}}{A}$ and natural isomorphisms encoded by the composite ⁶ 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}$

Definition 1.2.37

✓

A map $f \colon X \to Y$ between simplicial sets is a trivial fibration if it admits lifts against the boundary inclusions for all simplices

$\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}$

for n ≥0

We write “$\twoheadrightarrow $” to decorate trivial fibrations. ⁷

The notation “$\twoheadrightarrow $” is suggestive: the trivial fibrations between quasi-categories 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 [ RV22 , D.5.6 ] .