cyclesIso_inv_comp_iCycles — Mathlib

English

With h a LeftHomologyData for S and [S.HasLeftHomology], the inverse of cyclesIso composed with iCycles equals iCycles composed with h.i: h.cyclesIso.inv ≫ S.iCycles = h.i.

Русский

Пусть h — данные левой гомологии для S и S.hasLeftHomology. Обратно к cyclesIso отложено через iCycles: h.cyclesIso.inv ≫ S.iCycles = h.i.

LaTeX

$$$h.cyclesIso.inv \circ S.iCycles = h.i$$$

Lean4

@[reassoc (attr := simp)]
theorem cyclesIso_inv_comp_iCycles : h.cyclesIso.inv ≫ S.iCycles = h.i := by
  simp only [← h.cyclesIso_hom_comp_i, Iso.inv_hom_id_assoc]

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