Kerodon

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

Corollary 3.5.9.20. Let $f: X \rightarrow Y$ be a morphism of Kan complexes and let $n \geq -2$. The following conditions are equivalent:

$(1)$

The morphism $f$ is $n$-truncated.

$(2)$

The restriction map

\[ \theta : \operatorname{Fun}(\Delta ^{n+2}, X) \rightarrow \operatorname{Fun}(\Delta ^{n+2}, Y) \times _{ \operatorname{Fun}( \operatorname{\partial \Delta }^{n+2}, Y) } \operatorname{Fun}( \operatorname{\partial \Delta }^{n+2}, X) \]

is a homotopy equivalence.

$(3)$

The diagram of Kan complexes

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}(\Delta ^{n+2},X) \ar [d]^{f} \ar [r] & \operatorname{Fun}( \operatorname{\partial \Delta }^{n+2}, X) \ar [d] \\ \operatorname{Fun}(\Delta ^{n+2}, Y) \ar [r] & \operatorname{Fun}( \operatorname{\partial \Delta }^{n+2}, Y) } \]

is a homotopy pullback square.

$(4)$

The diagram of Kan complexes

\[ \xymatrix@R =50pt@C=50pt{ X \ar [d]^{f} \ar [r] & \operatorname{Fun}( \operatorname{\partial \Delta }^{n+2}, X) \ar [d] \\ Y \ar [r] & \operatorname{Fun}( \operatorname{\partial \Delta }^{n+2}, Y) } \]

is a homotopy pullback square.

Proof. The equivalence $(1) \Leftrightarrow (2)$ follows by applying Variant 3.5.9.19 in the special case $k = n+2$. The equivalence $(2) \Leftrightarrow (3)$ follows from Example 3.4.1.3, and the equivalence $(3) \Leftrightarrow (4)$ from Corollary 3.4.1.12. $\square$