# The Stacks Project

## Tag 017N

Lemma 14.17.5. Assume the category $\mathcal{C}$ has coproducts of any two objects and finite limits. Let $a : U \to V$, $b : U \to W$ be morphisms of simplicial sets. Assume $U_n, V_n, W_n$ finite nonempty for all $n \geq 0$. Assume that all $n$-simplices of $U, V, W$ are degenerate for all $n \gg 0$. Let $T$ be a simplicial object of $\mathcal{C}$. Then $$\mathop{\mathrm{Hom}}\nolimits(V, T) \times_{\mathop{\mathrm{Hom}}\nolimits(U, T)} \mathop{\mathrm{Hom}}\nolimits(W, T) = \mathop{\mathrm{Hom}}\nolimits(V \amalg_U W, T)$$ In other words, the fibre product on the left hand side is represented by the Hom object on the right hand side.

Proof. By Lemma 14.17.4 all the required $\mathop{\mathrm{Hom}}\nolimits$ objects exist and satisfy the correct functorial properties. Now we can identify the $n$th term on the left hand side as the object representing the functor that associates to $X$ the first set of the following sequence of functorial equalities \begin{align*} & \mathop{Mor}\nolimits(X \times \Delta[n], \mathop{\mathrm{Hom}}\nolimits(V, T) \times_{\mathop{\mathrm{Hom}}\nolimits(U, T)} \mathop{\mathrm{Hom}}\nolimits(W, T)) \\ & = \mathop{Mor}\nolimits(X \times \Delta[n], \mathop{\mathrm{Hom}}\nolimits(V, T)) \times_{\mathop{Mor}\nolimits(X \times \Delta[n], \mathop{\mathrm{Hom}}\nolimits(U, T))} \mathop{Mor}\nolimits(X \times \Delta[n], \mathop{\mathrm{Hom}}\nolimits(W, T)) \\ & = \mathop{Mor}\nolimits(X \times \Delta[n] \times V, T) \times_{\mathop{Mor}\nolimits(X \times \Delta[n] \times U, T)} \mathop{Mor}\nolimits(X \times \Delta[n] \times W, T) \\ & = \mathop{Mor}\nolimits(X \times \Delta[n] \times (V \amalg_U W), T)) \end{align*} Here we have used the fact that $$(X \times \Delta[n] \times V) \times_{X \times \Delta[n] \times U} (X \times \Delta[n] \times W) = X \times \Delta[n] \times (V \amalg_U W)$$ which is easy to verify term by term. The result of the lemma follows as the last term in the displayed sequence of equalities corresponds to $\mathop{\mathrm{Hom}}\nolimits(V \amalg_U W, T)_n$. $\square$

The code snippet corresponding to this tag is a part of the file simplicial.tex and is located in lines 1674–1692 (see updates for more information).

\begin{lemma}
\label{lemma-hom-from-coprod}
Assume the category $\mathcal{C}$
has coproducts of any two objects and finite
limits. Let $a : U \to V$, $b : U \to W$
be morphisms of simplicial sets.
Assume $U_n, V_n, W_n$ finite nonempty for all $n \geq 0$.
Assume that all $n$-simplices of $U, V, W$
are degenerate for all $n \gg 0$.
Let $T$ be a simplicial object of $\mathcal{C}$.
Then
$$\Hom(V, T) \times_{\Hom(U, T)} \Hom(W, T) = \Hom(V \amalg_U W, T)$$
In other words, the fibre product on the left hand
side is represented by the Hom object on the right hand side.
\end{lemma}

\begin{proof}
By Lemma \ref{lemma-exists-hom-from-simplicial-set-finite}
all the required $\Hom$ objects exist and satisfy the
correct functorial properties. Now we can identify
the $n$th term on the left hand side as the object
representing the functor that associates to $X$
the first set of the following sequence of functorial
equalities
\begin{align*}
&
\Mor(X \times \Delta[n],
\Hom(V, T) \times_{\Hom(U, T)} \Hom(W, T)) \\
& =
\Mor(X \times \Delta[n], \Hom(V, T))
\times_{\Mor(X \times \Delta[n], \Hom(U, T))}
\Mor(X \times \Delta[n], \Hom(W, T)) \\
& =
\Mor(X \times \Delta[n] \times V, T)
\times_{\Mor(X \times \Delta[n] \times U, T)}
\Mor(X \times \Delta[n] \times W, T) \\
& =
\Mor(X \times \Delta[n] \times (V \amalg_U W), T))
\end{align*}
Here we have used the fact that
$$(X \times \Delta[n] \times V) \times_{X \times \Delta[n] \times U} (X \times \Delta[n] \times W) = X \times \Delta[n] \times (V \amalg_U W)$$
which is easy to verify term by term. The result of the lemma
follows as the last term in the displayed sequence of
equalities corresponds to $\Hom(V \amalg_U W, T)_n$.
\end{proof}

There are no comments yet for this tag.

## Add a comment on tag 017N

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 lower-right corner).