Theorems · Theorem · category theory

CategoryTheory.IsGrothendieckAbelian.mono_of_isColimit_monoOver

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [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).comp (CategoryTheory.Over.forget X)))}
  (hc : CategoryTheory.Limits.IsColimit c) (f : c.pt ⟶ X),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι.app j) f = (F.obj j).obj.hom) → CategoryTheory.Mono 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.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelianCategoryTheory.SmallCategoryCategoryTheory.IsFiltered