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.

@[simp]
theorem CategoryTheory.Coyoneda.colimitCocone_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] (X : Cᵒᵖ) (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj X_1) :

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

Equations
Instances For

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.Limits.coneOfSectionCompYoneda_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : (F.comp (CategoryTheory.yoneda.obj X)).sections) :
        def CategoryTheory.Limits.coneOfSectionCompYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : (F.comp (CategoryTheory.yoneda.obj X)).sections) :

        The cone of F corresponding to an element in (F ⋙ yoneda.obj X).sections.

        Equations
        Instances For
          Equations

          The yoneda embeddings jointly reflect limits.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Limits.coneOfSectionCompCoyoneda_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : (F.comp (CategoryTheory.coyoneda.obj X)).sections) :
            def CategoryTheory.Limits.coneOfSectionCompCoyoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) (s : (F.comp (CategoryTheory.coyoneda.obj X)).sections) :

            The cone of F corresponding to an element in (F ⋙ coyoneda.obj X).sections.

            Equations
            Instances For
              Equations

              The coyoneda embeddings jointly reflect limits.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

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

                Equations

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

                Equations
                Equations
                Equations
                Equations
                • CategoryTheory.yonedaFunctorReflectsLimits = inferInstance
                Equations
                • CategoryTheory.coyonedaFunctorReflectsLimits = inferInstance
                Equations
                Equations
                Equations
                • F.corepresentablePreservesLimitsOfShape J = { preservesLimit := fun {K : CategoryTheory.Functor J C} => inferInstance }
                Equations