mono_fromOpcycles

Mathlib.Algebra.Homology.ShortComplex.Exact

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

English

If S is exact, then fromOpcycles is mono when there is right-homology.

Русский

Если S точен, то fromOpcycles моно при наличии правой гомологии.

LaTeX

$$$ Mono\\; S.fromOpcycles $$$

Lean4

theorem mono_fromOpcycles (hS : S.Exact) [S.HasRightHomology] : Mono S.fromOpcycles :=
  hS.mono_g' _

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

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

Разделы

Аффилиация

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