epi_toCycles

Mathlib.Algebra.Homology.ShortComplex.Exact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.Exact.epi_toCycles

English

If S is exact with left-homology, then toCycles is epi.

Русский

Если S точен и есть левая гомология, то toCycles эпиморфизм.

LaTeX

$$$ \\mathrm{epi}(S\\!\\to\\!Cycles) $$$

Lean4

theorem epi_toCycles (hS : S.Exact) [S.HasLeftHomology] : Epi S.toCycles :=
  hS.epi_f' _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru