instMonoHomologyι

Mathlib.Algebra.Homology.ShortComplex.Homology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.instMonoHomologyι

English

The morphism S.homologyι is monomorphic.

Русский

Морфизм S.homologyι мономорфизм.

LaTeX

$$$\operatorname{Mono}(S.homology\iota)$$$

Lean4

instance : Mono S.homologyι :=
  Limits.mono_of_isLimit_fork (S.homologyIsKernel)

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

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

Разделы

Аффилиация

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