Theorems · Definition · category theory

CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones

(J : Type v) →
  [inst : CategoryTheory.SmallCategory J] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (CategoryTheory.Functor.opHom J C).comp
            ((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).comp
              (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v))
                        (CategoryTheory.Functor Jᵒᵖ (Type v)) (Type v)).obj
                    CategoryTheory.Limits.lim).comp
                ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Functor Cᵒᵖ (Type v)) (Type v)).obj
                  CategoryTheory.yoneda))) ≅
          CategoryTheory.cocones J C

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

Defined in

Mathlib.CategoryTheory.Limits.Types.Yoneda

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.Category