P_is_eventually_constant — Mathlib

English

The 0-th component of the endomorphism PInfty on the complex X equals the identity on the 0-th level.

Русский

Нулевая компонента концевого отображения PInfty на комплексе X равна тождественному отображению на нулевом уровне.

LaTeX

$$$PInfty.f_0 = \mathrm{id}$$$

Lean4

theorem P_is_eventually_constant {q n : ℕ} (hqn : n ≤ q) : ((P (q + 1)).f n : X _⦋n⦌ ⟶ _) = (P q).f n := by
  cases n with
  | zero => simp only [P_f_0_eq]
  | succ
    n =>
    simp only [P_succ, comp_add, comp_id, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f, add_eq_left]
    exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)

Похожие утверждения