moduleCatCyclesIso_hom_i — Mathlib

English

The hom part of the cycles isomorphism composed with the inclusion i equals the map iCycles coming from the left-homology data.

Русский

Компонента 'hom' изоморфизма циклов, компонуемая с включением i, равна карте iCycles, полученной из данных левой гомологии.

LaTeX

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

Lean4

@[reassoc (attr := simp, elementwise)]
theorem moduleCatCyclesIso_hom_i : S.moduleCatCyclesIso.hom ≫ S.moduleCatLeftHomologyData.i = S.iCycles :=
  S.moduleCatLeftHomologyData.cyclesIso_hom_comp_i

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