leftHomologyMap_eq — Mathlib

English

For φ: S1⟶S2 with h1,h2LeftHomologyData, leftHomologyMap φ equals h1.leftHomologyIso.hom ≫ γ.φH ≫ h2.leftHomologyIso.inv.

Русский

Для φ: S1⟶S2 с данными левой гомологии h1,h2, leftHomologyMap φ равно h1.leftHomologyIso.hom ≫ γ.φH ≫ h2.leftHomologyIso.inv.

LaTeX

$$$leftHomologyMap\,\varphi = h_{1}.leftHomologyIso.hom \circ γ.φH \circ h_{2}.leftHomologyIso.inv$$$

Lean4

theorem leftHomologyMap_eq [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    leftHomologyMap φ = h₁.leftHomologyIso.hom ≫ γ.φH ≫ h₂.leftHomologyIso.inv :=
  by
  dsimp [LeftHomologyData.leftHomologyIso, leftHomologyMapIso']
  rw [← γ.leftHomologyMap'_eq, ← leftHomologyMap'_comp, ← leftHomologyMap'_comp, id_comp, comp_id]
  rfl

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