Theorems · Theorem · category theory

CategoryTheory.IsFinitelyPresentable.exists_eq_of_isColimit

∀ {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 : C} [CategoryTheory.IsFinitelyPresentable X] {i j : J} (f : X ⟶ D.obj i)
  (g : X ⟶ D.obj j),
  CategoryTheory.CategoryStruct.comp f (c.ι.app i) = CategoryTheory.CategoryStruct.comp g (c.ι.app j) →
    ∃ k u v, CategoryTheory.CategoryStruct.comp f (D.map u) = CategoryTheory.CategoryStruct.comp g (D.map v)

Defined in

Mathlib.CategoryTheory.Presentable.Finite

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.SmallCategoryCategoryTheory.IsFilteredCategoryTheory.IsFinitelyPresentable