Theorems · Theorem · category theory

CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup

∀ {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))
  [inst_4 : CategoryTheory.IsFiltered J]
  {c : CategoryTheory.Limits.Cocone (F.comp ((CategoryTheory.MonoOver.forget X).comp (CategoryTheory.Over.forget X)))}
  (hc : CategoryTheory.Limits.IsColimit c) (f : c.pt ⟶ X)
  (hf : ∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) f = (F.obj j).obj.hom),
  CategoryTheory.Subobject.mk f = ⨆ j, CategoryTheory.Subobject.mk (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, 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.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelianCategoryTheory.SmallCategoryCategoryTheory.IsFiltered