pOpcycles_comp_opcyclesIso_hom — Mathlib

English

For a RightHomologyData h with S having right homology, the composition h.rightHomologyIso.inv ≫ S.rightHomologyι equals h.ι ≫ h.opcyclesIso.inv.

Русский

Для правой гомологической структуры h с S, обладающим правой гомологией, композиция h.rightHomologyIso.inv ≫ S.rightHomologyι равна h.ι ≫ h.opcyclesIso.inv.

LaTeX

$$h.rightHomologyIso.inv \circ S.rightHomology\u03b9 = h.\u027e ≫ h.opcyclesIso.inv$$

Lean4

@[reassoc (attr := simp)]
theorem pOpcycles_comp_opcyclesIso_hom : S.pOpcycles ≫ h.opcyclesIso.hom = h.p := by
  simp only [← h.p_comp_opcyclesIso_inv, assoc, Iso.inv_hom_id, comp_id]

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