The Yoneda embedding for preadditive categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The Yoneda embedding for preadditive categories sends an object Y to the presheaf sending an
object X to the group of morphisms X ⟶ Y. At each point, we get an additional End Y-module
structure.
We also show that this presheaf is additive and that it is compatible with the normal Yoneda embedding in the expected way and deduce that the preadditive Yoneda embedding is fully faithful.
TODO #
- The Yoneda embedding is additive itself
@[simp]
theorem
category_theory.preadditive_yoneda_obj_obj
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(Y : C)
(X : Cᵒᵖ) :
(category_theory.preadditive_yoneda_obj Y).obj X = Module.of (category_theory.End Y) (opposite.unop X ⟶ Y)
@[simp]
theorem
category_theory.preadditive_yoneda_obj_map_apply
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(Y : C)
(X X' : Cᵒᵖ)
(f : X ⟶ X')
(g : ↥(Module.of (category_theory.End Y) (opposite.unop X ⟶ Y))) :
def
category_theory.preadditive_yoneda_obj
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(Y : C) :
Cᵒᵖ ⥤ Module (category_theory.End Y)
The Yoneda embedding for preadditive categories sends an object Y to the presheaf sending an
object X to the End Y-module of morphisms X ⟶ Y.
Equations
- category_theory.preadditive_yoneda_obj Y = {obj := λ (X : Cᵒᵖ), Module.of (category_theory.End Y) (opposite.unop X ⟶ Y), map := λ (X X' : Cᵒᵖ) (f : X ⟶ X'), {to_fun := λ (g : ↥(Module.of (category_theory.End Y) (opposite.unop X ⟶ Y))), f.unop ≫ g, map_add' := _, map_smul' := _}, map_id' := _, map_comp' := _}
Instances for category_theory.preadditive_yoneda_obj
@[simp]
theorem
category_theory.preadditive_yoneda_map_app_apply
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(Y Y' : C)
(f : Y ⟶ Y')
(X : Cᵒᵖ)
(g : ↥((category_theory.preadditive_yoneda_obj Y ⋙ category_theory.forget₂ (Module (category_theory.End Y)) AddCommGroup).obj X)) :
@[simp]
def
category_theory.preadditive_yoneda
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C] :
C ⥤ Cᵒᵖ ⥤ AddCommGroup
The Yoneda embedding for preadditive categories sends an object Y to the presheaf sending an
object X to the group of morphisms X ⟶ Y. At each point, we get an additional End Y-module
structure, see preadditive_yoneda_obj.
Equations
- category_theory.preadditive_yoneda = {obj := λ (Y : C), category_theory.preadditive_yoneda_obj Y ⋙ category_theory.forget₂ (Module (category_theory.End Y)) AddCommGroup, map := λ (Y Y' : C) (f : Y ⟶ Y'), {app := λ (X : Cᵒᵖ), {to_fun := λ (g : ↥((category_theory.preadditive_yoneda_obj Y ⋙ category_theory.forget₂ (Module (category_theory.End Y)) AddCommGroup).obj X)), g ≫ f, map_zero' := _, map_add' := _}, naturality' := _}, map_id' := _, map_comp' := _}
Instances for category_theory.preadditive_yoneda
@[simp]
theorem
category_theory.preadditive_coyoneda_obj_map_apply
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X : Cᵒᵖ)
(Y Y' : C)
(f : Y ⟶ Y')
(g : ↥(Module.of (category_theory.End X) (opposite.unop X ⟶ Y))) :
⇑((category_theory.preadditive_coyoneda_obj X).map f) g = g ≫ f
@[simp]
theorem
category_theory.preadditive_coyoneda_obj_obj
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X : Cᵒᵖ)
(Y : C) :
(category_theory.preadditive_coyoneda_obj X).obj Y = Module.of (category_theory.End X) (opposite.unop X ⟶ Y)
def
category_theory.preadditive_coyoneda_obj
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X : Cᵒᵖ) :
C ⥤ Module (category_theory.End X)
The Yoneda embedding for preadditive categories sends an object X to the copresheaf sending an
object Y to the End X-module of morphisms X ⟶ Y.
Equations
- category_theory.preadditive_coyoneda_obj X = {obj := λ (Y : C), Module.of (category_theory.End X) (opposite.unop X ⟶ Y), map := λ (Y Y' : C) (f : Y ⟶ Y'), {to_fun := λ (g : ↥(Module.of (category_theory.End X) (opposite.unop X ⟶ Y))), g ≫ f, map_add' := _, map_smul' := _}, map_id' := _, map_comp' := _}
Instances for category_theory.preadditive_coyoneda_obj
@[simp]
theorem
category_theory.preadditive_coyoneda_map_app_apply
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X X' : Cᵒᵖ)
(f : X ⟶ X')
(Y : C)
(g : ↥((category_theory.preadditive_coyoneda_obj X ⋙ category_theory.forget₂ (Module (category_theory.End X)) AddCommGroup).obj Y)) :
@[simp]
def
category_theory.preadditive_coyoneda
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C] :
Cᵒᵖ ⥤ C ⥤ AddCommGroup
The Yoneda embedding for preadditive categories sends an object X to the copresheaf sending an
object Y to the group of morphisms X ⟶ Y. At each point, we get an additional End X-module
structure, see preadditive_coyoneda_obj.
Equations
- category_theory.preadditive_coyoneda = {obj := λ (X : Cᵒᵖ), category_theory.preadditive_coyoneda_obj X ⋙ category_theory.forget₂ (Module (category_theory.End X)) AddCommGroup, map := λ (X X' : Cᵒᵖ) (f : X ⟶ X'), {app := λ (Y : C), {to_fun := λ (g : ↥((category_theory.preadditive_coyoneda_obj X ⋙ category_theory.forget₂ (Module (category_theory.End X)) AddCommGroup).obj Y)), f.unop ≫ g, map_zero' := _, map_add' := _}, naturality' := _}, map_id' := _, map_comp' := _}
Instances for category_theory.preadditive_coyoneda
@[protected, instance]
def
category_theory.additive_yoneda_obj
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X : C) :
@[protected, instance]
def
category_theory.additive_yoneda_obj'
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X : C) :
@[protected, instance]
def
category_theory.additive_coyoneda_obj
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X : Cᵒᵖ) :
@[protected, instance]
def
category_theory.additive_coyoneda_obj'
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C]
(X : Cᵒᵖ) :
@[simp]
theorem
category_theory.whiskering_preadditive_yoneda
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C] :
Composing the preadditive yoneda embedding with the forgetful functor yields the regular Yoneda embedding.
@[simp]
theorem
category_theory.whiskering_preadditive_coyoneda
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C] :
Composing the preadditive yoneda embedding with the forgetful functor yields the regular Yoneda embedding.
@[protected, instance]
def
category_theory.preadditive_yoneda_full
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C] :
Equations
- category_theory.preadditive_yoneda_full = let yoneda_full : category_theory.full (category_theory.preadditive_yoneda ⋙ (category_theory.whiskering_right Cᵒᵖ AddCommGroup (Type v)).obj (category_theory.forget AddCommGroup)) := category_theory.yoneda.yoneda_full in category_theory.full.of_comp_faithful category_theory.preadditive_yoneda ((category_theory.whiskering_right Cᵒᵖ AddCommGroup (Type v)).obj (category_theory.forget AddCommGroup))
@[protected, instance]
def
category_theory.preadditive_coyoneda_full
{C : Type u}
[category_theory.category C]
[category_theory.preadditive C] :
Equations
- category_theory.preadditive_coyoneda_full = let coyoneda_full : category_theory.full (category_theory.preadditive_coyoneda ⋙ (category_theory.whiskering_right C AddCommGroup (Type v)).obj (category_theory.forget AddCommGroup)) := category_theory.coyoneda.coyoneda_full in category_theory.full.of_comp_faithful category_theory.preadditive_coyoneda ((category_theory.whiskering_right C AddCommGroup (Type v)).obj (category_theory.forget AddCommGroup))
@[protected, instance]
@[protected, instance]