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 : Opposite.unop X_1 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) => { obj := fun (Y : Cᵒᵖ) => Opposite.unop Y X, map := fun {X_1 Y : Cᵒᵖ} (f : X_1 Y) (g : (fun (Y : Cᵒᵖ) => Opposite.unop Y 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 = (Opposite.unop Y X)

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

See https://stacks.math.columbia.edu/tag/001O.

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 = (Opposite.unop X 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ᵒᵖ) => { obj := fun (Y : C) => Opposite.unop X Y, map := fun {X_1 Y : C} (f : X_1 Y) (g : (fun (Y : C) => Opposite.unop X 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 : Opposite.unop X 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) :
      def CategoryTheory.Yoneda.fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
      CategoryTheory.yoneda.FullyFaithful

      The Yoneda embedding is fully faithful.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem CategoryTheory.Yoneda.fullyFaithful_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : CategoryTheory.yoneda.obj X CategoryTheory.yoneda.obj Y) :
        CategoryTheory.Yoneda.fullyFaithful.preimage f = f.app (Opposite.op X) (CategoryTheory.CategoryStruct.id X)
        instance CategoryTheory.Yoneda.yoneda_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
        CategoryTheory.yoneda.Full

        The Yoneda embedding is full.

        See https://stacks.math.columbia.edu/tag/001P.

        Equations
        • =
        instance CategoryTheory.Yoneda.yoneda_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
        CategoryTheory.yoneda.Faithful

        The Yoneda embedding is faithful.

        See https://stacks.math.columbia.edu/tag/001P.

        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 : Opposite.unop X Z') :
          def CategoryTheory.Coyoneda.fullyFaithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
          CategoryTheory.coyoneda.FullyFaithful

          The co-Yoneda embedding is fully faithful.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem CategoryTheory.Coyoneda.fullyFaithful_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : CategoryTheory.coyoneda.obj X CategoryTheory.coyoneda.obj Y) :
            CategoryTheory.Coyoneda.fullyFaithful.preimage f = Quiver.Hom.op (f.app (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X)))
            def CategoryTheory.Coyoneda.preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : CategoryTheory.coyoneda.obj X CategoryTheory.coyoneda.obj Y) :
            X Y

            The morphism X ⟶ Y corresponding to a natural transformation coyoneda.obj X ⟶ coyoneda.obj Y.

            Equations
            Instances For
              instance CategoryTheory.Coyoneda.coyoneda_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
              CategoryTheory.coyoneda.Full
              Equations
              • =
              instance CategoryTheory.Coyoneda.coyoneda_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
              CategoryTheory.coyoneda.Faithful
              Equations
              • =
              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_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
                @[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
                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 https://stacks.math.columbia.edu/tag/001Q.

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

                    Hom(-,X) ≅ F via f

                  Instances
                    theorem CategoryTheory.Functor.Representable.has_representation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} [self : F.Representable] :
                    ∃ (X : C), Nonempty (CategoryTheory.yoneda.obj X F)

                    Hom(-,X) ≅ F via f

                    instance CategoryTheory.Functor.instRepresentableObjOppositeTypeYoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} :
                    (CategoryTheory.yoneda.obj X).Representable
                    Equations
                    • =

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

                    See https://stacks.math.columbia.edu/tag/001Q.

                    • has_corepresentation : ∃ (X : Cᵒᵖ), Nonempty (CategoryTheory.coyoneda.obj X F)

                      Hom(X,-) ≅ F via f

                    Instances
                      theorem CategoryTheory.Functor.Corepresentable.has_corepresentation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v₁)} [self : F.Corepresentable] :
                      ∃ (X : Cᵒᵖ), Nonempty (CategoryTheory.coyoneda.obj X F)

                      Hom(X,-) ≅ F via f

                      instance CategoryTheory.Functor.instCorepresentableObjOppositeTypeCoyoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} :
                      (CategoryTheory.coyoneda.obj X).Corepresentable
                      Equations
                      • =
                      noncomputable def CategoryTheory.Functor.reprX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [hF : F.Representable] :
                      C

                      The representing object for the representable functor F.

                      Equations
                      • F.reprX = .choose
                      Instances For
                        noncomputable def CategoryTheory.Functor.reprW {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [hF : F.Representable] :
                        CategoryTheory.yoneda.obj F.reprX F

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

                        Equations
                        • F.reprW = .some
                        Instances For
                          noncomputable def CategoryTheory.Functor.reprx {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [hF : F.Representable] :
                          F.obj (Opposite.op F.reprX)

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

                          Equations
                          Instances For
                            theorem CategoryTheory.Functor.reprW_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [hF : F.Representable] (X : Cᵒᵖ) (f : Opposite.unop X F.reprX) :
                            (F.reprW.app X).hom f = F.map f.op F.reprx
                            noncomputable def CategoryTheory.Functor.coreprX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [hF : F.Corepresentable] :
                            C

                            The representing object for the corepresentable functor F.

                            Equations
                            Instances For
                              noncomputable def CategoryTheory.Functor.coreprW {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [hF : F.Corepresentable] :
                              CategoryTheory.coyoneda.obj (Opposite.op F.coreprX) F

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

                              Equations
                              • F.coreprW = .some
                              Instances For
                                noncomputable def CategoryTheory.Functor.coreprx {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [hF : F.Corepresentable] :
                                F.obj F.coreprX

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

                                Equations
                                Instances For
                                  theorem CategoryTheory.Functor.coreprW_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [hF : F.Corepresentable] (X : C) (f : F.coreprX X) :
                                  (F.coreprW.app X).hom f = F.map f F.coreprx
                                  theorem CategoryTheory.representable_of_natIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) {G : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (i : F G) [F.Representable] :
                                  G.Representable
                                  theorem CategoryTheory.corepresentable_of_natIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) {G : CategoryTheory.Functor C (Type v₁)} (i : F G) [F.Corepresentable] :
                                  G.Corepresentable
                                  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
                                  • One or more equations did not get rendered due to their size.
                                  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 : Opposite.unop Y 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 (Opposite.unop X) 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_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)
                                    theorem CategoryTheory.hom_ext_yoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f : P Q} {g : P Q} (h : ∀ (X : C) (p : CategoryTheory.yoneda.obj X P), CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp p g) :
                                    f = g

                                    Two morphisms of presheaves of types P ⟶ Q coincide if the precompositions with morphisms yoneda.obj X ⟶ P agree.

                                    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 https://stacks.math.columbia.edu/tag/001P.

                                          Equations
                                          Instances For
                                            def CategoryTheory.curriedYonedaLemma {C : Type u₁} [CategoryTheory.SmallCategory C] :
                                            CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda CategoryTheory.evaluation Cᵒᵖ (Type u₁)

                                            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 the Yoneda lemma.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def CategoryTheory.yonedaOpCompYonedaObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) :
                                                CategoryTheory.yoneda.op.comp (CategoryTheory.yoneda.obj P) P.comp CategoryTheory.uliftFunctor.{u₁, v₁}

                                                Version of the Yoneda lemma where the presheaf is fixed but the argument varies.

                                                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
                                                    def CategoryTheory.coyonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)} :
                                                    (CategoryTheory.coyoneda.obj (Opposite.op X) F) F.obj X

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

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      theorem CategoryTheory.coyonedaEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)} (f : CategoryTheory.coyoneda.obj (Opposite.op X) F) :
                                                      CategoryTheory.coyonedaEquiv f = f.app X (CategoryTheory.CategoryStruct.id X)
                                                      @[simp]
                                                      theorem CategoryTheory.coyonedaEquiv_symm_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)} (x : F.obj X) (Y : C) (f : X Y) :
                                                      (CategoryTheory.coyonedaEquiv.symm x).app Y f = F.map f x
                                                      theorem CategoryTheory.coyonedaEquiv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {F : CategoryTheory.Functor C (Type v₁)} (f : CategoryTheory.coyoneda.obj (Opposite.op X) F) (g : X Y) :
                                                      F.map g (CategoryTheory.coyonedaEquiv f) = CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map g.op) f)
                                                      theorem CategoryTheory.coyonedaEquiv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)} {G : CategoryTheory.Functor C (Type v₁)} (α : CategoryTheory.coyoneda.obj (Opposite.op X) F) (β : F G) :
                                                      CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app X (CategoryTheory.coyonedaEquiv α)
                                                      theorem CategoryTheory.coyonedaEquiv_coyoneda_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X Y) :
                                                      CategoryTheory.coyonedaEquiv (CategoryTheory.coyoneda.map f.op) = f
                                                      theorem CategoryTheory.coyonedaEquiv_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.coyonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map f.op) (CategoryTheory.coyonedaEquiv.symm t)

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

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem CategoryTheory.coyonedaEvaluation_map_down (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P : C × CategoryTheory.Functor C (Type v₁)) (Q : C × CategoryTheory.Functor C (Type v₁)) (α : P Q) (x : (CategoryTheory.coyonedaEvaluation C).obj P) :
                                                        ((CategoryTheory.coyonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)

                                                        The "Coyoneda pairing" functor, which sends X : C and F : C ⥤ Type to coyoneda.rightOp.obj X ⟶ F, functorially in both X and F.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem CategoryTheory.coyonedaPairingExt (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : C × CategoryTheory.Functor C (Type v₁)} {x : (CategoryTheory.coyonedaPairing C).obj X} {y : (CategoryTheory.coyonedaPairing C).obj X} (w : ∀ (Y : C), x.app Y = y.app Y) :
                                                          x = y

                                                          A bijection (coyoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (unop X) which is a variant of coyonedaEquiv with heterogeneous universes.

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

                                                            The Coyoneda lemma asserts that the Coyoneda pairing (X : C, F : C ⥤ Type) ↦ (coyoneda.obj X ⟶ F) is naturally isomorphic to the evaluation (X, F) ↦ F.obj X.

                                                            See https://stacks.math.columbia.edu/tag/001P.

                                                            Equations
                                                            Instances For
                                                              def CategoryTheory.curriedCoyonedaLemma {C : Type u₁} [CategoryTheory.SmallCategory C] :
                                                              CategoryTheory.coyoneda.rightOp.comp CategoryTheory.coyoneda CategoryTheory.evaluation C (Type u₁)

                                                              The curried version of coyoneda lemma when C is small.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                def CategoryTheory.largeCurriedCoyonedaLemma {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                                                                CategoryTheory.coyoneda.rightOp.comp CategoryTheory.coyoneda (CategoryTheory.evaluation C (Type v₁)).comp ((CategoryTheory.whiskeringRight (CategoryTheory.Functor C (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj CategoryTheory.uliftFunctor.{u₁, v₁} )

                                                                The curried version of the Coyoneda lemma.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  def CategoryTheory.coyonedaCompYonedaObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor C (Type v₁)) :
                                                                  CategoryTheory.coyoneda.rightOp.comp (CategoryTheory.yoneda.obj P) P.comp CategoryTheory.uliftFunctor.{u₁, v₁}

                                                                  Version of the Coyoneda lemma where the presheaf is fixed but the argument varies.

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

                                                                    The curried version of coyoneda lemma when C is small.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      def CategoryTheory.yonedaMap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v₁, u_1} D] (F : CategoryTheory.Functor C D) (X : C) :
                                                                      CategoryTheory.yoneda.obj X F.op.comp (CategoryTheory.yoneda.obj (F.obj X))

                                                                      The natural transformation yoneda.obj X ⟶ F.op ⋙ yoneda.obj (F.obj X) when F : C ⥤ D and X : C.

                                                                      Equations
                                                                      Instances For