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 #

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

Stacks Tag 001O

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.yoneda_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (Y : Cᵒᵖ) :
    @[simp]
    theorem CategoryTheory.yoneda_obj_map {C : Type u₁} [Category.{v₁, u₁} C] (X : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ Y✝) (g : Opposite.unop X✝ X) :
    @[simp]
    theorem CategoryTheory.yoneda_map_app {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : X✝ Y✝) (x✝ : Cᵒᵖ) (g : { obj := fun (Y : Cᵒᵖ) => Opposite.unop Y X✝, map := fun {X Y : Cᵒᵖ} (f : X Y) (g : Opposite.unop X X✝) => CategoryStruct.comp f.unop g, map_id := , map_comp := }.obj x✝) :

    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
      @[simp]
      theorem CategoryTheory.coyoneda_obj_map {C : Type u₁} [Category.{v₁, u₁} C] (X : Cᵒᵖ) {X✝ Y✝ : C} (f : X✝ Y✝) (g : Opposite.unop X X✝) :
      @[simp]
      theorem CategoryTheory.coyoneda_map_app {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ : Cᵒᵖ} (f : X✝ Y✝) (x✝ : C) (g : { obj := fun (Y : C) => Opposite.unop X✝ Y, map := fun {X Y : C} (f : X Y) (g : Opposite.unop X✝ X) => CategoryStruct.comp g f, map_id := , map_comp := }.obj x✝) :
      @[simp]
      @[simp]
      theorem CategoryTheory.Yoneda.naturality {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (α : yoneda.obj X yoneda.obj Y) {Z Z' : C} (f : Z Z') (h : Z' X) :

      The Yoneda embedding is fully faithful.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def CategoryTheory.Yoneda.ext {C : Type u₁} [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 (CategoryStruct.comp f g) = 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₁} [Category.{v₁, u₁} C] {X Y : C} (f : X Y) [IsIso (yoneda.map f)] :

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

          @[simp]
          theorem CategoryTheory.Coyoneda.naturality {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (α : coyoneda.obj X coyoneda.obj Y) {Z Z' : C} (f : Z' Z) (h : Opposite.unop X Z') :

          The co-Yoneda embedding is fully faithful.

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

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

            Equations
            Instances For
              theorem CategoryTheory.Coyoneda.isIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X Y) [IsIso (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

                Taking the unop of morphisms is a natural isomorphism.

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.Coyoneda.objOpOp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (X✝ : Cᵒᵖ) (a✝ : (yoneda.obj X).obj X✝) :
                  (objOpOp X).inv.app X✝ a✝ = (opEquiv (Opposite.op X) X✝).symm a✝
                  @[simp]
                  theorem CategoryTheory.Coyoneda.objOpOp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] (X : C) (X✝ : Cᵒᵖ) (a✝ : (coyoneda.obj (Opposite.op (Opposite.op X))).obj X✝) :
                  (objOpOp X).hom.app X✝ a✝ = (opEquiv (Opposite.op X) X✝) a✝

                  Taking the unop of morphisms is a natural isomorphism.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    structure CategoryTheory.Functor.RepresentableBy {C : Type u₁} [Category.{v₁, u₁} C] (F : 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

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

                      Equations
                      Instances For
                        structure CategoryTheory.Functor.CorepresentableBy {C : Type u₁} [Category.{v₁, u₁} C] (F : 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
                          theorem CategoryTheory.Functor.CorepresentableBy.homEquiv_symm_comp {C : Type u₁} [Category.{v₁, u₁} C] {F : Functor C (Type v)} {X : C} (e : F.CorepresentableBy X) {Y Y' : C} (y : F.obj Y) (g : Y Y') :

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

                          Equations
                          Instances For

                            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

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

                              Equations
                              Instances For

                                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

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

                                  Equations
                                  Instances For

                                    A functor F : Cᵒᵖ ⥤ Type v is representable if there is an object 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.

                                    Instances

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

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

                                      Instances

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

                                        noncomputable def CategoryTheory.Functor.reprX {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor Cᵒᵖ (Type v)) [hF : F.IsRepresentable] :
                                        C

                                        The representing object for the representable functor F.

                                        Equations
                                        Instances For

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

                                          Equations
                                          Instances For

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

                                            Equations
                                            Instances For

                                              An isomorphism between 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
                                              Instances For
                                                noncomputable def CategoryTheory.Functor.coreprX {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type v)) [hF : F.IsCorepresentable] :
                                                C

                                                The representing object for the corepresentable functor F.

                                                Equations
                                                Instances For

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

                                                  Equations
                                                  Instances For
                                                    noncomputable def CategoryTheory.Functor.coreprx {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type v)) [hF : F.IsCorepresentable] :

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

                                                    Equations
                                                    Instances For

                                                      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
                                                      Instances For

                                                        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
                                                          @[simp]
                                                          theorem CategoryTheory.yonedaEquiv_symm_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor Cᵒᵖ (Type v₁)} (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (f : Opposite.unop Y X) :
                                                          (yonedaEquiv.symm x).app Y f = F.map f.op x

                                                          See also yonedaEquiv_naturality' for a more general version.

                                                          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.

                                                          theorem CategoryTheory.yonedaEquiv_comp {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F G : Functor Cᵒᵖ (Type v₁)} (α : yoneda.obj X F) (β : F G) :
                                                          theorem CategoryTheory.map_yonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {F : Functor Cᵒᵖ (Type v₁)} (f : yoneda.obj X F) (g : Y X) :
                                                          F.map g.op (yonedaEquiv f) = f.app (Opposite.op Y) g

                                                          See also map_yonedaEquiv' for a more general version.

                                                          theorem CategoryTheory.map_yonedaEquiv' {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {F : Functor Cᵒᵖ (Type v₁)} (f : yoneda.obj (Opposite.unop X) F) (g : X Y) :
                                                          F.map g (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.

                                                          theorem CategoryTheory.hom_ext_yoneda {C : Type u₁} [Category.{v₁, u₁} C] {P Q : Functor Cᵒᵖ (Type v₁)} {f g : P Q} (h : ∀ (X : C) (p : yoneda.obj X P), CategoryStruct.comp p f = 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]
                                                            theorem CategoryTheory.yonedaEvaluation_map_down (C : Type u₁) [Category.{v₁, u₁} C] (P Q : Cᵒᵖ × Functor Cᵒᵖ (Type v₁)) (α : P Q) (x : (yonedaEvaluation C).obj P) :
                                                            ((yonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)

                                                            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
                                                              theorem CategoryTheory.yonedaPairingExt (C : Type u₁) [Category.{v₁, u₁} C] {X : Cᵒᵖ × Functor Cᵒᵖ (Type v₁)} {x y : (yonedaPairing C).obj X} (w : ∀ (Y : Cᵒᵖ), x.app Y = y.app Y) :
                                                              x = y
                                                              theorem CategoryTheory.yonedaPairingExt_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : Cᵒᵖ × Functor Cᵒᵖ (Type v₁)} {x y : (yonedaPairing C).obj X} :
                                                              x = y ∀ (Y : Cᵒᵖ), x.app Y = y.app Y

                                                              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.

                                                                Stacks Tag 001P

                                                                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

                                                                    The curried version of the Yoneda lemma.

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

                                                                      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
                                                                          theorem CategoryTheory.isIso_of_yoneda_map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X Y) (hf : ∀ (T : C), Function.Bijective fun (x : T X) => CategoryStruct.comp x f) :
                                                                          theorem CategoryTheory.isIso_iff_yoneda_map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X Y) :
                                                                          IsIso f ∀ (T : C), Function.Bijective fun (x : T X) => CategoryStruct.comp x f
                                                                          theorem CategoryTheory.isIso_iff_isIso_yoneda_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X Y) :
                                                                          IsIso f ∀ (c : C), IsIso ((yoneda.map f).app (Opposite.op c))
                                                                          def CategoryTheory.coyonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C (Type v₁)} :

                                                                          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
                                                                            @[simp]
                                                                            theorem CategoryTheory.coyonedaEquiv_symm_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F : Functor C (Type v₁)} (x : F.obj X) (Y : C) (f : X Y) :
                                                                            (coyonedaEquiv.symm x).app Y f = F.map f x
                                                                            theorem CategoryTheory.coyonedaEquiv_comp {C : Type u₁} [Category.{v₁, u₁} C] {X : C} {F G : Functor C (Type v₁)} (α : coyoneda.obj (Opposite.op X) F) (β : F G) :
                                                                            theorem CategoryTheory.map_coyonedaEquiv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {F : Functor C (Type v₁)} (f : coyoneda.obj (Opposite.op X) F) (g : X Y) :
                                                                            F.map g (coyonedaEquiv f) = f.app Y g
                                                                            def CategoryTheory.coyonedaEvaluation (C : Type u₁) [Category.{v₁, u₁} C] :
                                                                            Functor (C × 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
                                                                              @[simp]
                                                                              theorem CategoryTheory.coyonedaEvaluation_map_down (C : Type u₁) [Category.{v₁, u₁} C] (P Q : C × Functor C (Type v₁)) (α : P Q) (x : (coyonedaEvaluation C).obj P) :
                                                                              ((coyonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
                                                                              def CategoryTheory.coyonedaPairing (C : Type u₁) [Category.{v₁, u₁} C] :
                                                                              Functor (C × 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
                                                                                theorem CategoryTheory.coyonedaPairingExt (C : Type u₁) [Category.{v₁, u₁} C] {X : C × Functor C (Type v₁)} {x y : (coyonedaPairing C).obj X} (w : ∀ (Y : C), x.app Y = y.app Y) :
                                                                                x = y
                                                                                theorem CategoryTheory.coyonedaPairingExt_iff {C : Type u₁} [Category.{v₁, u₁} C] {X : C × Functor C (Type v₁)} {x y : (coyonedaPairing C).obj X} :
                                                                                x = y ∀ (Y : C), x.app Y = y.app Y
                                                                                @[simp]

                                                                                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.

                                                                                  Stacks Tag 001P

                                                                                  Equations
                                                                                  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

                                                                                      The curried version of the Coyoneda lemma.

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

                                                                                        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
                                                                                            theorem CategoryTheory.isIso_of_coyoneda_map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X Y) (hf : ∀ (T : C), Function.Bijective fun (x : Y T) => CategoryStruct.comp f x) :
                                                                                            theorem CategoryTheory.isIso_iff_coyoneda_map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X Y) :
                                                                                            IsIso f ∀ (T : C), Function.Bijective fun (x : Y T) => CategoryStruct.comp f x
                                                                                            theorem CategoryTheory.isIso_iff_isIso_coyoneda_map {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X Y) :
                                                                                            IsIso f ∀ (c : C), IsIso ((coyoneda.map f.op).app c)
                                                                                            def CategoryTheory.yonedaMap {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v₁, u_1} D] (F : Functor C D) (X : C) :

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

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem CategoryTheory.yonedaMap_app_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u_1} [Category.{v₁, u_1} D] (F : Functor C D) {Y : C} {X : Cᵒᵖ} (f : Opposite.unop X Y) :
                                                                                              (yonedaMap F Y).app X f = F.map f
                                                                                              def CategoryTheory.Functor.sectionsEquivHom {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type u₂)) (X : Type u₂) [Unique X] :
                                                                                              F.sections ((const C).obj X F)

                                                                                              A type-level equivalence between sections of a functor and morphisms from a terminal functor to it. We use the constant functor on a given singleton type here as a specific choice of terminal functor.

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem CategoryTheory.Functor.sectionsEquivHom_apply_app {C : Type u₁} [Category.{v₁, u₁} C] (F : Functor C (Type u₂)) (X : Type u₂) [Unique X] (s : F.sections) (j : C) (x : ((const C).obj X).obj j) :
                                                                                                ((F.sectionsEquivHom X) s).app j x = s j

                                                                                                A natural isomorphism between the sections functor (C ⥤ Type _) ⥤ Type _ and the co-Yoneda embedding of a terminal functor, specifically a constant functor on a given singleton type X.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem CategoryTheory.sectionsFunctorNatIsoCoyoneda_inv_app_coe {C : Type u₁} [Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : Functor C (Type (max u₁ u₂))) (a✝ : (coyoneda.obj (Opposite.op ((Functor.const C).obj X))).obj X✝) (j : C) :
                                                                                                  ((sectionsFunctorNatIsoCoyoneda X).inv.app X✝ a✝) j = a✝.app j default
                                                                                                  @[simp]
                                                                                                  theorem CategoryTheory.sectionsFunctorNatIsoCoyoneda_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] (X : Type (max u₁ u₂)) [Unique X] (X✝ : Functor C (Type (max u₁ u₂))) (a✝ : (Functor.sectionsFunctor C).obj X✝) (j : C) (x : ((Functor.const C).obj X).obj j) :
                                                                                                  ((sectionsFunctorNatIsoCoyoneda X).hom.app X✝ a✝).app j x = a✝ j
                                                                                                  @[simp]
                                                                                                  theorem CategoryTheory.Functor.FullyFaithful.homNatIso_inv_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : ((yoneda.obj X).comp uliftFunctor.{v₂, v₁}).obj X✝) :
                                                                                                  ((hF.homNatIso X).inv.app X✝ a✝).down = F.map a✝.down
                                                                                                  @[simp]
                                                                                                  theorem CategoryTheory.Functor.FullyFaithful.homNatIso_hom_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp ((yoneda.obj (F.obj X)).comp uliftFunctor.{v₁, v₂})).obj X✝) :
                                                                                                  ((hF.homNatIso X).hom.app X✝ a✝).down = hF.preimage a✝.down
                                                                                                  @[simp]
                                                                                                  theorem CategoryTheory.Functor.FullyFaithful.homNatIsoMaxRight_hom_app_down {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{max v₁ v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X : C) (X✝ : Cᵒᵖ) (a✝ : (F.op.comp (yoneda.obj (F.obj X))).obj X✝) :
                                                                                                  ((hF.homNatIsoMaxRight X).hom.app X✝ a✝).down = hF.preimage a✝