monoModSerre_of_mono

Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

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

← MathLib Explorer

English

If f is a mono, then f is in the Serre-mod-Serre class for P.

Русский

Если f мономорфизм, то f принадлежит классу Serre для P.

LaTeX

$$P.monoModSerre f$$

Lean4

theorem monoModSerre_of_mono {X Y : C} (f : X ⟶ Y) [Mono f] : P.monoModSerre f :=
  P.monomorphisms_le_monoModSerre f (monomorphisms.infer_property f)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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