Theorems · Theorem · category theory

CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity

∀ {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)
  {κ : Cardinal.{w}} [hκ : Fact κ.IsRegular] [CategoryTheory.IsCardinalFiltered J κ],
  HasCardinalLT (CategoryTheory.Subobject X) κ →
    ∀ (j₀ : J) (y₁ y₂ : X ⟶ Y.obj j₀),
      CategoryTheory.CategoryStruct.comp y₁ (c.ι.app j₀) = CategoryTheory.CategoryStruct.comp y₂ (c.ι.app j₀) →
        ∃ j φ, CategoryTheory.CategoryStruct.comp y₁ (Y.map φ) = CategoryTheory.CategoryStruct.comp y₂ (Y.map φ)

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelianCategoryTheory.SmallCategoryFactCategoryTheory.IsCardinalFiltered