Theorems · Theorem · category theory

CategoryTheory.IsGrothendieckAbelian.exists_isIso_of_functor_from_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)) {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ],
  HasCardinalLT (CategoryTheory.Subobject X) κ →
    ∀
      (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.Epi f → ∃ j, CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelianCategoryTheory.SmallCategoryFactCategoryTheory.IsCardinalFiltered