# mathlibdocumentation

category_theory.yoneda

# The Yoneda embedding

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

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

## References

@[simp]
theorem category_theory.yoneda_map_app {C : Type u₁} (X X' : C) (f : X X') (Y : Cᵒᵖ) (g : {obj := λ (Y : Cᵒᵖ), , map := λ (Y Y' : Cᵒᵖ) (f : Y Y') (g : X), f.unop g, map_id' := _, map_comp' := _}.obj Y) :
Y g = g f

def category_theory.yoneda {C : Type u₁}  :
C Cᵒᵖ Type v₁

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

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

Equations
@[simp]
theorem category_theory.yoneda_obj_obj {C : Type u₁} (X : C) (Y : Cᵒᵖ) :
Y = X)

@[simp]
theorem category_theory.yoneda_obj_map {C : Type u₁} (X : C) (Y Y' : Cᵒᵖ) (f : Y Y') (g : X) :
f g = f.unop g

@[simp]
theorem category_theory.coyoneda_obj_obj {C : Type u₁} (X : Cᵒᵖ) (Y : C) :
= Y)

def category_theory.coyoneda {C : Type u₁}  :
Cᵒᵖ C Type v₁

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

Equations
@[simp]
theorem category_theory.coyoneda_map_app {C : Type u₁} (X X' : Cᵒᵖ) (f : X X') (Y : C) (g : {obj := λ (Y : C), , map := λ (Y Y' : C) (f : Y Y') (g : Y), g f, map_id' := _, map_comp' := _}.obj Y) :
g = f.unop g

@[simp]
theorem category_theory.coyoneda_obj_map {C : Type u₁} (X : Cᵒᵖ) (Y Y' : C) (f : Y Y') (g : Y) :
g = g f

theorem category_theory.yoneda.obj_map_id {C : Type u₁} {X Y : C} (f : ) :
f (𝟙 X) = (opposite.op Y) (𝟙 Y)

@[simp]
theorem category_theory.yoneda.naturality {C : Type u₁} {X Y : C} {Z Z' : C} (f : Z Z') (h : Z' X) :
f α.app (opposite.op Z') h = α.app (opposite.op Z) (f h)

@[instance]

The Yoneda embedding is full.

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

Equations
@[instance]

The Yoneda embedding is faithful.

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

def category_theory.yoneda.ext {C : Type u₁} (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 (f g) = 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
def category_theory.yoneda.is_iso {C : Type u₁} {X Y : C} (f : X Y)  :

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

Equations
@[simp]
theorem category_theory.coyoneda.naturality {C : Type u₁} {X Y : Cᵒᵖ} {Z Z' : C} (f : Z' Z) (h : Z') :
α.app Z' h f = α.app Z (h f)

@[instance]

def category_theory.coyoneda.is_iso {C : Type u₁} {X Y : Cᵒᵖ} (f : X Y)  :

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

Equations
def category_theory.coyoneda.iso_comp_punit {C : Type u₁} (P : C Type v₁) :

A Type-valued presheaf P is isomorphic to the composition of P with the coyoneda functor coming from punit.

Equations
@[simp]
theorem category_theory.coyoneda.iso_comp_punit_hom_app {C : Type u₁} (P : C Type v₁) (X : C) (f : X) :

@[simp]
theorem category_theory.coyoneda.iso_comp_punit_inv_app {C : Type u₁} (P : C Type v₁) (X : C) (a : P.obj X) (_x : opposite.unop ) :
_x = a

@[class]
structure category_theory.representable {C : Type u₁} (F : Cᵒᵖ Type v₁) :
Type (max u₁ v₁)
• X : C
• w :

A presheaf F is representable if there is object X so F ≅ yoneda.obj X.

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

@[instance]

Equations
@[instance]

Equations
def category_theory.yoneda_evaluation (C : Type u₁)  :
Cᵒᵖ × (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
@[simp]
theorem category_theory.yoneda_evaluation_map_down (C : Type u₁) (P Q : Cᵒᵖ × (Cᵒᵖ Type v₁)) (α : P Q) (x : P) :
x).down = α.snd.app Q.fst (P.snd.map α.fst x.down)

def category_theory.yoneda_pairing (C : Type u₁)  :
Cᵒᵖ × (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
@[simp]
theorem category_theory.yoneda_pairing_map (C : Type u₁) (P Q : Cᵒᵖ × (Cᵒᵖ Type v₁)) (α : P Q) (β : P) :
= β α.snd

The Yoneda lemma asserts that 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
@[simp]
def category_theory.yoneda_sections {C : Type u₁} (X : C) (F : Cᵒᵖ Type v₁) :

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

Equations
def category_theory.yoneda_equiv {C : Type u₁} {X : C} {F : Cᵒᵖ Type v₁} :

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

Equations
theorem category_theory.yoneda_equiv_naturality {C : Type u₁} {X Y : C} {F : Cᵒᵖ Type v₁} (f : F) (g : Y X) :

@[simp]
theorem category_theory.yoneda_equiv_apply {C : Type u₁} {X : C} {F : Cᵒᵖ Type v₁} (f : F) :
= f.app (opposite.op X) (𝟙 X)

@[simp]
theorem category_theory.yoneda_equiv_symm_app_apply {C : Type u₁} {X : C} {F : Cᵒᵖ Type v₁} (x : F.obj (opposite.op X)) (Y : Cᵒᵖ) (f : X) :
Y f = F.map f.op x

def category_theory.yoneda_sections_small {C : Type u₁} (X : C) (F : Cᵒᵖ Type u₁) :

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

Equations
@[simp]
theorem category_theory.yoneda_sections_small_hom {C : Type u₁} (X : C) (F : Cᵒᵖ Type u₁) (f : F) :

@[simp]
theorem category_theory.yoneda_sections_small_inv_app_apply {C : Type u₁} (X : C) (F : Cᵒᵖ Type u₁) (t : F.obj (opposite.op X)) (Y : Cᵒᵖ) (f : X) :
t).app Y f = F.map f.op t