Lemma 14.20.3. Let $\mathcal{C}$ be a category with fibred products. Let $f : Y\to X$ be a morphism of $\mathcal{C}$. Let $U$ be the simplicial object of $\mathcal{C}$ whose $n$th term is the $(n + 1)$fold fibred product $Y \times _ X Y \times _ X \ldots \times _ X Y$. See Example 14.3.5. For any simplicial object $V$ of $\mathcal{C}$ we have

\begin{align*} \mathop{\mathrm{Mor}}\nolimits _{\text{Simp}(\mathcal{C})}(V, U) & = \mathop{\mathrm{Mor}}\nolimits _{\text{Simp}_1(\mathcal{C})}(\text{sk}_1 V, \text{sk}_1 U) \\ & = \{ g_0 : V_0 \to Y \mid f \circ g_0 \circ d^1_0 = f \circ g_0 \circ d^1_1\} \end{align*}

In particular we have $U = \text{cosk}_1 \text{sk}_1 U$.

Proof. Suppose that $g : \text{sk}_1V \to \text{sk}_1U$ is a morphism of $1$-truncated simplicial objects. Then the diagram

$\xymatrix{ V_1 \ar@<1ex>[r]^{d^1_0} \ar@<-1ex>[r]_{d^1_1} \ar[d]_{g_1} & V_0 \ar[d]^{g_0} \\ Y \times _ X Y \ar@<1ex>[r]^{pr_1} \ar@<-1ex>[r]_{pr_0} & Y \ar[r] & X }$

is commutative, which proves that the relation shown in the lemma holds. We have to show that, conversely, given a morphism $g_0$ satisfying the relation $f \circ g_0 \circ d^1_0 = f \circ g_0 \circ d^1_1$ we get a unique morphism of simplicial objects $g : V \to U$. This is done as follows. For any $n \geq 1$ let $g_{n, i} = g_0 \circ V([0] \to [n], 0 \mapsto i) : V_ n \to Y$. The equality above implies that $f \circ g_{n, i} = f \circ g_{n, i + 1}$ because of the commutative diagram

$\xymatrix{ [0] \ar[rd]_{0 \mapsto 0} \ar[rrrrrd]^{0 \mapsto i} \\ & [1] \ar[rrrr]^{0 \mapsto i, 1\mapsto i + 1} & & & & [n] \\ [0] \ar[ru]^{0 \mapsto 1} \ar[rrrrru]_{0 \mapsto i + 1} }$

Hence we get $(g_{n, 0}, \ldots , g_{n, n}) : V_ n \to Y \times _ X\ldots \times _ X Y = U_ n$. We leave it to the reader to see that this is a morphism of simplicial objects. The last assertion of the lemma is equivalent to the first equality in the displayed formula of the lemma. $\square$

Comment #1019 by correction_bot on

Being a robot, I noticed that in the statement of the lemma, $\text{Simp}_{\leq 1}(\mathcal{C})$ appears but should be $\text{Simp}_{1}(\mathcal{C})$ to be consistent with the notation introduced earlier.

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).