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)
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)) (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

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

@[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)

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

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

Equations
@[simp]
@[class]
structure category_theory.representable {C : Type u₁} [category_theory.category C] (F : 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
def category_theory.yoneda_equiv {C : Type u₁} [category_theory.category C] {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
@[simp]
theorem category_theory.yoneda_equiv_symm_app_apply {C : Type u₁} [category_theory.category C] {X : C} {F : Cᵒᵖ Type v₁} (x : F.obj (opposite.op X)) (Y : Cᵒᵖ) (f : opposite.unop Y X) :

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) :