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 #

source
def CategoryTheory.yoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ (Type v₁))

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
    source
    @[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)
    source
    @[simp]
    theorem CategoryTheory.yoneda_obj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (g : Opposite.unop X✝ ⟶ X) :
    (CategoryTheory.yoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp f.unop g
    source
    @[simp]
    theorem CategoryTheory.yoneda_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x✝ : 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 x✝) :
    (CategoryTheory.yoneda.map f).app x✝ g = CategoryTheory.CategoryStruct.comp g f
    source
    def CategoryTheory.coyoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
    CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (Type v₁))

    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
      source
      @[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)
      source
      @[simp]
      theorem CategoryTheory.coyoneda_obj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : Cᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (g : Opposite.unop X ⟶ X✝) :
      (CategoryTheory.coyoneda.obj X).map f g = CategoryTheory.CategoryStruct.comp g f
      source
      @[simp]
      theorem CategoryTheory.coyoneda_map_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (x✝ : 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 x✝) :
      (CategoryTheory.coyoneda.map f).app x✝ g = CategoryTheory.CategoryStruct.comp f.unop g
      source
      theorem CategoryTheory.Yoneda.obj_map_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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)
      source
      @[simp]
      theorem CategoryTheory.Yoneda.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (α : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y) {Z Z' : C} (f : Z ⟶ Z') (h : Z' ⟶ X) :
      CategoryTheory.CategoryStruct.comp f (α.app (Opposite.op Z') h) = α.app (Opposite.op Z) (CategoryTheory.CategoryStruct.comp f h)
      source
      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
        source
        theorem CategoryTheory.Yoneda.fullyFaithful_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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)
        source
        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
        • ⋯ = ⋯
        source
        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
        • ⋯ = ⋯
        source
        def CategoryTheory.Yoneda.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X 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
          source
          theorem CategoryTheory.Yoneda.isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (CategoryTheory.yoneda.map f)] :
          CategoryTheory.IsIso f

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

          source
          @[simp]
          theorem CategoryTheory.Coyoneda.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (α : CategoryTheory.coyoneda.obj X ⟶ CategoryTheory.coyoneda.obj Y) {Z Z' : C} (f : Z' ⟶ Z) (h : Opposite.unop X ⟶ Z') :
          CategoryTheory.CategoryStruct.comp (α.app Z' h) f = α.app Z (CategoryTheory.CategoryStruct.comp h f)
          source
          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
            source
            theorem CategoryTheory.Coyoneda.fullyFaithful_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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)))
            source
            def CategoryTheory.Coyoneda.preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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
              source
              instance CategoryTheory.Coyoneda.coyoneda_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
              CategoryTheory.coyoneda.Full
              Equations
              • ⋯ = ⋯
              source
              instance CategoryTheory.Coyoneda.coyoneda_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
              CategoryTheory.coyoneda.Faithful
              Equations
              • ⋯ = ⋯
              source
              theorem CategoryTheory.Coyoneda.isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y) [CategoryTheory.IsIso (CategoryTheory.coyoneda.map f)] :
              CategoryTheory.IsIso f

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

              source
              def CategoryTheory.Coyoneda.punitIso :
              CategoryTheory.coyoneda.obj (Opposite.op PUnit.{v₁ + 1} ) ≅ CategoryTheory.Functor.id (Type v₁)

              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
                source
                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
                  source
                  @[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✝
                  source
                  @[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✝
                  source
                  structure CategoryTheory.Functor.RepresentableBy {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) (Y : C) :
                  Type (max (max u₁ v) v₁)

                  The data which expresses that a functor F : Cᵒᵖ ⥤ Type v is representable by Y : C.

                  Instances For
                    source
                    def CategoryTheory.Functor.RepresentableBy.ofIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F F' : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) (e' : F ≅ F') :
                    F'.RepresentableBy Y

                    If F ≅ F', and F is representable, then F' is representable.

                    Equations
                    • e.ofIso e' = { homEquiv := fun {X : C} => e.homEquiv.trans (e'.app (Opposite.op X)).toEquiv, homEquiv_comp := ⋯ }
                    Instances For
                      source
                      structure CategoryTheory.Functor.CorepresentableBy {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) (X : C) :
                      Type (max (max u₁ v) v₁)

                      The data which expresses that a functor F : C ⥤ Type v is corepresentable by X : C.

                      Instances For
                        source
                        def CategoryTheory.Functor.CorepresentableBy.ofIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F F' : CategoryTheory.Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) (e' : F ≅ F') :
                        F'.CorepresentableBy X

                        If F ≅ F', and F is corepresentable, then F' is corepresentable.

                        Equations
                        • e.ofIso e' = { homEquiv := fun {X_1 : C} => e.homEquiv.trans (e'.app X_1).toEquiv, homEquiv_comp := ⋯ }
                        Instances For
                          source
                          theorem CategoryTheory.Functor.RepresentableBy.homEquiv_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) {X : C} (f : X ⟶ Y) :
                          e.homEquiv f = F.map f.op (e.homEquiv (CategoryTheory.CategoryStruct.id Y))
                          source
                          theorem CategoryTheory.Functor.CorepresentableBy.homEquiv_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) {Y : C} (f : X ⟶ Y) :
                          e.homEquiv f = F.map f (e.homEquiv (CategoryTheory.CategoryStruct.id X))
                          source
                          theorem CategoryTheory.Functor.RepresentableBy.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} {e e' : F.RepresentableBy Y} (h : e.homEquiv (CategoryTheory.CategoryStruct.id Y) = e'.homEquiv (CategoryTheory.CategoryStruct.id Y)) :
                          e = e'
                          source
                          theorem CategoryTheory.Functor.CorepresentableBy.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} {e e' : F.CorepresentableBy X} (h : e.homEquiv (CategoryTheory.CategoryStruct.id X) = e'.homEquiv (CategoryTheory.CategoryStruct.id X)) :
                          e = e'
                          source
                          def CategoryTheory.Functor.representableByEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {Y : C} :
                          F.RepresentableBy Y ≃ (CategoryTheory.yoneda.obj Y ≅ F)

                          The obvious bijection F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F) when F : Cᵒᵖ ⥤ Type v₁ and [Category.{v₁} C].

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            def CategoryTheory.Functor.RepresentableBy.toIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {Y : C} (e : F.RepresentableBy Y) :
                            CategoryTheory.yoneda.obj Y ≅ F

                            The isomorphism yoneda.obj Y ≅ F induced by e : F.RepresentableBy Y.

                            Equations
                            • e.toIso = CategoryTheory.Functor.representableByEquiv e
                            Instances For
                              source
                              def CategoryTheory.Functor.corepresentableByEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v₁)} {X : C} :
                              F.CorepresentableBy X ≃ (CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F)

                              The obvious bijection F.CorepresentableBy X ≃ (yoneda.obj Y ≅ F) when F : C ⥤ Type v₁ and [Category.{v₁} C].

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def CategoryTheory.Functor.CorepresentableBy.toIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v₁)} {X : C} (e : F.CorepresentableBy X) :
                                CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F

                                The isomorphism coyoneda.obj (op X) ≅ F induced by e : F.CorepresentableBy X.

                                Equations
                                • e.toIso = CategoryTheory.Functor.corepresentableByEquiv e
                                Instances For
                                  source
                                  class CategoryTheory.Functor.IsRepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) :
                                  Prop

                                  A functor F : Cᵒᵖ ⥤ Type v is representable if there is oan bject Y with a structure F.RepresentableBy Y, i.e. there is a natural bijection (X ⟶ Y) ≃ F.obj (op X), which may also be rephrased as a natural isomorphism yoneda.obj X ≅ F when Category.{v} C.

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

                                  • has_representation : ∃ (Y : C), Nonempty (F.RepresentableBy Y)
                                  Instances
                                    source
                                    @[deprecated CategoryTheory.Functor.IsRepresentable]
                                    def CategoryTheory.Functor.Representable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) :
                                    Prop

                                    Alias of CategoryTheory.Functor.IsRepresentable.

                                    A functor F : Cᵒᵖ ⥤ Type v is representable if there is oan bject Y with a structure F.RepresentableBy Y, i.e. there is a natural bijection (X ⟶ Y) ≃ F.obj (op X), which may also be rephrased as a natural isomorphism yoneda.obj X ≅ F when Category.{v} C.

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

                                    Equations
                                    Instances For
                                      source
                                      theorem CategoryTheory.Functor.RepresentableBy.isRepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C} (e : F.RepresentableBy Y) :
                                      F.IsRepresentable
                                      source
                                      theorem CategoryTheory.Functor.IsRepresentable.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {X : C} (e : CategoryTheory.yoneda.obj X ≅ F) :
                                      F.IsRepresentable

                                      Alternative constructure for F.IsRepresentable, which takes as an input an isomorphism yoneda.obj X ≅ F.

                                      source
                                      instance CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} :
                                      (CategoryTheory.yoneda.obj X).IsRepresentable
                                      Equations
                                      • ⋯ = ⋯
                                      source
                                      class CategoryTheory.Functor.IsCorepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) :
                                      Prop

                                      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 (F.CorepresentableBy X)
                                      Instances
                                        source
                                        @[deprecated CategoryTheory.Functor.IsCorepresentable]
                                        def CategoryTheory.Functor.Corepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) :
                                        Prop

                                        Alias of CategoryTheory.Functor.IsCorepresentable.

                                        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.

                                        Equations
                                        Instances For
                                          source
                                          theorem CategoryTheory.Functor.CorepresentableBy.isCorepresentable {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) :
                                          F.IsCorepresentable
                                          source
                                          theorem CategoryTheory.Functor.IsCorepresentable.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v₁)} {X : C} (e : CategoryTheory.coyoneda.obj (Opposite.op X) ≅ F) :
                                          F.IsCorepresentable

                                          Alternative constructure for F.IsCorepresentable, which takes as an input an isomorphism coyoneda.obj (op X) ≅ F.

                                          source
                                          instance CategoryTheory.Functor.instIsCorepresentableObjOppositeTypeCoyoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} :
                                          (CategoryTheory.coyoneda.obj X).IsCorepresentable
                                          Equations
                                          • ⋯ = ⋯
                                          source
                                          noncomputable def CategoryTheory.Functor.reprX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) [hF : F.IsRepresentable] :
                                          C

                                          The representing object for the representable functor F.

                                          Equations
                                          • F.reprX = ⋯.choose
                                          Instances For
                                            source
                                            noncomputable def CategoryTheory.Functor.representableBy {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) [hF : F.IsRepresentable] :
                                            F.RepresentableBy F.reprX

                                            A chosen term in F.RepresentableBy (reprX F) when F.IsRepresentable holds.

                                            Equations
                                            • F.representableBy = ⋯.some
                                            Instances For
                                              source
                                              noncomputable def CategoryTheory.Functor.reprx {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) [hF : F.IsRepresentable] :
                                              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
                                                source
                                                noncomputable def CategoryTheory.Functor.reprW {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [F.IsRepresentable] :
                                                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.reprX) ≅ F.obj X.

                                                Equations
                                                • F.reprW = F.representableBy.toIso
                                                Instances For
                                                  source
                                                  theorem CategoryTheory.Functor.reprW_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) [F.IsRepresentable] (X : Cᵒᵖ) (f : Opposite.unop X ⟶ F.reprX) :
                                                  F.reprW.hom.app X f = F.map f.op F.reprx
                                                  source
                                                  noncomputable def CategoryTheory.Functor.coreprX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) [hF : F.IsCorepresentable] :
                                                  C

                                                  The representing object for the corepresentable functor F.

                                                  Equations
                                                  • F.coreprX = ⋯.choose
                                                  Instances For
                                                    source
                                                    noncomputable def CategoryTheory.Functor.corepresentableBy {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v)) [hF : F.IsCorepresentable] :
                                                    F.CorepresentableBy F.coreprX

                                                    A chosen term in F.CorepresentableBy (coreprX F) when F.IsCorepresentable holds.

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

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

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

                                                        An isomorphism between a corepresentable 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 = F.corepresentableBy.toIso
                                                        Instances For
                                                          source
                                                          theorem CategoryTheory.Functor.coreprW_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type v₁)) [F.IsCorepresentable] (X : C) (f : F.coreprX ⟶ X) :
                                                          F.coreprW.hom.app X f = F.map f F.coreprx
                                                          source
                                                          theorem CategoryTheory.isRepresentable_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.IsRepresentable] :
                                                          G.IsRepresentable
                                                          source
                                                          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.IsCorepresentable] :
                                                          G.IsCorepresentable
                                                          source
                                                          instance CategoryTheory.instIsCorepresentableIdType :
                                                          (CategoryTheory.Functor.id (Type v₁)).IsCorepresentable
                                                          Equations
                                                          source
                                                          instance CategoryTheory.prodCategoryInstance1 (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
                                                          CategoryTheory.Category.{max u₁ v₁, max u₁ (max (v₁ + 1) u₁) v₁} (CategoryTheory.Functor Cᵒᵖ (Type v₁) × Cᵒᵖ)
                                                          Equations
                                                          source
                                                          instance CategoryTheory.prodCategoryInstance2 (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
                                                          CategoryTheory.Category.{max u₁ v₁, max (max (max (v₁ + 1) u₁) v₁) u₁} (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁))
                                                          Equations
                                                          source
                                                          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
                                                            source
                                                            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)
                                                            source
                                                            @[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
                                                            source
                                                            theorem CategoryTheory.yonedaEquiv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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)

                                                            See also yonedaEquiv_naturality' for a more general version.

                                                            source
                                                            theorem CategoryTheory.yonedaEquiv_naturality' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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)

                                                            Variant of yonedaEquiv_naturality with general g. This is technically strictly more general than yonedaEquiv_naturality, but yonedaEquiv_naturality is sometimes preferable because it can avoid the "motive is not type correct" error.

                                                            source
                                                            theorem CategoryTheory.yonedaEquiv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (α : CategoryTheory.yoneda.obj X ⟶ F) (β : F ⟶ G) :
                                                            CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app (Opposite.op X) (CategoryTheory.yonedaEquiv α)
                                                            source
                                                            theorem CategoryTheory.yonedaEquiv_yoneda_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
                                                            CategoryTheory.yonedaEquiv (CategoryTheory.yoneda.map f) = f
                                                            source
                                                            theorem CategoryTheory.yonedaEquiv_symm_naturality_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X X' : C} (f : X' ⟶ X) (F : CategoryTheory.Functor Cᵒᵖ (Type v₁)) (x : F.obj (Opposite.op X)) :
                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) (CategoryTheory.yonedaEquiv.symm x) = CategoryTheory.yonedaEquiv.symm (F.map f.op x)
                                                            source
                                                            theorem CategoryTheory.yonedaEquiv_symm_naturality_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X : C) {F F' : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : F ⟶ F') (x : F.obj (Opposite.op X)) :
                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.yonedaEquiv.symm x) f = CategoryTheory.yonedaEquiv.symm (f.app (Opposite.op X) x)
                                                            source
                                                            theorem CategoryTheory.map_yonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f : CategoryTheory.yoneda.obj X ⟶ F) (g : Y ⟶ X) :
                                                            F.map g.op (CategoryTheory.yonedaEquiv f) = f.app (Opposite.op Y) g

                                                            See also map_yonedaEquiv' for a more general version.

                                                            source
                                                            theorem CategoryTheory.map_yonedaEquiv' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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) = f.app Y g.unop

                                                            Variant of map_yonedaEquiv with general g. This is technically strictly more general than map_yonedaEquiv, but map_yonedaEquiv is sometimes preferable because it can avoid the "motive is not type correct" error.

                                                            source
                                                            theorem CategoryTheory.yonedaEquiv_symm_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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)
                                                            source
                                                            theorem CategoryTheory.hom_ext_yoneda {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f 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.

                                                            source
                                                            def CategoryTheory.yonedaEvaluation (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
                                                            CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type (max u₁ v₁))

                                                            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
                                                              source
                                                              @[simp]
                                                              theorem CategoryTheory.yonedaEvaluation_map_down (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (α : P ⟶ Q) (x : (CategoryTheory.yonedaEvaluation C).obj P) :
                                                              ((CategoryTheory.yonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
                                                              source
                                                              def CategoryTheory.yonedaPairing (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
                                                              CategoryTheory.Functor (Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (Type (max u₁ v₁))

                                                              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
                                                                source
                                                                theorem CategoryTheory.yonedaPairingExt (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)} {x y : (CategoryTheory.yonedaPairing C).obj X} (w : ∀ (Y : Cᵒᵖ), x.app Y = y.app Y) :
                                                                x = y
                                                                source
                                                                @[simp]
                                                                theorem CategoryTheory.yonedaPairing_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : Cᵒᵖ × CategoryTheory.Functor Cᵒᵖ (Type v₁)) (α : P ⟶ Q) (β : (CategoryTheory.yonedaPairing C).obj P) :
                                                                (CategoryTheory.yonedaPairing C).map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map α.1.unop) (CategoryTheory.CategoryStruct.comp β α.2)
                                                                source
                                                                def CategoryTheory.yonedaCompUliftFunctorEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ w))) (X : C) :
                                                                ((CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{w, v₁} ⟶ F) ≃ F.obj (Opposite.op X)

                                                                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
                                                                  source
                                                                  def CategoryTheory.yonedaLemma (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
                                                                  CategoryTheory.yonedaPairing C ≅ CategoryTheory.yonedaEvaluation C

                                                                  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
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    source
                                                                    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
                                                                      source
                                                                      def CategoryTheory.largeCurriedYonedaLemma {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] :
                                                                      CategoryTheory.yoneda.op.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 Yoneda lemma.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        source
                                                                        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
                                                                          source
                                                                          def CategoryTheory.curriedYonedaLemma' {C : Type u₁} [CategoryTheory.SmallCategory C] :
                                                                          CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type u₁))ᵒᵖ (Type u₁)).obj CategoryTheory.yoneda.op) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor 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
                                                                            source
                                                                            theorem CategoryTheory.isIso_of_yoneda_map_bijective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (T : C), Function.Bijective fun (x : T ⟶ X) => CategoryTheory.CategoryStruct.comp x f) :
                                                                            CategoryTheory.IsIso f
                                                                            source
                                                                            theorem CategoryTheory.isIso_iff_yoneda_map_bijective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
                                                                            CategoryTheory.IsIso f ↔ ∀ (T : C), Function.Bijective fun (x : T ⟶ X) => CategoryTheory.CategoryStruct.comp x f
                                                                            source
                                                                            theorem CategoryTheory.isIso_iff_isIso_yoneda_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
                                                                            CategoryTheory.IsIso f ↔ ∀ (c : C), CategoryTheory.IsIso ((CategoryTheory.yoneda.map f).app (Opposite.op c))
                                                                            source
                                                                            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
                                                                              source
                                                                              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)
                                                                              source
                                                                              @[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
                                                                              source
                                                                              theorem CategoryTheory.coyonedaEquiv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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)
                                                                              source
                                                                              theorem CategoryTheory.coyonedaEquiv_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {F G : CategoryTheory.Functor C (Type v₁)} (α : CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) (β : F ⟶ G) :
                                                                              CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp α β) = β.app X (CategoryTheory.coyonedaEquiv α)
                                                                              source
                                                                              theorem CategoryTheory.coyonedaEquiv_coyoneda_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
                                                                              CategoryTheory.coyonedaEquiv (CategoryTheory.coyoneda.map f.op) = f
                                                                              source
                                                                              theorem CategoryTheory.map_coyonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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) = f.app Y g
                                                                              source
                                                                              theorem CategoryTheory.coyonedaEquiv_symm_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X 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)
                                                                              source
                                                                              def CategoryTheory.coyonedaEvaluation (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
                                                                              CategoryTheory.Functor (C × CategoryTheory.Functor C (Type v₁)) (Type (max u₁ v₁))

                                                                              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
                                                                                source
                                                                                @[simp]
                                                                                theorem CategoryTheory.coyonedaEvaluation_map_down (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P 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)
                                                                                source
                                                                                def CategoryTheory.coyonedaPairing (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
                                                                                CategoryTheory.Functor (C × CategoryTheory.Functor C (Type v₁)) (Type (max u₁ v₁))

                                                                                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
                                                                                  source
                                                                                  theorem CategoryTheory.coyonedaPairingExt (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X : C × CategoryTheory.Functor C (Type v₁)} {x y : (CategoryTheory.coyonedaPairing C).obj X} (w : ∀ (Y : C), x.app Y = y.app Y) :
                                                                                  x = y
                                                                                  source
                                                                                  @[simp]
                                                                                  theorem CategoryTheory.coyonedaPairing_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (P Q : C × CategoryTheory.Functor C (Type v₁)) (α : P ⟶ Q) (β : (CategoryTheory.coyonedaPairing C).obj P) :
                                                                                  (CategoryTheory.coyonedaPairing C).map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map α.1.op) (CategoryTheory.CategoryStruct.comp β α.2)
                                                                                  source
                                                                                  def CategoryTheory.coyonedaCompUliftFunctorEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor C (Type (max v₁ w))) (X : Cᵒᵖ) :
                                                                                  ((CategoryTheory.coyoneda.obj X).comp CategoryTheory.uliftFunctor.{w, v₁} ⟶ F) ≃ F.obj (Opposite.unop X)

                                                                                  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
                                                                                    source
                                                                                    def CategoryTheory.coyonedaLemma (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] :
                                                                                    CategoryTheory.coyonedaPairing C ≅ CategoryTheory.coyonedaEvaluation C

                                                                                    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
                                                                                      source
                                                                                      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
                                                                                        source
                                                                                        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
                                                                                          source
                                                                                          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
                                                                                            source
                                                                                            def CategoryTheory.curriedCoyonedaLemma' {C : Type u₁} [CategoryTheory.SmallCategory C] :
                                                                                            CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft C (CategoryTheory.Functor C (Type u₁))ᵒᵖ (Type u₁)).obj CategoryTheory.coyoneda.rightOp) ≅ CategoryTheory.Functor.id (CategoryTheory.Functor 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
                                                                                              source
                                                                                              theorem CategoryTheory.isIso_of_coyoneda_map_bijective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (T : C), Function.Bijective fun (x : Y ⟶ T) => CategoryTheory.CategoryStruct.comp f x) :
                                                                                              CategoryTheory.IsIso f
                                                                                              source
                                                                                              theorem CategoryTheory.isIso_iff_coyoneda_map_bijective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
                                                                                              CategoryTheory.IsIso f ↔ ∀ (T : C), Function.Bijective fun (x : Y ⟶ T) => CategoryTheory.CategoryStruct.comp f x
                                                                                              source
                                                                                              theorem CategoryTheory.isIso_iff_isIso_coyoneda_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
                                                                                              CategoryTheory.IsIso f ↔ ∀ (c : C), CategoryTheory.IsIso ((CategoryTheory.coyoneda.map f.op).app c)
                                                                                              source
                                                                                              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
                                                                                                source
                                                                                                @[simp]
                                                                                                theorem CategoryTheory.yonedaMap_app_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1} [CategoryTheory.Category.{v₁, u_1} D] (F : CategoryTheory.Functor C D) {Y : C} {X : Cᵒᵖ} (f : Opposite.unop X ⟶ Y) :
                                                                                                (CategoryTheory.yonedaMap F Y).app X f = F.map f
                                                                                                source
                                                                                                def CategoryTheory.Functor.FullyFaithful.homNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) :
                                                                                                F.op.comp ((CategoryTheory.yoneda.obj (F.obj X)).comp CategoryTheory.uliftFunctor.{v₁, v₂} ) ≅ (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{v₂, v₁}

                                                                                                FullyFaithful.homEquiv as a natural isomorphism.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  source
                                                                                                  @[simp]
                                                                                                  theorem CategoryTheory.Functor.FullyFaithful.homNatIso_inv_app_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : ((CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{v₂, v₁} ).obj X✝) :
                                                                                                  ((hF.homNatIso X).inv.app X✝ a✝).down = F.map a✝.down
                                                                                                  source
                                                                                                  @[simp]
                                                                                                  theorem CategoryTheory.Functor.FullyFaithful.homNatIso_hom_app_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp ((CategoryTheory.yoneda.obj (F.obj X)).comp CategoryTheory.uliftFunctor.{v₁, v₂} )).obj X✝) :
                                                                                                  ((hF.homNatIso X).hom.app X✝ a✝).down = hF.preimage a✝.down
                                                                                                  source
                                                                                                  def CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{max v₁ v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) :
                                                                                                  F.op.comp (CategoryTheory.yoneda.obj (F.obj X)) ≅ (CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{v₂, v₁}

                                                                                                  FullyFaithful.homEquiv as a natural isomorphism.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    source
                                                                                                    @[simp]
                                                                                                    theorem CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight_hom_app_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{max v₁ v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp (CategoryTheory.yoneda.obj (F.obj X))).obj X✝) :
                                                                                                    ((hF.homNatIsoMaxRight X).hom.app X✝ a✝).down = hF.preimage a✝
                                                                                                    source
                                                                                                    @[simp]
                                                                                                    theorem CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{max v₁ v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : ((CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{v₂, v₁} ).obj X✝) :
                                                                                                    (hF.homNatIsoMaxRight X).inv.app X✝ a✝ = F.map a✝.down
                                                                                                    source
                                                                                                    def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) :
                                                                                                    F.comp (CategoryTheory.yoneda.comp (((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₂)).obj F.op).comp ((CategoryTheory.whiskeringRight Cᵒᵖ (Type v₂) (Type (max v₂ v₁))).obj CategoryTheory.uliftFunctor.{v₁, v₂} ))) ≅ CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringRight Cᵒᵖ (Type v₁) (Type (max v₂ v₁))).obj CategoryTheory.uliftFunctor.{v₂, v₁} )

                                                                                                    FullyFaithful.homEquiv as a natural isomorphism.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft_inv_app_app_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : ((CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{v₂, v₁} ).obj X✝) :
                                                                                                      ((hF.compYonedaCompWhiskeringLeft.inv.app X).app X✝ a✝).down = F.map a✝.down
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeft_hom_app_app_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp ((CategoryTheory.yoneda.obj (F.obj X)).comp CategoryTheory.uliftFunctor.{v₁, v₂} )).obj X✝) :
                                                                                                      ((hF.compYonedaCompWhiskeringLeft.hom.app X).app X✝ a✝).down = hF.preimage a✝.down
                                                                                                      source
                                                                                                      def CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{max v₁ v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) :
                                                                                                      F.comp (CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max v₁ v₂))).obj F.op)) ≅ CategoryTheory.yoneda.comp ((CategoryTheory.whiskeringRight Cᵒᵖ (Type v₁) (Type (max v₁ v₂))).obj CategoryTheory.uliftFunctor.{v₂, v₁} )

                                                                                                      FullyFaithful.homEquiv as a natural isomorphism.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        source
                                                                                                        @[simp]
                                                                                                        theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_hom_app_app_down {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{max v₁ v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp (CategoryTheory.yoneda.obj (F.obj X))).obj X✝) :
                                                                                                        ((hF.compYonedaCompWhiskeringLeftMaxRight.hom.app X).app X✝ a✝).down = hF.preimage a✝
                                                                                                        source
                                                                                                        @[simp]
                                                                                                        theorem CategoryTheory.Functor.FullyFaithful.compYonedaCompWhiskeringLeftMaxRight_inv_app_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{max v₁ v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : ((CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{v₂, v₁} ).obj X✝) :
                                                                                                        (hF.compYonedaCompWhiskeringLeftMaxRight.inv.app X).app X✝ a✝ = F.map a✝.down