1.3 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.

Definition 1.3.1 simplicial categories as enriched categories

✓

The data of a simplicial category is a simplicially enriched category with a set of objects and a simplicial set ${\mathord {\mathcal{A}}}(x,y)$ of morphisms between each ordered pair of objects. Each endo-hom space contains a distinguished 0-simplex $\textup{id}_x \in {\mathord {\mathcal{A}}}(x,y)_0$, and composition is required to define a simplicial map

$\begin{tikzcd} \cA(y,z) \times \cA(x,y) \arrow[r, "\circ"] & \cA(x,z) \end{tikzcd}$

The composition is required to be associative and unital, in a sense expressed by the commutative diagrams of simplicial sets

$\begin{tikzcd} [column sep=small] \cA(y,z) \times \cA(x,y) \times \cA(w,x) \arrow[d, "\id \times \circ"'] \arrow[r, "\circ \times \id"] & \cA(x,z) \times \cA(w,x) \arrow[d, "\circ"] \\ \cA(y,z) \times \cA(w,y) \arrow[r, "\circ"'] & \cA(w,z) \end{tikzcd}$

$\begin{tikzcd} \cA(x,y) \arrow[r, "\id_y \times \id"] \arrow[dr, "\id"] \arrow[d, "\id \times \id_x"'] & \cA(y,y) \times \cA(x,y) \arrow[d, "\circ"] \\ \cA(x,y) \times \cA(x,x) \arrow[r, "\circ"'] & \cA(x,y) \end{tikzcd}$

Definition 1.3.2

For each $n \geq 0$, an $n$-simplex in ${\mathord {\mathcal{A}}}(x,y)$ is referred to as an $n$-arrow from $x$ to $y$.

Lemma 1.3.3

For any simplicial category ${\mathord {\mathcal{A}}}$ and $n \geq 0$, the $n$-arrows assemble into the arrows of an ordinary category ${\mathord {\mathcal{A}}}_n$ with the same set of objects as ${\mathord {\mathcal{A}}}$.

Proof ▶

The category of $n$-arrows is easy to construct directly. Alternatively, this result can be proven by applying the theory of change-of-base of §1.5 to the functor $\textup{ev}_n \colon {\mathord {\mathcal{sSet}}}\to {\mathord {\mathcal{Set}}}$.

In particular, the underlying category of a simplicial category can be identified with the category of $0$-arrows. Below we link the general Mathlib construction of the underlying category of an enriched category, though it might be useful to formalize a lemma characterizing it in the way stated here.

Definition 1.3.4

✓

The category ${\mathord {\mathcal{A}}}_0$ of 0-arrows is the underlying category of the simplicial category ${\mathord {\mathcal{A}}}$, which forgets the higher dimensional simplicial structure.

There is alternate presentation of the data of a simplicial category as a simplicial object in the category of categories and identity-on-objects functors. ¹

Digression 1.3.5 simplicial categories as simplicial objects

A simplicial category ${\mathord {\mathcal{A}}}$ is equivalently given by categories ${\mathord {\mathcal{A}}}_n$, with a common set of objects and whose arrows are called $n$-arrows, that assemble into a diagram $\Delta ^{\mathord {\textup{op}}}\to {\mathord {\mathcal{Cat}}}$ of identity-on-objects functors

$\begin{tikzcd} [column sep=large] \cdots \cA_3 \arrow[r, shift right=2.25em, "\cdot\face^0" description, pos=.35] \arrow[r, shift right=.75em, "\cdot\face^1" description, pos=.35] \arrow[r, shift left=.75em, "\cdot\face^2" description, pos=.35] \arrow[r, shift left=2.25em, "\cdot\face^3" description, pos=.35]& \cA_2 \arrow[l, "\cdot\degen^1" description, pos=.35] \arrow[l, shift left=1.5em, "\cdot\degen^0" description, pos=.35] \arrow[l, shift right=1.5em, "\cdot\degen^2" description, pos=.35] \arrow[r, "\cdot\face^1" description, pos=.35] \arrow[r, shift left=1.5em, "\cdot\face^2" description, pos=.35] \arrow[r, shift right=1.5em, "\cdot\face^0" description, pos=.35] & \cA_1 \arrow[l, shift left=.75em, "\cdot\degen^0" description, pos=.35] \arrow[l, shift right=.75em, "\cdot\degen^1" description, pos=.35] \arrow[r, shift left=.75em, "\cdot\face^1" description, pos=.35] \arrow[r, shift right=.75em, "\cdot\face^0" description, pos=.35] & \cA_0 \arrow[l, "\cdot\degen^0" description, pos=.35] \end{tikzcd}$

