Commit 2025-02-20 13:00 34c48f24

feat(CategoryTheory/Abelian/GrothendieckCategory): computing colimits in Subobject (#22123) Let X : C be an object in a Grothendieck abelian category, F : J ⥤ MonoOver X a functor from a filtered category, c a cocone for the composition F ⋙ MonoOver.forget _ : J ⥤ Over X. We assume that c.pt.hom : c.pt.left ⟶ X is a monomorphism and that the corresponding subobject of X is the supremum of the subobjects given by (F.obj j).obj.hom, then c becomes a colimit cocone after the application of the forget functor Over X ⥤ C.