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

def CategoryTheory.preadditiveYonedaObj {C : Type u} [Category.{v, u} C] [Preadditive C] (Y : C) : Functor Cᵒᵖ (ModuleCat (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.

@[simp]

theorem CategoryTheory.preadditiveYonedaObj_map {C : Type u} [Category.{v, u} C] [Preadditive C] (Y : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (preadditiveYonedaObj Y).map f = ModuleCat.ofHom { toFun := fun (g : Opposite.unop X✝ ⟶ Y) => CategoryStruct.comp f.unop g, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CategoryTheory.preadditiveYonedaObj_obj_isModule {C : Type u} [Category.{v, u} C] [Preadditive C] (Y : C) (X : Cᵒᵖ) : ((preadditiveYonedaObj Y).obj X).isModule = Preadditive.moduleEndRight

@[simp]

theorem CategoryTheory.preadditiveYonedaObj_obj_carrier {C : Type u} [Category.{v, u} C] [Preadditive C] (Y : C) (X : Cᵒᵖ) : ↑((preadditiveYonedaObj Y).obj X) = (Opposite.unop X ⟶ Y)

@[simp]

theorem CategoryTheory.preadditiveYonedaObj_obj_isAddCommGroup {C : Type u} [Category.{v, u} C] [Preadditive C] (Y : C) (X : Cᵒᵖ) : ((preadditiveYonedaObj Y).obj X).isAddCommGroup = Preadditive.homGroup (Opposite.unop X) Y

def CategoryTheory.preadditiveYoneda {C : Type u} [Category.{v, u} C] [Preadditive C] : Functor C (Functor Cᵒᵖ AddCommGrp)

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.

@[simp]

theorem CategoryTheory.preadditiveYoneda_obj {C : Type u} [Category.{v, u} C] [Preadditive C] (Y : C) : preadditiveYoneda.obj Y = (preadditiveYonedaObj Y).comp (forget₂ (ModuleCat (End Y)) AddCommGrp)

def CategoryTheory.preadditiveCoyonedaObj {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) : Functor C (ModuleCat (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.

@[simp]

theorem CategoryTheory.preadditiveCoyonedaObj_obj_isAddCommGroup {C : Type u} [Category.{v, u} C] [Preadditive C] (X Y : C) : ((preadditiveCoyonedaObj X).obj Y).isAddCommGroup = Preadditive.homGroup X Y

@[simp]

theorem CategoryTheory.preadditiveCoyonedaObj_obj_carrier {C : Type u} [Category.{v, u} C] [Preadditive C] (X Y : C) : ↑((preadditiveCoyonedaObj X).obj Y) = (X ⟶ Y)

@[simp]

theorem CategoryTheory.preadditiveCoyonedaObj_obj_isModule {C : Type u} [Category.{v, u} C] [Preadditive C] (X Y : C) : ((preadditiveCoyonedaObj X).obj Y).isModule = moduleEndLeft C

@[simp]

theorem CategoryTheory.preadditiveCoyonedaObj_map {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (preadditiveCoyonedaObj X).map f = ModuleCat.ofHom { toFun := fun (g : X ⟶ X✝) => CategoryStruct.comp g f, map_add' := ⋯, map_smul' := ⋯ }

def CategoryTheory.preadditiveCoyoneda {C : Type u} [Category.{v, u} C] [Preadditive C] : Functor Cᵒᵖ (Functor C AddCommGrp)

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.

@[simp]

theorem CategoryTheory.preadditiveCoyoneda_obj {C : Type u} [Category.{v, u} C] [Preadditive C] (X : Cᵒᵖ) : preadditiveCoyoneda.obj X = (preadditiveCoyonedaObj (Opposite.unop X)).comp (forget₂ (ModuleCat (End (Opposite.unop X))ᵐᵒᵖ) AddCommGrp)

instance CategoryTheory.additive_yonedaObj {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) : (preadditiveYonedaObj X).Additive

instance CategoryTheory.additive_yonedaObj' {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) : (preadditiveYoneda.obj X).Additive

instance CategoryTheory.additive_coyonedaObj {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) : (preadditiveCoyonedaObj X).Additive

instance CategoryTheory.additive_coyonedaObj' {C : Type u} [Category.{v, u} C] [Preadditive C] (X : Cᵒᵖ) : (preadditiveCoyoneda.obj X).Additive

@[simp]

theorem CategoryTheory.whiskering_preadditiveYoneda {C : Type u} [Category.{v, u} C] [Preadditive C] : preadditiveYoneda.comp ((Functor.whiskeringRight Cᵒᵖ AddCommGrp (Type v)).obj (forget AddCommGrp)) = yoneda

Composing the preadditive yoneda embedding with the forgetful functor yields the regular Yoneda embedding.

@[simp]

theorem CategoryTheory.whiskering_preadditiveCoyoneda {C : Type u} [Category.{v, u} C] [Preadditive C] : preadditiveCoyoneda.comp ((Functor.whiskeringRight C AddCommGrp (Type v)).obj (forget AddCommGrp)) = coyoneda

Composing the preadditive yoneda embedding with the forgetful functor yields the regular Yoneda embedding.

instance CategoryTheory.full_preadditiveYoneda {C : Type u} [Category.{v, u} C] [Preadditive C] : preadditiveYoneda.Full

instance CategoryTheory.full_preadditiveCoyoneda {C : Type u} [Category.{v, u} C] [Preadditive C] : preadditiveCoyoneda.Full

instance CategoryTheory.faithful_preadditiveYoneda {C : Type u} [Category.{v, u} C] [Preadditive C] : preadditiveYoneda.Faithful

instance CategoryTheory.faithful_preadditiveCoyoneda {C : Type u} [Category.{v, u} C] [Preadditive C] : preadditiveCoyoneda.Faithful

def CategoryTheory.preadditiveYonedaMap {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u₁} [Category.{v, u₁} D] [Preadditive D] (F : Functor C D) [F.Additive] (X : C) : preadditiveYoneda.obj X ⟶ F.op.comp (preadditiveYoneda.obj (F.obj X))

The natural transformation preadditiveYoneda.obj X ⟶ F.op ⋙ preadditiveYoneda.obj (F.obj X) when F : C ⥤ D is an additive functor between preadditive categories and X : C.

@[simp]

theorem CategoryTheory.preadditiveYonedaMap_app {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u₁} [Category.{v, u₁} D] [Preadditive D] (F : Functor C D) [F.Additive] (X : C) (Y : Cᵒᵖ) : (preadditiveYonedaMap F X).app Y = AddCommGrp.ofHom F.mapAddHom

def AddCommGrp.preadditiveCoyonedaIso : CategoryTheory.preadditiveCoyoneda ≅ coyoneda

The preadditive coyoneda functor for the category AddCommGrp agrees with AddCommGrp.coyoneda.