generatingMonomorphisms — Mathlib

English

There is an instance giving HasCoseparator for Grothendieck abelian categories via an equivalence.

Русский

Существует инстанс HasCoseparator для абелевых категорий Гротендика через эквивалентность.

LaTeX

$$$\text{HasCoseparator } C$$$

Lean4

/-- Given an object `G : C`, this is the family of morphisms in `C`
given by the inclusions of all subobjects of `G`. If `G` is a separator,
and `C` is a Grothendieck abelian category, then any monomorphism in `C`
is a transfinite composition of pushouts of monomorphisms in this family
(see `generatingMonomorphisms.exists_transfiniteCompositionOfShape`). -/
def generatingMonomorphisms (G : C) : MorphismProperty C :=
  MorphismProperty.ofHoms (fun (X : Subobject G) ↦ X.arrow)

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