Documentation

Mathlib.CategoryTheory.Limits.Yoneda

Limit properties relating to the (co)yoneda embedding. #

We calculate the colimit of Y ↦ (X ⟶ Y), which is just PUnit. (This is used in characterising cofinal functors.)

We also show the (co)yoneda embeddings preserve limits and jointly reflect them.

source
@[simp]
theorem CategoryTheory.Coyoneda.colimitCocone_ι_app {C : Type v} [CategoryTheory.SmallCategory C] (X : Cᵒᵖ) (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj X_1) :
(CategoryTheory.Coyoneda.colimitCocone X).ι.app X_1 a = id PUnit.unit
source
@[simp]
theorem CategoryTheory.Coyoneda.colimitCocone_pt {C : Type v} [CategoryTheory.SmallCategory C] (X : Cᵒᵖ) :
(CategoryTheory.Coyoneda.colimitCocone X).pt = PUnit.{v + 1}
source
def CategoryTheory.Coyoneda.colimitCocone {C : Type v} [CategoryTheory.SmallCategory C] (X : Cᵒᵖ) :
CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)

The colimit cocone over coyoneda.obj X, with cocone point PUnit.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Coyoneda.colimitCoconeIsColimit_desc {C : Type v} [CategoryTheory.SmallCategory C] (X : Cᵒᵖ) (s : CategoryTheory.Limits.Cocone (CategoryTheory.coyoneda.obj X)) :
    ∀ (x : (CategoryTheory.Coyoneda.colimitCocone X).pt), CategoryTheory.Limits.IsColimit.desc C inst✝ (Type v) CategoryTheory.types (CategoryTheory.coyoneda.obj X) (CategoryTheory.Coyoneda.colimitCocone X) (CategoryTheory.Coyoneda.colimitCoconeIsColimit X) s x = C.app inst✝ (Type v) CategoryTheory.types (CategoryTheory.coyoneda.obj X) ((CategoryTheory.Functor.const C).obj s.pt) s.ι X.unop (CategoryTheory.CategoryStruct.id X.unop)
    source
    def CategoryTheory.Coyoneda.colimitCoconeIsColimit {C : Type v} [CategoryTheory.SmallCategory C] (X : Cᵒᵖ) :
    CategoryTheory.Limits.IsColimit (CategoryTheory.Coyoneda.colimitCocone X)

    The proposed colimit cocone over coyoneda.obj X is a colimit cocone.

    Instances For
      source
      instance CategoryTheory.Coyoneda.instHasColimitTypeTypesObjOppositeToQuiverToCategoryStructOppositeFunctorToQuiverToCategoryStructCategoryToPrefunctorCoyoneda {C : Type v} [CategoryTheory.SmallCategory C] (X : Cᵒᵖ) :
      CategoryTheory.Limits.HasColimit (CategoryTheory.coyoneda.obj X)
      source
      noncomputable def CategoryTheory.Coyoneda.colimitCoyonedaIso {C : Type v} [CategoryTheory.SmallCategory C] (X : Cᵒᵖ) :
      CategoryTheory.Limits.colimit (CategoryTheory.coyoneda.obj X) ≅ PUnit.{v + 1}

      The colimit of coyoneda.obj X is isomorphic to PUnit.

      Instances For
        source
        instance CategoryTheory.yonedaPreservesLimits {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) :
        CategoryTheory.Limits.PreservesLimits (CategoryTheory.yoneda.obj X)

        The yoneda embedding yoneda.obj X : Cᵒᵖ ⥤ Type v for X : C preserves limits.

        source
        instance CategoryTheory.coyonedaPreservesLimits {C : Type u} [CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) :
        CategoryTheory.Limits.PreservesLimits (CategoryTheory.coyoneda.obj X)

        The coyoneda embedding coyoneda.obj X : C ⥤ Type v for X : Cᵒᵖ preserves limits.

        source
        def CategoryTheory.yonedaJointlyReflectsLimits {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J Cᵒᵖ) (c : CategoryTheory.Limits.Cone K) (t : (X : C) → CategoryTheory.Limits.IsLimit ((CategoryTheory.yoneda.obj X).mapCone c)) :
        CategoryTheory.Limits.IsLimit c

        The yoneda embeddings jointly reflect limits.

        Instances For
          source
          def CategoryTheory.coyonedaJointlyReflectsLimits {C : Type u} [CategoryTheory.Category.{v, u} C] (J : Type w) [CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone K) (t : (X : Cᵒᵖ) → CategoryTheory.Limits.IsLimit ((CategoryTheory.coyoneda.obj X).mapCone c)) :
          CategoryTheory.Limits.IsLimit c

          The coyoneda embeddings jointly reflect limits.

          Instances For
            source
            instance CategoryTheory.yonedaFunctorPreservesLimits {D : Type u} [CategoryTheory.SmallCategory D] :
            CategoryTheory.Limits.PreservesLimits CategoryTheory.yoneda
            source
            instance CategoryTheory.coyonedaFunctorPreservesLimits {D : Type u} [CategoryTheory.SmallCategory D] :
            CategoryTheory.Limits.PreservesLimits CategoryTheory.coyoneda
            source
            instance CategoryTheory.yonedaFunctorReflectsLimits {D : Type u} [CategoryTheory.SmallCategory D] :
            CategoryTheory.Limits.ReflectsLimits CategoryTheory.yoneda
            source
            instance CategoryTheory.coyonedaFunctorReflectsLimits {D : Type u} [CategoryTheory.SmallCategory D] :
            CategoryTheory.Limits.ReflectsLimits CategoryTheory.coyoneda