toCycles_moduleCatCyclesIso_hom — Mathlib

English

The composition of toCycles with the hom part of the cycles isomorphism equals the left-homology data map f'.

Русский

Составление toCycles с гомоморфной частью изоморфизма циклов даёт отображение f'.

LaTeX

$$$ S.toCycles \circ S.moduleCatCyclesIso.hom = S.moduleCatLeftHomologyData.f' $$$

Lean4

@[reassoc (attr := simp, elementwise)]
theorem toCycles_moduleCatCyclesIso_hom : S.toCycles ≫ S.moduleCatCyclesIso.hom = S.moduleCatLeftHomologyData.f' := by
  simp [← cancel_mono S.moduleCatLeftHomologyData.i]

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