Theorems · Theorem · category theory

CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  {J : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.IsCardinalPresentable X κ]
  [CategoryTheory.EssentiallySmall.{w, v_1, u_1} J] [CategoryTheory.IsCardinalFiltered J κ]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  (f : X ⟶ c.pt), ∃ j f', CategoryTheory.CategoryStruct.comp f' (c.ι.app j) = f

Defined in

Mathlib.CategoryTheory.Presentable.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFactCategoryTheory.CategoryCategoryTheory.IsCardinalPresentableCategoryTheory.EssentiallySmallCategoryTheory.IsCardinalFiltered