Commit 2025-02-17 13:55 ea862f95

View on Github →

feat(CategoryTheory): subobjects in Grothendieck abelian categories (#21986) We study the complete lattice of subjects of X : C when C is a Grothendieck abelian cateogry. In particular, for a functor F : J ⥤ MonoOver X from a filtered category, we relate the colimit of F (computed in C) and the supremum of the subobjects corresponding to the objects in the image of F.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean

added theorem CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver

added theorem CategoryTheory.IsGrothendieckAbelian.mono_of_isColimit_monoOver

added theorem CategoryTheory.IsGrothendieckAbelian.subobject_mk_of_isColimit_eq_iSup

Modified Mathlib/CategoryTheory/Subobject/Basic.lean

added theorem CategoryTheory.MonoOver.subobjectMk_le_mk_of_hom

Modified Mathlib/CategoryTheory/Subobject/Lattice.lean

added theorem CategoryTheory.Subobject.epi_iff_mk_eq_top

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean