English
In a Grothendieck abelian setting, a canonical transfinite construction from the bottom to top provides a factorization of any morphism into a transfinite composition of pushouts of generating monomorphisms.
Русский
В условиях Гротендековой абелевой категории каноническое трансфинитное построение от низа к верху обеспечивает факторизацию любого морфизма в трансфинитную композицию pushouts порождающих мономорфизмов.
LaTeX
$$$\\forall f:\\, A\\to X,\\; f\\text{ factors as a transfinite composition of pushouts of generating monomorphisms}$$$
Lean4
/-- If `transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤`,
then the monomorphism `f` is a transfinite composition of pushouts of
monomorphisms in the family `generatingMonomorphisms G`. -/
noncomputable def transfiniteCompositionOfShapeOfEqTop {J : Type w} [LinearOrder J] [OrderBot J] [SuccOrder J]
[WellFoundedLT J] {j : J} (hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤) :
(generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape (Set.Iic j) f :=
by
let t := transfiniteIterate (largerSubobject hG) j (Subobject.mk f)
have := (Subobject.isIso_arrow_iff_eq_top t).2 hj
apply (transfiniteCompositionOfShapeMapFromBot hG (Subobject.mk f) j).ofArrowIso
refine
Arrow.isoMk ((Subobject.isoOfEq _ _ (transfiniteIterate_bot _ _) ≪≫ Subobject.underlyingIso f)) (asIso t.arrow) ?_
dsimp [MonoOver.forget]
rw [assoc, Subobject.underlyingIso_hom_comp_eq_mk, Subobject.ofLE_arrow, Subobject.ofLE_arrow]
