homologyπ_comp_homologyIso_hom — Mathlib

English

For a left homology data h, the relation h.π ≫ h.homologyIso.inv = h.cyclesIso.inv ≫ S.homologyπ holds.

Русский

Для левого гомологического набора данных h справедливо h.π ≫ h.homologyIso.inv = h.cyclesIso.inv ≫ S.homologyπ.

LaTeX

$$$h.\pi \circ h.homologyIso.inv = h.cyclesIso.inv \circ S.homologyπ$$$

Lean4

@[reassoc (attr := simp)]
theorem homologyπ_comp_homologyIso_hom (h : S.LeftHomologyData) :
    S.homologyπ ≫ h.homologyIso.hom = h.cyclesIso.hom ≫ h.π :=
  by
  dsimp only [homologyπ, homologyIso]
  simp only [Iso.trans_hom, Iso.symm_hom, assoc, Iso.hom_inv_id_assoc, leftHomologyπ_comp_leftHomologyIso_hom]

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