Documentation

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Subobjects in Grothendieck abelian categories #

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.

If C is a Grothendieck abelian category, X : C, if F : J ⥤ MonoOver X is a functor from a filtered category J, c is a colimit cocone for the corresponding functor J ⥤ C, and f : c.pt ⟶ X is induced by the inclusions, then f is a monomorphism.

If C is a Grothendieck abelian category, X : C, if F : J ⥤ MonoOver X is a functor from a filtered category J, the colimit of F (computed in C) gives a subobject of F which is a supremum of the subobjects corresponding to the objects in the image of the functor F.

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. (See also subobjectMk_of_isColimit_eq_iSup.)

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_monoOver {C : Type u} [Category.{v, u} C] [Abelian C] [IsGrothendieckAbelian C] {X : C} {J : Type w} [SmallCategory J] (F : Functor J (MonoOver X)) {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [IsCardinalFiltered J κ] (hXκ : HasCardinalLT (Subobject X) κ) (c : Limits.Cocone (F.comp ((MonoOver.forget X).comp (Over.forget X)))) (hc : Limits.IsColimit c) (f : c.pt X) (hf : ∀ (j : J), CategoryStruct.comp (c.ι.app j) f = (F.obj j).obj.hom) (h : Epi f) :
    ∃ (j : J), IsIso (F.obj j).obj.hom

    If C is a Grothendieck abelian category, X : C, if F : J ⥤ MonoOver X is a functor from a κ-filtered category J with κ a regular cardinal such that HasCardinalLT (Subobject X) κ, and if the colimit of F (computed in C) maps epimorphically onto X, then there exists j : J such that (F.obj j).obj.hom is an isomorphism.