English
There are homotopies connecting the null-homotopic maps Hσ and the complementary projection Q in the Dold–Kan decomposition, providing a full homotopy equivalence between P and Id components.
Русский
Существуют гомотопии, соединяющие нулевые гомотопии Hσ и комплементарное проецирование Q в разложении Dold–Kan, образуя полное гомотопное равенство между P и Id компонентами.
LaTeX
$$$$ Hσ \sim 0 \quad\text{and}\quad Q \sim 0 \quad\text{in appropriate decompositions} $$$$
Lean4
/-- Inductive construction of homotopies from `P q` to `𝟙 _` -/
noncomputable def homotopyPToId : ∀ q : ℕ, Homotopy (P q : K[X] ⟶ _) (𝟙 _)
| 0 => Homotopy.refl _
| q + 1 =>
by
refine
Homotopy.trans (Homotopy.ofEq ?_)
(Homotopy.trans (Homotopy.add (homotopyPToId q) (Homotopy.compLeft (homotopyHσToZero q) (P q)))
(Homotopy.ofEq ?_))
· simp only [P_succ, comp_add, comp_id]
· simp only [add_zero, comp_zero]
