rightHomologyIso_inv_naturality — Mathlib

English

Naturality for the inverse of the right homology iso: the inverse maps commute with homology maps along φ.

Русский

Естественность обратного правого гомологического изоморфизма: обратные отображения коммутируют с отображениями гомологии вдоль φ.

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 (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
    h₁.homologyIso.inv ≫ homologyMap φ = rightHomologyMap' φ h₁ h₂ ≫ h₂.homologyIso.inv := by
  simp only [← cancel_mono h₂.homologyIso.hom, assoc, Iso.inv_hom_id_assoc, comp_id,
    ← RightHomologyData.rightHomologyIso_hom_naturality φ h₁ h₂, Iso.inv_hom_id]

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