leftHomologyMap_comm — Mathlib

English

Same as LeftHomologyMap_eq, expressing leftHomologyMap φ in terms of iso data and γ.

Русский

То же, что и ранее, выражающее leftHomologyMap φ через данные изоморфизмов и γ.

LaTeX

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

Lean4

theorem leftHomologyMap_comm [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    leftHomologyMap φ ≫ h₂.leftHomologyIso.hom = h₁.leftHomologyIso.hom ≫ γ.φH := by
  simp only [γ.leftHomologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

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