epi_δ

Mathlib.Algebra.Homology.HomologySequence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.ShortExact.epi_δ

English

If the j-th homology of X2 is zero, then hS.δ i j hij is epic.

Русский

Если j-я гомология X2 равна нулю, то hS.δ i j hij эпиморфизм

LaTeX

$$hS.δ i j hij is an epimorphism$$

Lean4

theorem epi_δ (hj : IsZero (S.X₂.homology j)) : Epi (hS.δ i j hij) :=
  (HomologicalComplex.HomologySequence.snakeInput _ _ _ _).epi_δ hj

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

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

Разделы

Аффилиация

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