Commit 2025-02-21 13:27 b0751898

View on Github →

feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) 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 morphisms of the form Y ⟶ G for some subobject Y of G.

Estimated changes