mathlib documentation

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₁} [category_theory.category C] (X X' : C) (f : X X') (Y : Cᵒᵖ) (g : {obj := λ (Y : Cᵒᵖ), opposite.unop Y X, map := λ (Y Y' : Cᵒᵖ) (f : Y Y') (g : opposite.unop Y X), f.unop g, map_id' := _, map_comp' := _}.obj Y) :

def category_theory.yoneda {C : Type u₁} [category_theory.category C] :
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]

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

@[simp]

def category_theory.coyoneda {C : Type u₁} [category_theory.category C] :
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₁} [category_theory.category C] (X X' : Cᵒᵖ) (f : X X') (Y : C) (g : {obj := λ (Y : C), opposite.unop X Y, map := λ (Y Y' : C) (f : Y Y') (g : opposite.unop X Y), g f, map_id' := _, map_comp' := _}.obj Y) :

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

@[simp]
theorem category_theory.yoneda.naturality {C : Type u₁} [category_theory.category C] {X Y : C} (α : category_theory.yoneda.obj X category_theory.yoneda.obj Y) {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₁} [category_theory.category C] (X Y : C) (p : Π {Z : C}, (Z X)(Z Y)) (q : Π {Z : C}, (Z Y)(Z X)) :
(∀ {Z : C} (f : Z X), q (p f) = f)(∀ {Z : C} (f : Z Y), p (q f) = f)(∀ {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
@[simp]
theorem category_theory.coyoneda.naturality {C : Type u₁} [category_theory.category C] {X Y : Cᵒᵖ} (α : category_theory.coyoneda.obj X category_theory.coyoneda.obj Y) {Z Z' : C} (f : Z' Z) (h : opposite.unop X Z') :
α.app Z' h f = α.app Z (h f)

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

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

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

def category_theory.yoneda_evaluation (C : Type u₁) [category_theory.category C] :
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]

def category_theory.yoneda_pairing (C : Type u₁) [category_theory.category C] :
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

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₁} [category_theory.category C] (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

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_inv_app_apply {C : Type u₁} [category_theory.small_category C] (X : C) (F : Cᵒᵖ Type u₁) (t : F.obj (opposite.op X)) (Y : Cᵒᵖ) (f : opposite.unop Y X) :