mono_δ

Mathlib.Algebra.Homology.HomologySequence

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

English

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

Русский

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

LaTeX

$$hS.δ i j hij is a monomorphism$$

Lean4

theorem mono_δ (hi : IsZero (S.X₂.homology i)) : Mono (hS.δ i j hij) :=
  (HomologicalComplex.HomologySequence.snakeInput _ _ _ _).mono_δ hi

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

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

Разделы

Аффилиация

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