homologyMap_eq — Mathlib

English

HomologyMap φ equals h1.homologyIso.hom ≫ γ.φH ≫ h2.homologyIso.inv.

Русский

ГомологияMap φ равен h1.homologyIso.hom ≫ γ.φH ≫ h2.homologyIso.inv.

LaTeX

$$$\mathrm{homologyMap}(\varphi) = h_1.homologyIso.hom \; \circ \gamma.\phi_H \circ h_2.homologyIso.inv$$$

Lean4

theorem homologyMap_eq : homologyMap φ = h₁.homologyIso.hom ≫ γ.φH ≫ h₂.homologyIso.inv :=
  by
  dsimp [homologyMap, homologyMap', RightHomologyData.homologyIso, rightHomologyIso, RightHomologyData.rightHomologyIso]
  have γ' : HomologyMapData φ S₁.homologyData S₂.homologyData := default
  simp only [← γ.rightHomologyMap'_eq, assoc, ← rightHomologyMap'_comp_assoc, id_comp, comp_id,
    γ'.left.leftHomologyMap'_eq, γ'.right.rightHomologyMap'_eq, ← γ'.comm_assoc, Iso.hom_inv_id]

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