English
Let G be separator in a Grothendieck abelian category. Then for any morphism f: A → X there exists a transfinite composition of pushouts of monomorphisms in the generating family of G realizing f.
Русский
Пусть G — разделяющий объект в абелевой категории Гротенштейда. Тогда для любого морфизма f: A → X существует трансфинитная композиция pushouts мономорфизмов из порождающей семьи G, реализующая f.
LaTeX
$$$\\forall f:\\; A\\to X, \\exists \\text{TransfiniteCompositionOfShape } J\\; (\\text{from bot})\\; f$$$
Lean4
/-- Let `C` be a Grothendieck abelian category. Assume that `G : C` is a generator
of `C`. Then, any morphism in `C` is a transfinite composition of pushouts
of monomorphisms in the family `generatingMonomorphisms G` which consists
of the inclusions of the subobjects of `G`. -/
theorem exists_transfiniteCompositionOfShape :
∃ (J : Type w) (_ : LinearOrder J) (_ : OrderBot J) (_ : SuccOrder J) (_ : WellFoundedLT J),
Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f) :=
by
obtain ⟨o, j, hj⟩ := exists_ordinal hG (Subobject.mk f)
letI : OrderBot o.toType :=
Ordinal.toTypeOrderBot (by simpa only [← Ordinal.toType_nonempty_iff_ne_zero] using Nonempty.intro j)
exact ⟨_, _, _, _, _, ⟨transfiniteCompositionOfShapeOfEqTop hG hj⟩⟩