$\eqcolon {\mathord {\mathcal{A}}}$

By contrast, the notion of simplicially enriched limit remains to be formalized. Fortunately, we do not (immediately) require the general notion of weighted limits, as the notion of an $\infty $-cosmos only requires two special cases: cotensors and conical limits.

Definition 1.3.6 simplicial cotensors

✓

Let ${\mathord {\mathcal{A}}}$ be a simplicial category. The cotensor of an object $A \in {\mathord {\mathcal{A}}}$ by a simplicial set $U$ is given by the data of an object $A^U \in {\mathord {\mathcal{A}}}$ together with a cone $U \to {\mathord {\mathcal{A}}}(A^U,A)$ so that the induced map defines an isomorphism of simplicial sets:

\begin{equation} \label{eq:cotensor-defn} {\mathord {\mathcal{A}}}(X,A^U) \cong {\mathord {\mathcal{A}}}(X,A)^U \end{equation}

1.3.1

Note by construction the isomorphism 1.3.1 is automatically simplicially natural in $X$. This simplicial naturality is an important aspect of the enriched universal property.

Definition 1.3.7 simplicial cotensors

✓

A simplicial category ${\mathord {\mathcal{A}}}$ has cotensors when all cotensors exist.

Lemma 1.3.8

When a simplicial category has cotensors, cotensors are associative: given $A \in {\mathord {\mathcal{A}}}$ and simplicial sets $U$ and $V$ there are canonical isomorphisms

\[ (A^U)^V \cong A^{U \times V} \cong (A^V)^U. \]

Proof ▶

By the enriched Yoneda lemma, these objects represent the same simplicial functors ${\mathord {\mathcal{A}}}^{\mathord {\textup{op}}}\to {\mathord {\mathcal{sSet}}}$.

Lemma 1.3.9

Assuming such objects exist, the simplicial cotensor defines a bifunctor

$\begin{tikzcd} [row sep=tiny] s\mathcal{S}et\op \times \cA \arrow[r] & \cA \\ (U,A) \arrow[r, maps to] & A^U \end{tikzcd}$

in a unique way making the isomorphism 1.3.1 natural in $U$ and $A$ as well.

Proof ▶

Functoriality in each variable follows from the universal property.

The other simplicial limit notions postulated by axiom 1.4.1 i are conical, which is the term used for ordinary 1-categorical limit shapes that satisfy an enriched analog of the usual universal property. Such limits also define limits in the underlying category, but the usual universal property is strengthened.

Definition 1.3.10 simplicial conical limits

✓

Consider a limit cone $(\lim _{j \in J}A_j \to A_j)_{j \in J}$ in the underlying category ${\mathord {\mathcal{A}}}_0$ of a simplicially-enriched category ${\mathord {\mathcal{A}}}$. By applying the covariant representable functor ${\mathord {\mathcal{A}}}(X,-) \colon {\mathord {\mathcal{A}}}_0 \to {\mathord {\mathcal{sSet}}}$ to a limit cone $(\lim _{j \in J}A_j \to A_j)_{j \in J}$ in ${\mathord {\mathcal{A}}}_0$, we obtain a natural comparison map

\begin{equation} \label{eq:simplicial-limit-map} {\mathord {\mathcal{A}}}(X,\lim _{j \in J}A_j) \to \lim _{j \in J}{\mathord {\mathcal{A}}}(X,A_j). \end{equation}

1.3.2

We say that $\lim _{j\in J}A_j$ defines a simplicially enriched limit if and only if 1.3.2 is an isomorphism of simplicial sets for all $X \in {\mathord {\mathcal{A}}}$.

Remark 1.3.11

The notion of cotensors and conical limits could be introduced for categories enriched over arbitrary cartesian monoidal categories or more generally for categories enriched over symmetric monoidal categories. This might be worth doing as a service to the broader Mathlib.