rightHomologyIso_hom_comp_ι — Mathlib

English

For h with rightHomology, the equality h.rightHomologyIso.hom ≫ h.ι = S.rightHomologyι ≫ h.opcyclesIso.hom holds.

Русский

Для правой гомологической структуры h выполняется равенство h.rightHomologyIso.hom ≫ h.ι = S.rightHomologyι ≫ h.opcyclesIso.hom.

LaTeX

$$h.rightHomologyIso.hom \circ h.ι = S.rightHomologyι \circ h.opcyclesIso.hom$$

Lean4

@[reassoc (attr := simp)]
theorem rightHomologyIso_hom_comp_ι : h.rightHomologyIso.hom ≫ h.ι = S.rightHomologyι ≫ h.opcyclesIso.hom := by
  simp only [← cancel_mono h.opcyclesIso.inv, ← cancel_epi h.rightHomologyIso.inv, assoc, Iso.inv_hom_id_assoc,
    Iso.hom_inv_id, comp_id, rightHomologyIso_inv_comp_rightHomologyι]

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