homologyIso_inv_comp_homologyι — Mathlib

English

For h : S.RightHomologyData, the relation h.homologyIso.inv ≫ S.homologyι = h.ι ≫ h.opcyclesIso.inv holds.

Русский

Для h : S.RightHomologyData справедлива связь h.homologyIso.inv ≫ S.homologyι = h.ι ≫ h.opcyclesIso.inv.

LaTeX

$$$h.homologyIso.inv \circ S.homology\iota = h.\iota \circ h.opcyclesIso.inv$$$

Lean4

@[reassoc (attr := simp)]
theorem homologyIso_inv_comp_homologyι (h : S.RightHomologyData) :
    h.homologyIso.inv ≫ S.homologyι = h.ι ≫ h.opcyclesIso.inv :=
  by
  dsimp only [homologyι, homologyIso]
  simp only [Iso.trans_inv, Iso.symm_inv, assoc, Iso.hom_inv_id_assoc, rightHomologyIso_inv_comp_rightHomologyι]

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