exact_iff_surjective_moduleCatToCycles

English

Exactness of a short complex is equivalent to the surjectivity of the map to cycles.

Русский

Точность короткого комплекса эквивалентна сюръективности отображения к циклам.

LaTeX

$$$ S.Exact \iff Surjective\; S.moduleCatToCycles $$$

Lean4

theorem exact_iff_surjective_moduleCatToCycles : S.Exact ↔ Function.Surjective S.moduleCatToCycles := by
  simp [S.moduleCatLeftHomologyData.exact_iff_epi_f', ModuleCat.epi_iff_surjective, moduleCatLeftHomologyData_K]

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