Documentation

Mathlib.CategoryTheory.Yoneda

The Yoneda embedding #

The Yoneda embedding as a functor yoneda : C ⥤ (Cᵒᵖ ⥤ Type v₁), along with an instance that it is FullyFaithful.

Also the Yoneda lemma, yonedaLemma : (yoneda_pairing C) ≅ (yoneda_evaluation C).

References #

@[simp]
theorem CategoryTheory.yoneda_obj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
∀ {X_1 Y : Cᵒᵖ} (f : X_1 Y) (g : X_1.unop X), (CategoryTheory.yoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp f.unop g
@[simp]
theorem CategoryTheory.yoneda_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
∀ {X Y : C} (f : X Y) (Y_1 : Cᵒᵖ) (g : ((fun (X : C) => { toPrefunctor := { obj := fun (Y : Cᵒᵖ) => Y.unop X, map := fun {X_1 Y : Cᵒᵖ} (f : X_1 Y) (g : (fun (Y : Cᵒᵖ) => Y.unop X) X_1) => CategoryTheory.CategoryStruct.comp f.unop g }, map_id := , map_comp := }) X).obj Y_1), (CategoryTheory.yoneda.map f).app Y_1 g = CategoryTheory.CategoryStruct.comp g f
@[simp]
theorem CategoryTheory.yoneda_obj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (Y : Cᵒᵖ) :
(CategoryTheory.yoneda.obj X).obj Y = (Y.unop X)

The Yoneda embedding, as a functor from C into presheaves on C.

See .

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.coyoneda_obj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) (Y : C) :
    (CategoryTheory.coyoneda.obj X).obj Y = (X.unop Y)
    @[simp]
    theorem CategoryTheory.coyoneda_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
    ∀ {X Y : Cᵒᵖ} (f : X Y) (Y_1 : C) (g : ((fun (X : Cᵒᵖ) => { toPrefunctor := { obj := fun (Y : C) => X.unop Y, map := fun {X_1 Y : C} (f : X_1 Y) (g : (fun (Y : C) => X.unop Y) X_1) => CategoryTheory.CategoryStruct.comp g f }, map_id := , map_comp := }) X).obj Y_1), (CategoryTheory.coyoneda.map f).app Y_1 g = CategoryTheory.CategoryStruct.comp f.unop g
    @[simp]
    theorem CategoryTheory.coyoneda_obj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) :
    ∀ {X_1 Y : C} (f : X_1 Y) (g : X.unop X_1), (CategoryTheory.coyoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp g f

    The co-Yoneda embedding, as a functor from Cᵒᵖ into co-presheaves on C.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem CategoryTheory.Yoneda.obj_map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : Opposite.op X Opposite.op Y) :
      (CategoryTheory.yoneda.obj X).map f (CategoryTheory.CategoryStruct.id X) = (CategoryTheory.yoneda.map f.unop).app (Opposite.op Y) (CategoryTheory.CategoryStruct.id Y)
      @[simp]
      theorem CategoryTheory.Yoneda.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (α : CategoryTheory.yoneda.obj X CategoryTheory.yoneda.obj Y) {Z : C} {Z' : C} (f : Z Z') (h : Z' X) :

      The Yoneda embedding is full.

      See .

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

      The Yoneda embedding is faithful.

      See .

      Equations
      • =
      def CategoryTheory.Yoneda.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (Y : C) (p : {Z : C} → (Z X)(Z Y)) (q : {Z : C} → (Z Y)(Z X)) (h₁ : ∀ {Z : C} (f : Z X), q (p f) = f) (h₂ : ∀ {Z : C} (f : Z Y), p (q f) = f) (n : ∀ {Z Z' : C} (f : Z' Z) (g : Z X), p (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp f (p g)) :
      X Y

      Extensionality via Yoneda. The typical usage would be

      -- Goal is `X ≅ Y`
      apply yoneda.ext,
      -- Goals are now functions `(Z ⟶ X) → (Z ⟶ Y)`, `(Z ⟶ Y) → (Z ⟶ X)`, and the fact that these
      -- functions are inverses and natural in `Z`.
      
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem CategoryTheory.Yoneda.isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) [CategoryTheory.IsIso (CategoryTheory.yoneda.map f)] :

        If yoneda.map f is an isomorphism, so was f.

        @[simp]
        theorem CategoryTheory.Coyoneda.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (α : CategoryTheory.coyoneda.obj X CategoryTheory.coyoneda.obj Y) {Z : C} {Z' : C} (f : Z' Z) (h : X.unop Z') :
        Equations
        • One or more equations did not get rendered due to their size.
        theorem CategoryTheory.Coyoneda.isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) [CategoryTheory.IsIso (CategoryTheory.coyoneda.map f)] :

        If coyoneda.map f is an isomorphism, so was f.

        The identity functor on Type is isomorphic to the coyoneda functor coming from PUnit.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Coyoneda.objOpOp_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (X : Cᵒᵖ) :
          ∀ (a : (CategoryTheory.yoneda.obj X✝).obj X), (CategoryTheory.Coyoneda.objOpOp X✝).inv.app X a = (CategoryTheory.opEquiv (Opposite.op X✝) X).symm a
          @[simp]
          theorem CategoryTheory.Coyoneda.objOpOp_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (X : Cᵒᵖ) :
          ∀ (a : (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X✝))).obj X), (CategoryTheory.Coyoneda.objOpOp X✝).hom.app X a = (CategoryTheory.opEquiv (Opposite.op X✝) X) a
          def CategoryTheory.Coyoneda.objOpOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) :
          CategoryTheory.coyoneda.obj (Opposite.op (Opposite.op X)) CategoryTheory.yoneda.obj X

          Taking the unop of morphisms is a natural isomorphism.

          Equations
          Instances For

            A functor F : Cᵒᵖ ⥤ Type v₁ is representable if there is object X so F ≅ yoneda.obj X.

            See .

            • has_representation : ∃ (X : C), ∃ (f : CategoryTheory.yoneda.obj X F), CategoryTheory.IsIso f

              Hom(-,X) ≅ F via f

            Instances

              A functor F : C ⥤ Type v₁ is corepresentable if there is object X so F ≅ coyoneda.obj X.

              See .

              Instances

                The representing object for the representable functor F.

                Equations
                Instances For

                  The (forward direction of the) isomorphism witnessing F is representable.

                  Equations
                  Instances For

                    The representing element for the representable functor F, sometimes called the universal element of the functor.

                    Equations
                    Instances For

                      An isomorphism between F and a functor of the form C(-, F.repr_X). Note the components F.repr_w.app X definitionally have type (X.unop ⟶ F.repr_X) ≅ F.obj X.

                      Equations
                      Instances For

                        The representing object for the corepresentable functor F.

                        Equations
                        Instances For

                          The (forward direction of the) isomorphism witnessing F is corepresentable.

                          Equations
                          Instances For

                            The representing element for the corepresentable functor F, sometimes called the universal element of the functor.

                            Equations
                            Instances For

                              An isomorphism between F and a functor of the form C(F.corepr X, -). Note the components F.corepr_w.app X definitionally have type F.corepr_X ⟶ X ≅ F.obj X.

                              Equations
                              Instances For

                                The "Yoneda evaluation" functor, which sends X : Cᵒᵖ and F : Cᵒᵖ ⥤ Type to F.obj X, functorially in both X and F.

                                Equations
                                Instances For
                                  @[simp]

                                  The "Yoneda pairing" functor, which sends X : Cᵒᵖ and F : Cᵒᵖ ⥤ Type to yoneda.op.obj X ⟶ F, functorially in both X and F.

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

                                    A bijection (yoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (op X) which is a variant of yonedaEquiv with heterogeneous universes.

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

                                      The Yoneda lemma asserts that the Yoneda pairing (X : Cᵒᵖ, F : Cᵒᵖ ⥤ Type) ↦ (yoneda.obj (unop X) ⟶ F) is naturally isomorphic to the evaluation (X, F) ↦ F.obj X.

                                      See .

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.yonedaSections_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) :
                                        ∀ (a : (CategoryTheory.yonedaEvaluation C).obj (Opposite.op X, F)) (X_1 : Cᵒᵖ) (a_1 : ((CategoryTheory.Functor.prod CategoryTheory.yoneda.op (CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ (Type v₁)))).obj (Opposite.op X, F)).1.unop.obj X_1), ((CategoryTheory.yonedaSections X F).inv a).app X_1 a_1 = F.map a_1.op a.down
                                        def CategoryTheory.yonedaSections {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) :
                                        (CategoryTheory.yoneda.obj X F) ULift.{u₁, v₁} (F.obj (Opposite.op X))

                                        The isomorphism between yoneda.obj X ⟶ F and F.obj (op X) (we need to insert a ULift to get the universes right!) given by the Yoneda lemma.

                                        Equations
                                        Instances For
                                          def CategoryTheory.yonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} :
                                          (CategoryTheory.yoneda.obj X F) F.obj (Opposite.op X)

                                          We have a type-level equivalence between natural transformations from the yoneda embedding and elements of F.obj X, without any universe switching.

                                          Equations
                                          Instances For
                                            theorem CategoryTheory.yonedaEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X F) :
                                            CategoryTheory.yonedaEquiv f = f.app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)
                                            @[simp]
                                            theorem CategoryTheory.yonedaEquiv_symm_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Y.unop X) :
                                            (CategoryTheory.yonedaEquiv.symm x).app Y f = F.map f.op x
                                            theorem CategoryTheory.yonedaEquiv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X F) (g : Y X) :
                                            F.map g.op (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g) f)
                                            theorem CategoryTheory.yonedaEquiv_naturality' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X.unop F) (g : X Y) :
                                            F.map g (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g.unop) f)
                                            theorem CategoryTheory.yonedaEquiv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {G : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (α : CategoryTheory.yoneda.obj X F) (β : F G) :
                                            CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app (Opposite.op X) (CategoryTheory.yonedaEquiv α)
                                            theorem CategoryTheory.yonedaEquiv_comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {G : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (α : CategoryTheory.yoneda.obj X.unop F) (β : F G) :
                                            CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app X (CategoryTheory.yonedaEquiv α)
                                            @[simp]
                                            theorem CategoryTheory.yonedaEquiv_yoneda_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :
                                            CategoryTheory.yonedaEquiv (CategoryTheory.yoneda.map f) = f
                                            theorem CategoryTheory.yonedaEquiv_symm_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (t : F.obj X) :
                                            CategoryTheory.yonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f.unop) (CategoryTheory.yonedaEquiv.symm t)
                                            def CategoryTheory.yonedaSectionsSmall {C : Type u₁} [CategoryTheory.SmallCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type u₁)) :
                                            (CategoryTheory.yoneda.obj X F) F.obj (Opposite.op X)

                                            When C is a small category, we can restate the isomorphism from yoneda_sections without having to change universes.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem CategoryTheory.yonedaSectionsSmall_hom {C : Type u₁} [CategoryTheory.SmallCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (f : CategoryTheory.yoneda.obj X F) :
                                              (CategoryTheory.yonedaSectionsSmall X F).hom f = f.app { unop := X } (CategoryTheory.CategoryStruct.id { unop := X }.unop)
                                              @[simp]
                                              theorem CategoryTheory.yonedaSectionsSmall_inv_app_apply {C : Type u₁} [CategoryTheory.SmallCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ (Type u₁)) (t : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Y.unop X) :
                                              ((CategoryTheory.yonedaSectionsSmall X F).inv t).app Y f = F.map f.op t

                                              The curried version of yoneda lemma when C is small.

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

                                                The curried version of yoneda lemma when C is small.

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