Theorems · Definition · category theory

CategoryTheory.IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
        {X : C} →
          {J : Type w} →
            [inst_3 : CategoryTheory.SmallCategory J] →
              (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X)) →
                [CategoryTheory.IsFiltered J] →
                  (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.MonoOver.forget X))) →
                    [inst_5 : CategoryTheory.Mono c.pt.hom] →
                      CategoryTheory.Subobject.mk c.pt.hom = ⨆ j, CategoryTheory.Subobject.mk (F.obj j).obj.hom →
                        CategoryTheory.Limits.IsColimit ((CategoryTheory.Over.forget X).mapCocone c)

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.)

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Cited by

0 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelianCategoryTheory.SmallCategoryCategoryTheory.IsFilteredCategoryTheory.Mono