English
Let C be a Grothendieck abelian category and G a separator object. Then the construction associated to G yields a well-ordered, continuous filtration of subobjects, ensuring a transfinite composition of pushouts of monomorphisms from a generating family exists along every initial segment of a given well-ordered index set.
Русский
Пусть C — абелева категория Гротенштейджа и G — разделяющий объект. Тогда соответствующая конструкция дает хорошо упорядочиваемую, непрерывную фильтрацию подобъектов, которая обеспечивает существование трансфинитной композиции воздушных объединений мономорфизмов из порождающей семьи по каждому начальному отрезку данного хорошо упорядоченного множества индексов.
LaTeX
$$$\\forall \\text{ J a LinearOrder},\\;\\text{the transfinite construction for }(G, \\text{A₀}, J)\\text{ yields a well-ordered continuous diagram of monomorphisms},$$$
Lean4
instance : (functor hG A₀ J).IsWellOrderContinuous where
nonempty_isColimit m
hm :=
⟨by
have := hm.nonempty_Iio.to_subtype
let c := (Set.principalSegIio m).cocone (functorToMonoOver hG A₀ J ⋙ MonoOver.forget _)
have : Mono c.pt.hom := by dsimp [c]; infer_instance
apply
IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup
((Set.principalSegIio m).monotone.functor ⋙ functorToMonoOver hG A₀ J) c
dsimp [c]
simp only [Subobject.mk_arrow]
exact transfiniteIterate_limit (largerSubobject hG) A₀ m hm⟩
