# The Yoneda embedding #

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

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

## References #

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

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

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

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

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

The Yoneda embedding is fully faithful.

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

The Yoneda embedding is full.

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

The Yoneda embedding is faithful.

Equations
• =
def CategoryTheory.Yoneda.ext {C : Type u₁} [] (X : C) (Y : C) (p : {Z : C} → (Z X)(Z Y)) (q : {Z : C} → (Z Y)(Z X)) (h₁ : ∀ {Z : C} (f : Z X), q (p f) = f) (h₂ : ∀ {Z : C} (f : Z Y), p (q f) = f) (n : ∀ {Z Z' : C} (f : Z' Z) (g : Z X), ) :
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₁} [] {X : C} {Y : C} (f : X Y) [CategoryTheory.IsIso (CategoryTheory.yoneda.map f)] :

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

@[simp]
theorem CategoryTheory.Coyoneda.naturality {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (α : CategoryTheory.coyoneda.obj X CategoryTheory.coyoneda.obj Y) {Z : C} {Z' : C} (f : Z' Z) (h : Z') :
CategoryTheory.CategoryStruct.comp (α.app Z' h) f = α.app Z
def CategoryTheory.Coyoneda.fullyFaithful {C : Type u₁} [] :
CategoryTheory.coyoneda.FullyFaithful

The co-Yoneda embedding is fully faithful.

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

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

Equations
Instances For
instance CategoryTheory.Coyoneda.coyoneda_full {C : Type u₁} [] :
CategoryTheory.coyoneda.Full
Equations
• =
instance CategoryTheory.Coyoneda.coyoneda_faithful {C : Type u₁} [] :
CategoryTheory.coyoneda.Faithful
Equations
• =
theorem CategoryTheory.Coyoneda.isIso {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) [CategoryTheory.IsIso (CategoryTheory.coyoneda.map f)] :

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

def CategoryTheory.Coyoneda.punitIso :
CategoryTheory.coyoneda.obj

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

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

Taking the unop of morphisms is a natural isomorphism.

Equations
Instances For
class CategoryTheory.Functor.Representable {C : Type u₁} [] (F : ) :

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

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

Hom(-,X) ≅ F via f

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

Hom(-,X) ≅ F via f

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

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

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

Hom(X,-) ≅ F via f

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

Hom(X,-) ≅ F via f

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

The representing object for the representable functor F.

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

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

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

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

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

The representing object for the corepresentable functor F.

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

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

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

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

Equations
Instances For
theorem CategoryTheory.Functor.coreprW_app_hom {C : Type u₁} [] (F : ) [hF : F.Corepresentable] (X : C) (f : F.coreprX X) :
(F.coreprW.app X).hom f = F.map f F.coreprx
theorem CategoryTheory.representable_of_natIso {C : Type u₁} [] (F : ) {G : } (i : F G) [F.Representable] :
G.Representable
theorem CategoryTheory.corepresentable_of_natIso {C : Type u₁} [] (F : ) {G : } (i : F G) [F.Corepresentable] :
G.Corepresentable
instance CategoryTheory.instCorepresentableIdType :
.Corepresentable
Equations
Equations
Equations
def CategoryTheory.yonedaEquiv {C : Type u₁} [] {X : C} {F : } :
(CategoryTheory.yoneda.obj X F) F.obj ()

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.yonedaEquiv_apply {C : Type u₁} [] {X : C} {F : } (f : CategoryTheory.yoneda.obj X F) :
CategoryTheory.yonedaEquiv f = f.app ()
@[simp]
theorem CategoryTheory.yonedaEquiv_symm_app_apply {C : Type u₁} [] {X : C} {F : } (x : F.obj ()) (Y : Cᵒᵖ) (f : ) :
(CategoryTheory.yonedaEquiv.symm x).app Y f = F.map f.op x
theorem CategoryTheory.yonedaEquiv_naturality {C : Type u₁} [] {X : C} {Y : C} {F : } (f : CategoryTheory.yoneda.obj X F) (g : Y X) :
F.map g.op (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g) f)
theorem CategoryTheory.yonedaEquiv_naturality' {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} {F : } (f : CategoryTheory.yoneda.obj () F) (g : X Y) :
F.map g (CategoryTheory.yonedaEquiv f) = CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g.unop) f)
theorem CategoryTheory.yonedaEquiv_comp {C : Type u₁} [] {X : C} {F : } {G : } (α : CategoryTheory.yoneda.obj X F) (β : F G) :
CategoryTheory.yonedaEquiv = β.app () (CategoryTheory.yonedaEquiv α)
theorem CategoryTheory.yonedaEquiv_yoneda_map {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
CategoryTheory.yonedaEquiv (CategoryTheory.yoneda.map f) = f
theorem CategoryTheory.yonedaEquiv_symm_map {C : Type u₁} [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) {F : } (t : F.obj X) :
CategoryTheory.yonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f.unop) (CategoryTheory.yonedaEquiv.symm t)
theorem CategoryTheory.hom_ext_yoneda {C : Type u₁} [] {P : } {Q : } {f : P Q} {g : P Q} (h : ∀ (X : C) (p : CategoryTheory.yoneda.obj X P), ) :
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₁) [] (P : Cᵒᵖ × ) (Q : Cᵒᵖ × ) (α : P Q) (x : .obj P) :
(.map α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
def CategoryTheory.yonedaPairing (C : Type u₁) [] :
CategoryTheory.Functor (Cᵒᵖ × ) (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
theorem CategoryTheory.yonedaPairingExt (C : Type u₁) [] {X : Cᵒᵖ × } {x : .obj X} {y : .obj X} (w : ∀ (Y : Cᵒᵖ), x.app Y = y.app Y) :
x = y
@[simp]
theorem CategoryTheory.yonedaPairing_map (C : Type u₁) [] (P : Cᵒᵖ × ) (Q : Cᵒᵖ × ) (α : P Q) (β : .obj P) :
.map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map α.1.unop)
def CategoryTheory.yonedaCompUliftFunctorEquiv {C : Type u₁} [] (F : CategoryTheory.Functor Cᵒᵖ (Type (max v₁ w))) (X : C) :
((CategoryTheory.yoneda.obj X).comp CategoryTheory.uliftFunctor.{w, v₁} F) F.obj ()

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.

Equations
Instances For
def CategoryTheory.curriedYonedaLemma {C : Type u₁} :
CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda

The curried version of yoneda lemma when C is small.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.largeCurriedYonedaLemma {C : Type u₁} [] :
CategoryTheory.yoneda.op.comp CategoryTheory.coyoneda ().comp ((CategoryTheory.whiskeringRight () (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
def CategoryTheory.yonedaOpCompYonedaObj {C : Type u₁} [] (P : ) :
CategoryTheory.yoneda.op.comp (CategoryTheory.yoneda.obj P)

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
def CategoryTheory.curriedYonedaLemma' {C : Type u₁} :
CategoryTheory.yoneda.comp (().obj CategoryTheory.yoneda.op)

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₁} [] {X : C} {Y : C} (f : X Y) (hf : ∀ (T : C), Function.Bijective fun (x : T X) => ) :
def CategoryTheory.coyonedaEquiv {C : Type u₁} [] {X : C} {F : } :
(CategoryTheory.coyoneda.obj () F) F.obj X

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.coyonedaEquiv_apply {C : Type u₁} [] {X : C} {F : } (f : CategoryTheory.coyoneda.obj () F) :
CategoryTheory.coyonedaEquiv f = f.app X
@[simp]
theorem CategoryTheory.coyonedaEquiv_symm_app_apply {C : Type u₁} [] {X : C} {F : } (x : F.obj X) (Y : C) (f : X Y) :
(CategoryTheory.coyonedaEquiv.symm x).app Y f = F.map f x
theorem CategoryTheory.coyonedaEquiv_naturality {C : Type u₁} [] {X : C} {Y : C} {F : } (f : CategoryTheory.coyoneda.obj () F) (g : X Y) :
F.map g (CategoryTheory.coyonedaEquiv f) = CategoryTheory.coyonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map g.op) f)
theorem CategoryTheory.coyonedaEquiv_comp {C : Type u₁} [] {X : C} {F : } {G : } (α : CategoryTheory.coyoneda.obj () F) (β : F G) :
CategoryTheory.coyonedaEquiv = β.app X (CategoryTheory.coyonedaEquiv α)
theorem CategoryTheory.coyonedaEquiv_coyoneda_map {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
CategoryTheory.coyonedaEquiv (CategoryTheory.coyoneda.map f.op) = f
theorem CategoryTheory.coyonedaEquiv_symm_map {C : Type u₁} [] {X : C} {Y : C} (f : X Y) {F : } (t : F.obj X) :
CategoryTheory.coyonedaEquiv.symm (F.map f t) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map f.op) (CategoryTheory.coyonedaEquiv.symm t)
def CategoryTheory.coyonedaEvaluation (C : Type u₁) [] :
CategoryTheory.Functor (C × ) (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₁) [] (P : C × ) (Q : C × ) (α : P Q) (x : P) :
( α x).down = α.2.app Q.1 (P.2.map α.1 x.down)
def CategoryTheory.coyonedaPairing (C : Type u₁) [] :
CategoryTheory.Functor (C × ) (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₁) [] {X : C × } {x : .obj X} {y : .obj X} (w : ∀ (Y : C), x.app Y = y.app Y) :
x = y
@[simp]
theorem CategoryTheory.coyonedaPairing_map (C : Type u₁) [] (P : C × ) (Q : C × ) (α : P Q) (β : .obj P) :
.map α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map α.1.op)
def CategoryTheory.coyonedaCompUliftFunctorEquiv {C : Type u₁} [] (F : CategoryTheory.Functor C (Type (max v₁ w))) (X : Cᵒᵖ) :
((CategoryTheory.coyoneda.obj X).comp CategoryTheory.uliftFunctor.{w, v₁} F) F.obj ()

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.

Equations
Instances For
def CategoryTheory.curriedCoyonedaLemma {C : Type u₁} :
CategoryTheory.coyoneda.rightOp.comp CategoryTheory.coyoneda

The curried version of coyoneda lemma when C is small.

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

The curried version of the Coyoneda lemma.

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

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
def CategoryTheory.curriedCoyonedaLemma' {C : Type u₁} :
CategoryTheory.yoneda.comp (().obj CategoryTheory.coyoneda.rightOp)

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₁} [] {X : C} {Y : C} (f : X Y) (hf : ∀ (T : C), Function.Bijective fun (x : Y T) => ) :
def CategoryTheory.yonedaMap {C : Type u₁} [] {D : Type u_1} [] (F : ) (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
@[simp]
theorem CategoryTheory.yonedaMap_app_apply {C : Type u₁} [] {D : Type u_1} [] (F : ) {Y : C} {X : Cᵒᵖ} (f : ) :
().app X f = F.map f