Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proposition 3.4.1.9 (Symmetry). A commutative diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ X_{01} \ar [r] \ar [d] & X_0 \ar [d]^{f_0} \\ X_1 \ar [r]^-{f_1} & X } \]

is a homotopy pullback square if and only if the transposed diagram

\[ \xymatrix@R =50pt@C=50pt{ X_{01} \ar [r] \ar [d] & X_1 \ar [d]^{f_1} \\ X_0 \ar [r]^-{f_0} & X } \]

is a homotopy pullback square.

Proof. Using Proposition 3.1.7.1, we can choose factorizations

\[ X_0 \xrightarrow {w_0} X'_0 \xrightarrow {f'_0} S \quad \quad X_1 \xrightarrow {w_1} X'_1 \xrightarrow {f'_1} S \]

of $f_0$ and $f_1$, where both $f'_0$ and $f'_1$ are Kan fibrations and both $w_0$ and $w_1$ are weak homotopy equivalences. We have a commutative diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ X_{01} \ar [r]^-{u} \ar [d]^{v} & X_0 \times _{X} X'_1 \ar [r] \ar [d]^{v'} & X_0 \ar [d]^{w_0} \\ X'_0 \times _{X} X_1 \ar [r]^-{u'} \ar [d] & X'_0 \times _{X} X'_1 \ar [r] \ar [d] & X'_0 \ar [d]^{f'_0} \\ X_1 \ar [r]^-{w_1} & X'_1 \ar [r]^-{ f'_1} & X. } \]

We wish to show that $u$ is a weak homotopy equivalence if and only if $v$ is a weak homotopy equivalence (see Proposition 3.4.1.2). This follows from the two-out-of-three property (Remark 3.1.6.16), since the morphisms $u'$ and $v'$ are weak homotopy equivalences by virtue of Corollary 3.3.7.4. $\square$