English
There is a canonical homotopy from the endomorphism PInfty on the complex X to the identity map, constructed by pasting the individual homotopies PToId at successive stages.
Русский
Существует каноническая гомотопия от PInfty к identidad на комплексe X, собранная из последовательных гомотопий PToId на последовательных шагах.
LaTeX
$$$\text{There exists a canonical homotopy } PInftyToId\ X\;:\; (PInfty : K[X] \to \mathrm{Id})\;\Rightarrow\; \mathrm{Id}$$$
Lean4
/-- Construction of the homotopy from `PInfty` to the identity using eventually
(termwise) constant homotopies from `P q` to the identity for all `q` -/
@[simps]
def homotopyPInftyToId : Homotopy (PInfty : K[X] ⟶ _) (𝟙 _)
where
hom i j := (homotopyPToId X (j + 1)).hom i j
zero i j hij := Homotopy.zero _ i j hij
comm
n := by
rcases n with _ | n
·
simpa only [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex, PInfty_f, P_f_0_eq, zero_add] using
(homotopyPToId X 2).comm 0
·
simpa only [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex, HomologicalComplex.id_f, PInfty_f,
← P_is_eventually_constant (le_refl <| n + 1),
homotopyPToId_eventually_constant X (Nat.lt_add_one (Nat.succ n)), Homotopy.dNext_succ_chainComplex,
Homotopy.prevD_chainComplex] using (homotopyPToId X (n + 2)).comm (n + 1)
