totalFlipIsoX

Mathlib.Algebra.Homology.TotalComplexSymmetry

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

Lean4

/-- Auxiliary definition for `totalFlipIso`. -/
noncomputable def totalFlipIsoX (j : J) : (K.flip.total c).X j ≅ (K.total c).X j
    where
  hom :=
    K.flip.totalDesc
      (fun i₂ i₁ h =>
        ComplexShape.σ c₁ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j (by rw [← ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]))
  inv :=
    K.totalDesc
      (fun i₁ i₂ h =>
        ComplexShape.σ c₁ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j (by rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]))
  hom_inv_id := by ext; simp
  inv_hom_id := by ext; simp

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

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

Разделы

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

Аффилиация

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