leftHomologyIso_inv_naturality — Mathlib

English

Naturality for right homology with respect to a morphism φ: the right-homology map commutes with the central morphism and the rightHomologyIso.

Русский

Естественность правой гомологии по отношению к φ: отображение правой гомологии коммутирует с центральным отображением и rightHomologyIso.

LaTeX

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

Lean4

@[reassoc]
theorem leftHomologyIso_inv_naturality :
    S₁.leftHomologyIso.inv ≫ leftHomologyMap φ = homologyMap φ ≫ S₂.leftHomologyIso.inv := by
  simpa only [LeftHomologyData.homologyIso_leftHomologyData, Iso.symm_inv] using
    LeftHomologyData.leftHomologyIso_hom_naturality φ S₁.leftHomologyData S₂.leftHomologyData

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