totalFlipIso

Mathlib.Algebra.Homology.TotalComplexSymmetry

URI: https://scilib.ai/kg/mathlib#HomologicalComplex₂.totalFlipIso

Lean4

/-- The symmetry isomorphism `K.flip.total c ≅ K.total c` of the total complex of a
bicomplex when we have `[TotalComplexShapeSymmetry c₁ c₂ c]`. -/
noncomputable def totalFlipIso : K.flip.total c ≅ K.total c :=
  HomologicalComplex.Hom.isoOfComponents (K.totalFlipIsoX c)
    (fun j j' _ =>
      by
      simp only [total_d, Preadditive.comp_add, totalFlipIsoX_hom_D₁, totalFlipIsoX_hom_D₂, Preadditive.add_comp]
      rw [add_comm])

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru