rightHomologyIso_hom_naturality — Mathlib

English

There exists a natural isomorphism between right and left homology data via the homology data iso.

Русский

Существует естественный изоморфизм между данными правой и левой гомологии через изоморфизм данных гомологии.

LaTeX

$$$h_1.\\text{right.homologyIso} = h_1.\\text{left.homologyIso} \\circ h_1.\\text{iso}$$$

Lean4

@[reassoc]
theorem rightHomologyIso_hom_naturality (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
    h₁.homologyIso.hom ≫ rightHomologyMap' φ h₁ h₂ = homologyMap φ ≫ h₂.homologyIso.hom := by
  rw [← cancel_epi h₁.homologyIso.inv, Iso.inv_hom_id_assoc, ←
    cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁), ←
    leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂, ←
    cancel_epi (S₁.leftHomologyData.homologyIso.hom), LeftHomologyData.leftHomologyIso_hom_naturality_assoc,
    leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac, assoc, Iso.hom_inv_id_assoc,
    Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc]

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