Theorems · Theorem · category theory

CategoryTheory.IsFiltered.cocone_nonempty

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered C] {J : Type w}
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (F : CategoryTheory.Functor J C),
  Nonempty (CategoryTheory.Limits.Cocone F)

If we have IsFiltered C, then for any functor F : J ⥤ C with FinCategory J, there exists a cocone over F.

Defined in

Mathlib.CategoryTheory.Filtered.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.IsFilteredCategoryTheory.SmallCategoryCategoryTheory.FinCategory