# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$

Proposition 3.1.2.7. Let $f: A_{} \hookrightarrow B_{}$ and $f': A'_{} \hookrightarrow B'_{}$ be monomorphisms of simplicial sets. If either $f$ is anodyne, then the induced map

$(A_{} \times B'_{} ) \coprod _{ A_{} \times A'_{} } ( B_{} \times A'_{} ) \hookrightarrow B_{} \times B'_{}$

is anodyne.

Proof of Proposition 3.1.2.7. Let us first regard the monomorphism $f': A'_{} \hookrightarrow B'_{}$ as fixed, and let $T$ be the collection of all maps $f: A_{} \rightarrow B_{}$ for which the induced map

$(A_{} \times B'_{} ) \coprod _{ A_{} \times A'_{} } ( B_{} \times A'_{} ) \hookrightarrow B_{} \times B'_{}$

is anodyne. We wish to show that every anodyne morphism belongs to $T$. Since $T$ is weakly saturated, it will suffice to show that every horn inclusion $f: \Lambda ^{n}_{i} \hookrightarrow \Delta ^ n$ belongs to $T$ (for $n > 0$). Without loss of generality, we may assume that $0 < i$, so that $f$ is a retract of the map $g: (\Delta ^1 \times \Lambda ^ n_ i) \coprod _{ \{ 1\} \times \Lambda ^{n}_ i} ( \{ 1\} \times \Delta ^ n) \hookrightarrow \Delta ^1 \times \Delta ^ n$ (Lemma 3.1.2.8). It will therefore suffice to show that $g$ belongs to $T$. Replacing $f'$ by the monomorphism $(\Lambda ^{n}_{i} \times B'_{} ) \coprod _{ \Lambda ^{n}_{i} \times A'_{} } (\Delta ^ n \times A'_{} )$, we are reduced to showing that the inclusion $\{ 1\} \hookrightarrow \Delta ^1$ belongs to $T$.

Let $T'$ denote the collection of all morphisms of simplicial sets $f'': A''_{} \rightarrow B''_{}$ for which the map $(\{ 1\} \times B''_{} ) \coprod _{ \{ 1\} \times A''_{} } ( \Delta ^1 \times A''_{} ) \rightarrow \Delta ^1 \times B''_{}$ is anodyne. We will complete the proof by showing that $T'$ contains all monomorphisms of simplicial sets. By virtue of Proposition 1.4.5.12, it will suffice to show that $T''$ contains the inclusion map $\operatorname{\partial \Delta }^ m \hookrightarrow \Delta ^{m}$, for each $m > 0$. In other words, we are reduced to showing that the inclusion $(\{ 1\} \times \Delta ^ m ) \coprod _{ \{ 1\} \times \operatorname{\partial \Delta }^ m } ( \Delta ^1 \times \operatorname{\partial \Delta }^ m) \hookrightarrow \Delta ^1 \times \Delta ^ m$ is anodyne, which follows from Lemma 3.1.2.9. $\square$