# Kerodon

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

Proposition 3.4.1.14 (Summands). Suppose we are given a homotopy pullback square of simplicial sets

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

Let $X'_0 \subseteq X_0$, $X'_1 \subseteq X_1$, and $X' \subseteq X$ be summands satisfying $f_0(X'_0) \subseteq X' \supseteq f_1(X'_1)$, and set $X'_{01} = u^{-1}(X'_0) \cap v^{-1}(X'_1) \subseteq X_{01}$. Then the diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ X'_{01} \ar [r] \ar [d] & X'_0 \ar [d] \\ X'_1 \ar [r] & X' }$

is also a homotopy pullback square.

Proof. Consider the diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ v^{-1}( X'_1) \ar [r] \ar [d] & X_{01} \ar [r]^-{u} \ar [d]^{v} & X_0 \ar [d]^{f_0} \\ X'_1 \ar [r] & X_1 \ar [r] & X. }$

The square on the left is a pullback diagram whose horizontal maps are Kan fibrations (Example 3.1.1.4), and is therefore a homotopy pullback square (Example 3.4.1.3). The square on the right is a homotopy pullback by assumption. Applying Proposition 3.4.1.11, we deduce that bottom half of the commutative diagram

$\xymatrix@R =50pt@C=50pt{ X'_{01} \ar [r] \ar [d] & X'_0 \ar [d] \\ v^{-1}(X'_1) \ar [r] \ar [d] & X_0 \ar [d] \\ X'_1 \ar [r] & X }$

is a homotopy pullback square. The top half is a pullback diagram whose vertical maps are Kan fibrations (Example 3.1.1.4), and is therefore also a homotopy pullback square (Example 3.4.1.3). Applying Proposition 3.4.1.11 again, we conclude that the outer rectangle in the diagram

$\xymatrix@R =50pt@C=50pt{ X'_{01} \ar [r] \ar [d] & X'_0 \ar@ {=}[r] \ar [d] & X'_0 \ar [d] \\ X'_1 \ar [r] & X' \ar [r] & X }$

is a homotopy pullback square. Here the square on the right is a pullback diagram of Kan fibrations (Example 3.1.1.4), and therefore a homotopy pullback. Applying Proposition 3.4.1.11 again, we conclude that the left square is a homotopy pullback, as desired. $\square$