moduleCatCyclesIso_inv_iCycles — Mathlib

English

The inverse of the cycles isomorphism composed with iCycles equals the left-homology inclusion data.

Русский

Обратное изоморфизма циклов, после композиции с iCycles, равно включению левой гомологии.

LaTeX

$$$ \mathrm{moduleCatCyclesIso.inv} \circ \mathrm{iCycles} = \mathrm{moduleCatLeftHomologyData.i} $$$

Lean4

@[reassoc (attr := simp, elementwise)]
theorem moduleCatCyclesIso_inv_iCycles : S.moduleCatCyclesIso.inv ≫ S.iCycles = S.moduleCatLeftHomologyData.i :=
  S.moduleCatLeftHomologyData.cyclesIso_inv_comp_iCycles

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