The Yoneda embedding for preadditive categories #
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
CategoryTheory.preadditiveYonedaObj_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(Y : C)
(X : Cᵒᵖ)
:
(CategoryTheory.preadditiveYonedaObj Y).obj X = ModuleCat.of (CategoryTheory.End Y) (X.unop ⟶ Y)
@[simp]
theorem
CategoryTheory.preadditiveYonedaObj_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(Y : C)
:
∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
(CategoryTheory.preadditiveYonedaObj Y).map f = ModuleCat.ofHom
{
toAddHom :=
{ toFun := fun g => CategoryTheory.CategoryStruct.comp f.unop g,
map_add' :=
(_ :
∀ (g g' : X.unop ⟶ Y),
CategoryTheory.CategoryStruct.comp f.unop (g + g') = CategoryTheory.CategoryStruct.comp f.unop g + CategoryTheory.CategoryStruct.comp f.unop g') },
map_smul' :=
(_ :
∀ (r : CategoryTheory.End Y) (g : X.unop ⟶ Y),
AddHom.toFun
{ toFun := fun g => CategoryTheory.CategoryStruct.comp f.unop g,
map_add' :=
(_ :
∀ (g g' : X.unop ⟶ Y),
CategoryTheory.CategoryStruct.comp f.unop (g + g') = CategoryTheory.CategoryStruct.comp f.unop g + CategoryTheory.CategoryStruct.comp f.unop g') }
(r • g) = ↑(RingHom.id (CategoryTheory.End Y)) r • AddHom.toFun
{ toFun := fun g => CategoryTheory.CategoryStruct.comp f.unop g,
map_add' :=
(_ :
∀ (g g' : X.unop ⟶ Y),
CategoryTheory.CategoryStruct.comp f.unop (g + g') = CategoryTheory.CategoryStruct.comp f.unop g + CategoryTheory.CategoryStruct.comp f.unop g') }
g) }
def
CategoryTheory.preadditiveYonedaObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(Y : C)
:
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.
Instances For
@[simp]
theorem
CategoryTheory.preadditiveYoneda_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(Y : C)
:
CategoryTheory.preadditiveYoneda.obj Y = CategoryTheory.Functor.comp (CategoryTheory.preadditiveYonedaObj Y)
(CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End Y)) AddCommGroupCat)
@[simp]
theorem
CategoryTheory.preadditiveYoneda_map_app_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
∀ {X Y : C} (f : X ⟶ Y) (X_1 : Cᵒᵖ)
(g :
↑(((fun Y =>
CategoryTheory.Functor.comp (CategoryTheory.preadditiveYonedaObj Y)
(CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End Y)) AddCommGroupCat))
X).obj
X_1)),
↑((CategoryTheory.preadditiveYoneda.map f).app X_1) g = CategoryTheory.CategoryStruct.comp g f
def
CategoryTheory.preadditiveYoneda
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
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 preadditiveYonedaObj.
Instances For
@[simp]
theorem
CategoryTheory.preadditiveCoyonedaObj_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : Cᵒᵖ)
(Y : C)
:
(CategoryTheory.preadditiveCoyonedaObj X).obj Y = ModuleCat.of (CategoryTheory.End X) (X.unop ⟶ Y)
@[simp]
theorem
CategoryTheory.preadditiveCoyonedaObj_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : Cᵒᵖ)
:
∀ {X Y : C} (f : X ⟶ Y),
(CategoryTheory.preadditiveCoyonedaObj X).map f = ModuleCat.ofHom
{
toAddHom :=
{ toFun := fun g => CategoryTheory.CategoryStruct.comp g f,
map_add' :=
(_ :
∀ (g g' : X.unop ⟶ X),
CategoryTheory.CategoryStruct.comp (g + g') f = CategoryTheory.CategoryStruct.comp g f + CategoryTheory.CategoryStruct.comp g' f) },
map_smul' :=
(_ :
∀ (r : CategoryTheory.End X) (g : X.unop ⟶ X),
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp r.unop g) f = CategoryTheory.CategoryStruct.comp r.unop (CategoryTheory.CategoryStruct.comp g f)) }
def
CategoryTheory.preadditiveCoyonedaObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : Cᵒᵖ)
:
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.
Instances For
@[simp]
theorem
CategoryTheory.preadditiveCoyoneda_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : Cᵒᵖ)
:
CategoryTheory.preadditiveCoyoneda.obj X = CategoryTheory.Functor.comp (CategoryTheory.preadditiveCoyonedaObj X)
(CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End X)) AddCommGroupCat)
@[simp]
theorem
CategoryTheory.preadditiveCoyoneda_map_app_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (Y_1 : C)
(g :
↑(((fun X =>
CategoryTheory.Functor.comp (CategoryTheory.preadditiveCoyonedaObj X)
(CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End X)) AddCommGroupCat))
X).obj
Y_1)),
↑((CategoryTheory.preadditiveCoyoneda.map f).app Y_1) g = CategoryTheory.CategoryStruct.comp f.unop g
def
CategoryTheory.preadditiveCoyoneda
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
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 preadditiveCoyonedaObj.
Instances For
instance
CategoryTheory.additive_yonedaObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : C)
:
instance
CategoryTheory.additive_yonedaObj'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : C)
:
CategoryTheory.Functor.Additive (CategoryTheory.preadditiveYoneda.obj X)
instance
CategoryTheory.additive_coyonedaObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : Cᵒᵖ)
:
instance
CategoryTheory.additive_coyonedaObj'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
(X : Cᵒᵖ)
:
CategoryTheory.Functor.Additive (CategoryTheory.preadditiveCoyoneda.obj X)
@[simp]
theorem
CategoryTheory.whiskering_preadditiveYoneda
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
CategoryTheory.Functor.comp CategoryTheory.preadditiveYoneda
((CategoryTheory.whiskeringRight Cᵒᵖ AddCommGroupCat (Type v)).obj (CategoryTheory.forget AddCommGroupCat)) = CategoryTheory.yoneda
Composing the preadditive yoneda embedding with the forgetful functor yields the regular Yoneda embedding.
@[simp]
theorem
CategoryTheory.whiskering_preadditiveCoyoneda
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
CategoryTheory.Functor.comp CategoryTheory.preadditiveCoyoneda
((CategoryTheory.whiskeringRight C AddCommGroupCat (Type v)).obj (CategoryTheory.forget AddCommGroupCat)) = CategoryTheory.coyoneda
Composing the preadditive yoneda embedding with the forgetful functor yields the regular Yoneda embedding.
instance
CategoryTheory.full_preadditiveYoneda
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
CategoryTheory.Full CategoryTheory.preadditiveYoneda
instance
CategoryTheory.full_preadditiveCoyoneda
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
CategoryTheory.Full CategoryTheory.preadditiveCoyoneda
instance
CategoryTheory.faithful_preadditiveYoneda
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
CategoryTheory.Faithful CategoryTheory.preadditiveYoneda
instance
CategoryTheory.faithful_preadditiveCoyoneda
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
:
CategoryTheory.Faithful CategoryTheory.preadditiveCoyoneda