hasHomology_of_iso — Mathlib

English

If K has homology at i, then L also has homology at i given an isomorphism K ≅ L of homological complexes.

Русский

Если у K есть гомология в индексе i, то и у L она есть при изоморфизме K ≅ L как гомологические комплексы.

LaTeX

$$[K.HasHomology i] ⇒ [L.HasHomology i] (via iso)$$

Lean4

theorem hasHomology_of_iso [K.HasHomology i] : L.HasHomology i :=
  ShortComplex.hasHomology_of_iso ((shortComplexFunctor _ _ i).mapIso iso : K.sc i ≅ L.sc i)

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