rightHomologyIso_inv_naturality — Mathlib

English

Naturality for the left/right homology maps with the right homology maps under φ.

Русский

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

LaTeX

$$$\\text{rightHomologyIso}.inv \\circ \\text{homologyMap}(\\varphi) = \\text{rightHomologyMap}'(\\varphi,h_1,h_2) \\circ h_2.\\mathrm{inv}$$$

Lean4

@[reassoc]
theorem rightHomologyIso_inv_naturality :
    S₁.rightHomologyIso.inv ≫ rightHomologyMap φ = homologyMap φ ≫ S₂.rightHomologyIso.inv := by
  simpa only [RightHomologyData.homologyIso_rightHomologyData, Iso.symm_inv] using
    RightHomologyData.rightHomologyIso_hom_naturality φ S₁.rightHomologyData S₂.rightHomologyData

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