hasTotal_of_iso — Mathlib

English

The property of having a total structure is preserved under isomorphism of total complexes: if K has a total for c12 and K ≅ L, then L has the same total structure.

Русский

Свойство существования полной структуры сохраняется под изоморфизмами полных комплексов: если K имеет полную структуру для c12 и K ≅ L, то и L имеет такую же полную структуру.

LaTeX

$$$\\text{hasTotal}(K,c_{12}) \\Rightarrow (K\\cong L) \\Rightarrow \\text{hasTotal}(L,c_{12})$$$

Lean4

theorem hasTotal_of_iso [K.HasTotal c₁₂] : L.HasTotal c₁₂ :=
  GradedObject.hasMap_of_iso
    (GradedObject.isoMk K.toGradedObject L.toGradedObject
      (fun ⟨i₁, i₂⟩ => (HomologicalComplex.eval _ _ i₁ ⋙ HomologicalComplex.eval _ _ i₂).mapIso e))
    _

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