π_comp_leftHomologyIso_inv — Mathlib

English

Under the LeftHomologyData h and S.HasLeftHomology, the dual relation holds: h.π ≫ h.leftHomologyIso.inv = h.cyclesIso.inv ≫ S.leftHomologyπ.

Русский

При данных левой гомологии h и S.hasLeftHomology выполняется двойная связь: h.π ≫ h.leftHomologyIso.inv = h.cyclesIso.inv ≫ S.leftHomologyπ.

LaTeX

$$$h.\pi \circ h.leftHomologyIso.inv = h.cyclesIso.inv \circ S.leftHomology\pi$$$

Lean4

@[reassoc (attr := simp)]
theorem π_comp_leftHomologyIso_inv : h.π ≫ h.leftHomologyIso.inv = h.cyclesIso.inv ≫ S.leftHomologyπ := by
  simp only [← cancel_epi h.cyclesIso.hom, ← cancel_mono h.leftHomologyIso.hom, assoc, Iso.inv_hom_id, comp_id,
    Iso.hom_inv_id_assoc, LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom]

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