Theorems · Theorem · category theory

CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivity

∀ {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]
  {Y : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone Y} (hc : CategoryTheory.Limits.IsColimit c)
  [∀ (j j' : J) (φ : j ⟶ j'), CategoryTheory.Mono (Y.map φ)] {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J κ],
  HasCardinalLT (CategoryTheory.Subobject X) κ →
    ∀ (z : X ⟶ c.pt), ∃ j₀ y, z = CategoryTheory.CategoryStruct.comp y (c.ι.app j₀)

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelianCategoryTheory.SmallCategoryCategoryTheory.MonoFactCategoryTheory.IsCardinalFiltered