mathlib3 documentation

category_theory.yoneda

The Yoneda embedding #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

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

Equations
Instances for category_theory.yoneda
@[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) :

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

Equations
Instances for category_theory.coyoneda
@[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.

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

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

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

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

Instances of this typeclass
@[class]
structure category_theory.functor.corepresentable {C : Type u₁} [category_theory.category C] (F : C Type v₁) :
Prop

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

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

Instances of this typeclass
noncomputable def category_theory.functor.repr_X {C : Type u₁} [category_theory.category C] (F : Cᵒᵖ Type v₁) [F.representable] :
C

The representing object for the representable functor F.

Equations

The (forward direction of the) isomorphism witnessing F is representable.

Equations
Instances for category_theory.functor.repr_f

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

Equations

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

Equations
noncomputable def category_theory.functor.corepr_X {C : Type u₁} [category_theory.category C] (F : C Type v₁) [F.corepresentable] :
C

The representing object for the corepresentable functor F.

Equations

The (forward direction of the) isomorphism witnessing F is corepresentable.

Equations
Instances for category_theory.functor.corepr_f
noncomputable def category_theory.functor.corepr_x {C : Type u₁} [category_theory.category C] (F : C Type v₁) [F.corepresentable] :

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

Equations

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

Equations
theorem category_theory.functor.corepr_w_app_hom {C : Type u₁} [category_theory.category C] (F : C Type v₁) [F.corepresentable] (X : C) (f : F.corepr_X X) :
(F.corepr_w.app X).hom f = F.map f F.corepr_x

The "Yoneda evaluation" functor, which sends X : Cᵒᵖ and F : Cᵒᵖ ⥤ Type to F.obj X, functorially in both X and F.

Equations
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

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

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]

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

Equations