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).
@[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) :
Equations
- category_theory.yoneda = {obj := λ (X : C), {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' := _}, map := λ (X X' : C) (f : X ⟶ X'), {app := λ (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), g ≫ f, naturality' := _}, map_id' := _, map_comp' := _}
@[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) :
(category_theory.yoneda.map f).app Y g = g ≫ f
@[simp]
theorem
category_theory.yoneda_obj_obj
{C : Type u₁}
[category_theory.category C]
(X : C)
(Y : Cᵒᵖ) :
(category_theory.yoneda.obj X).obj Y = (opposite.unop Y ⟶ X)
@[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) :
(category_theory.coyoneda.obj X).map f g = g ≫ f
@[simp]
theorem
category_theory.coyoneda_obj_obj
{C : Type u₁}
[category_theory.category C]
(X : Cᵒᵖ)
(Y : C) :
(category_theory.coyoneda.obj X).obj Y = (opposite.unop X ⟶ Y)
Equations
- category_theory.coyoneda = {obj := λ (X : Cᵒᵖ), {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' := _}, map := λ (X X' : Cᵒᵖ) (f : X ⟶ X'), {app := λ (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), f.unop ≫ g, naturality' := _}, map_id' := _, map_comp' := _}
@[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) :
theorem
category_theory.yoneda.obj_map_id
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : opposite.op X ⟶ opposite.op Y) :
(category_theory.yoneda.obj X).map f (𝟙 X) = (category_theory.yoneda.map f.unop).app (opposite.op Y) (𝟙 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]
Equations
- category_theory.yoneda.yoneda_full = {preimage := λ (X Y : C) (f : category_theory.yoneda.obj X ⟶ category_theory.yoneda.obj Y), f.app (opposite.op X) (𝟙 X), witness' := _}
@[instance]
Equations
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)) :
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
- category_theory.yoneda.ext X Y p q h₁ h₂ n = category_theory.preimage_iso (category_theory.nat_iso.of_components (λ (Z : Cᵒᵖ), {hom := p (opposite.unop Z), inv := q (opposite.unop Z), hom_inv_id' := _, inv_hom_id' := _}) _)
def
category_theory.yoneda.is_iso
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_iso (category_theory.yoneda.map 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') :
@[instance]
Equations
- category_theory.coyoneda.coyoneda_full = {preimage := λ (X Y : Cᵒᵖ) (f : category_theory.coyoneda.obj X ⟶ category_theory.coyoneda.obj Y), category_theory.has_hom.hom.op (f.app (opposite.unop X) (𝟙 (opposite.unop X))), witness' := _}
@[instance]
Equations
def
category_theory.coyoneda.is_iso
{C : Type u₁}
[category_theory.category C]
{X Y : Cᵒᵖ}
(f : X ⟶ Y)
[category_theory.is_iso (category_theory.coyoneda.map f)] :
@[class]
- X : C
- w : category_theory.yoneda.obj (category_theory.representable.X F) ≅ F
@[instance]
def
category_theory.prod_category_instance_1
(C : Type u₁)
[category_theory.category C] :
category_theory.category ((Cᵒᵖ ⥤ Type v₁) × Cᵒᵖ)
Equations
- category_theory.prod_category_instance_1 C = category_theory.prod (Cᵒᵖ ⥤ Type v₁) Cᵒᵖ
@[instance]
def
category_theory.prod_category_instance_2
(C : Type u₁)
[category_theory.category C] :
category_theory.category (Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁))
Equations
- category_theory.prod_category_instance_2 C = category_theory.prod Cᵒᵖ (Cᵒᵖ ⥤ Type v₁)
Equations
Equations
- category_theory.yoneda_pairing C = category_theory.yoneda.op.prod (𝟭 (Cᵒᵖ ⥤ Type v₁)) ⋙ category_theory.functor.hom (Cᵒᵖ ⥤ Type v₁)
@[simp]
theorem
category_theory.yoneda_pairing_map
(C : Type u₁)
[category_theory.category C]
(P Q : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁))
(α : P ⟶ Q)
(β : (category_theory.yoneda_pairing C).obj P) :
(category_theory.yoneda_pairing C).map α β = category_theory.yoneda.map α.fst.unop ≫ β ≫ α.snd
Equations
- category_theory.yoneda_lemma C = {hom := {app := λ (F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (x : (category_theory.yoneda_pairing C).obj F), {down := x.app F.fst (𝟙 (opposite.unop F.fst))}, naturality' := _}, inv := {app := λ (F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (x : (category_theory.yoneda_evaluation C).obj F), {app := λ (X : Cᵒᵖ) (a : (opposite.unop ((category_theory.yoneda.op.prod (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst).obj X), F.snd.map (category_theory.has_hom.hom.op a) x.down, naturality' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
def
category_theory.yoneda_sections
{C : Type u₁}
[category_theory.category C]
(X : C)
(F : Cᵒᵖ ⥤ Type v₁) :
(category_theory.yoneda.obj X ⟶ F) ≅ ulift (F.obj (opposite.op X))
Equations
- category_theory.yoneda_sections X F = (category_theory.yoneda_lemma C).app (opposite.op X, F)
@[simp]
def
category_theory.yoneda_sections_small
{C : Type u₁}
[category_theory.small_category C]
(X : C)
(F : Cᵒᵖ ⥤ Type u₁) :
(category_theory.yoneda.obj X ⟶ F) ≅ F.obj (opposite.op X)