Theorems · Theorem · category theory

CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit_under

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.IsFiltered J] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D}
  (hc : CategoryTheory.Limits.IsColimit c) {X A : C} (p : X ⟶ A) (s : (CategoryTheory.Functor.const J).obj X ⟶ D)
  [CategoryTheory.IsFinitelyPresentable (CategoryTheory.Under.mk p)] (f : A ⟶ c.pt),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = CategoryTheory.CategoryStruct.comp p f) →
    ∃ j q, CategoryTheory.CategoryStruct.comp p q = s.app j ∧ CategoryTheory.CategoryStruct.comp q (c.ι.app j) = f

Defined in

Mathlib.CategoryTheory.Presentable.Finite

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.SmallCategoryCategoryTheory.IsFilteredCategoryTheory.IsFinitelyPresentable