monomorphisms_le_monoModSerre

Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.monomorphisms_le_monoModSerre

English

Every monomorphism f in C lies in the Serre-mod-Serre class monomorphisms of P.

Русский

Каждый мономорфизм f в C лежит в множестве monomorphisms класса P.monoModSerre.

LaTeX

$$monomorphisms C ≤ P.monoModSerre$$

Lean4

theorem monomorphisms_le_monoModSerre : monomorphisms C ≤ P.monoModSerre := fun _ _ f (_ : Mono f) ↦
  P.prop_of_isZero (isZero_kernel_of_mono f)

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

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

Разделы

Аффилиация

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