Theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_transfiniteCompositionOfShape
Modification history
2025-02-21 13:27
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family (#22157) …
Added CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_transfiniteCompositionOfShapeView on Github →