leftHomologyIso_inv_naturality — Mathlib

English

Naturality for left homology: the homomorphism map commutes with leftHomologyMap under φ.

Русский

Естественность левой гомологии: отображение гомологии совместимо с leftHomologyMap при φ.

LaTeX

$$$h_1.\\mathrm{homologyIso}.hom \\circ \\text{homologyMap}(\\varphi) = \\text{leftHomologyMap}'(\\varphi,h_1,h_2) \\circ h_2.\\mathrm{homologyIso}.hom$$$

Lean4

@[reassoc]
theorem leftHomologyIso_inv_naturality (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    h₁.homologyIso.inv ≫ homologyMap φ = leftHomologyMap' φ h₁ h₂ ≫ h₂.homologyIso.inv :=
  by
  dsimp [homologyIso, ShortComplex.leftHomologyIso, homologyMap, homologyMap', leftHomologyIso]
  simp only [← leftHomologyMap'_comp, id_comp, comp_id]

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