Theorem CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject_top
Modification history
2026-08-11 00:21
Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
chore: bump toolchain to v4.34.0-rc1 (#42619)
Modified CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject_topView on Github →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.largerSubobject_topView on Github →