Theorems · Definition · category theory

CategoryTheory.Limits.limitCompCoyonedaIsoCone

{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          (X : C) →
            CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) ≅
              (CategoryTheory.Functor.const J).obj X ⟶ F

A cone on F with cone point X is the same as an element of lim Hom(X, F·).

Defined in

Mathlib.CategoryTheory.Limits.Types.Yoneda

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.Category