Homotopy equivalent Kan complexes have homotopy equivalent "path spaces"

38 Views Asked by At

$\DeclareMathOperator{\Fun}{Fun}$ Let $f\colon X\to Y$ be a homotopy equivalence of Kan complexes (in the sense of Definition 3.1.6.1. in Kerodon), with a homotopy inverse $g\colon Y\to X$. I want to show that the induced map $f^*\colon\Fun(\Delta^1, X)\to\Fun(\Delta^1, Y)$ is a homotopy equivalence (the $\infty$-category of functors is defined in Construction 1.4.3.1.).

I was thinking of applying Proposition 3.2.9.1. to

but I'm unsure how to show that the fibers are homotopy equivalent.

Alternatively, I was thinking that for every 0-simplex $\alpha\colon\Delta^1\to X$ we get the $\Lambda^3_1$ horn

so we can fill its bottom face to get a homotopy $gf\alpha\simeq\alpha$, but I don't know how to extend this "pointwise" homotopy.

1

There are 1 best solutions below

1
On BEST ANSWER

If $S$ is any simplicial set, then $\mathrm{Fun}(S,X)$ and $\mathrm{Fun}(S,Y)$ are both Kan complexes. Furthermore, if $h\colon X\times\Delta^1\to X$ is a simplicial homotopy between the identity and $g\circ f$ and the identity, then the composition $$\mathrm{Fun}(S,X)\times\Delta^1\to \mathrm{Fun}(S,X\times\Delta^1)\xrightarrow{h_\ast}\mathrm{Fun}(S,X)$$ is a simplicial homotopy from $(g\circ f)_\ast = g_\ast\circ f_\ast$ and the identity. Here the undecorated arrow is the adjoint of $$\mathrm{Fun}(S,X)\times\Delta^1\times S\cong \mathrm{Fun}(S,X)\times S\times\Delta^1\xrightarrow{\mathrm{ev}\times \mathrm{id}_{\Delta^1}} X\times\Delta^1.$$ The same argument shows that $f_\ast\circ g_\ast$ is homotopic to the identity of $\mathrm{Fun}(S,Y).$