Documentation

Mathlib.CategoryTheory.Preadditive.Yoneda.Basic

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 #

source
@[simp]
theorem CategoryTheory.preadditiveYonedaObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) (X : Cᵒᵖ) :
(CategoryTheory.preadditiveYonedaObj Y).toPrefunctor.obj X = ModuleCat.of (CategoryTheory.End Y) (X.unop ⟶ Y)
source
@[simp]
theorem CategoryTheory.preadditiveYonedaObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) :
∀ {X Y_1 : Cᵒᵖ} (f : X ⟶ Y_1), (CategoryTheory.preadditiveYonedaObj Y).toPrefunctor.map f = ModuleCat.ofHom { toAddHom := { toFun := fun (g : X.unop ⟶ Y) => 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), { toFun := fun (g : X.unop ⟶ Y) => 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') }.toFun (r • g) = (RingHom.id (CategoryTheory.End Y)) r • { toFun := fun (g : X.unop ⟶ Y) => 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') }.toFun g) }
source
def CategoryTheory.preadditiveYonedaObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) :
CategoryTheory.Functor Cᵒᵖ (ModuleCat (CategoryTheory.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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.preadditiveYoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Y : C) :
    CategoryTheory.preadditiveYoneda.toPrefunctor.obj Y = CategoryTheory.Functor.comp (CategoryTheory.preadditiveYonedaObj Y) (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End Y)) AddCommGroupCat)
    source
    @[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 : C) => CategoryTheory.Functor.comp (CategoryTheory.preadditiveYonedaObj Y) (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End Y)) AddCommGroupCat)) X).toPrefunctor.obj X_1)), ((CategoryTheory.preadditiveYoneda.toPrefunctor.map f).app X_1) g = CategoryTheory.CategoryStruct.comp g f
    source
    def CategoryTheory.preadditiveYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
    CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ AddCommGroupCat)

    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.preadditiveCoyonedaObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) (Y : C) :
      (CategoryTheory.preadditiveCoyonedaObj X).toPrefunctor.obj Y = ModuleCat.of (CategoryTheory.End X) (X.unop ⟶ Y)
      source
      @[simp]
      theorem CategoryTheory.preadditiveCoyonedaObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) :
      ∀ {X_1 Y : C} (f : X_1 ⟶ Y), (CategoryTheory.preadditiveCoyonedaObj X).toPrefunctor.map f = ModuleCat.ofHom { toAddHom := { toFun := fun (g : X.unop ⟶ X_1) => CategoryTheory.CategoryStruct.comp g f, map_add' := (_ : ∀ (g g' : X.unop ⟶ X_1), 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_1), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp r.unop g) f = CategoryTheory.CategoryStruct.comp r.unop (CategoryTheory.CategoryStruct.comp g f)) }
      source
      def CategoryTheory.preadditiveCoyonedaObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) :
      CategoryTheory.Functor C (ModuleCat (CategoryTheory.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
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.preadditiveCoyoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) :
        CategoryTheory.preadditiveCoyoneda.toPrefunctor.obj X = CategoryTheory.Functor.comp (CategoryTheory.preadditiveCoyonedaObj X) (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End X)) AddCommGroupCat)
        source
        @[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 : Cᵒᵖ) => CategoryTheory.Functor.comp (CategoryTheory.preadditiveCoyonedaObj X) (CategoryTheory.forget₂ (ModuleCat (CategoryTheory.End X)) AddCommGroupCat)) X).toPrefunctor.obj Y_1)), ((CategoryTheory.preadditiveCoyoneda.toPrefunctor.map f).app Y_1) g = CategoryTheory.CategoryStruct.comp f.unop g
        source
        def CategoryTheory.preadditiveCoyoneda {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
        CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C AddCommGroupCat)

        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.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance CategoryTheory.additive_yonedaObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) :
          CategoryTheory.Functor.Additive (CategoryTheory.preadditiveYonedaObj X)
          Equations
          source
          instance CategoryTheory.additive_yonedaObj' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) :
          CategoryTheory.Functor.Additive (CategoryTheory.preadditiveYoneda.toPrefunctor.obj X)
          Equations
          source
          instance CategoryTheory.additive_coyonedaObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) :
          CategoryTheory.Functor.Additive (CategoryTheory.preadditiveCoyonedaObj X)
          Equations
          source
          instance CategoryTheory.additive_coyonedaObj' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) :
          CategoryTheory.Functor.Additive (CategoryTheory.preadditiveCoyoneda.toPrefunctor.obj X)
          Equations
          source
          @[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)).toPrefunctor.obj (CategoryTheory.forget AddCommGroupCat)) = CategoryTheory.yoneda

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

          source
          @[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)).toPrefunctor.obj (CategoryTheory.forget AddCommGroupCat)) = CategoryTheory.coyoneda

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

          source
          instance CategoryTheory.full_preadditiveYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
          CategoryTheory.Full CategoryTheory.preadditiveYoneda
          Equations
          • One or more equations did not get rendered due to their size.
          source
          instance CategoryTheory.full_preadditiveCoyoneda {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
          CategoryTheory.Full CategoryTheory.preadditiveCoyoneda
          Equations
          • One or more equations did not get rendered due to their size.
          source
          instance CategoryTheory.faithful_preadditiveYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
          CategoryTheory.Faithful CategoryTheory.preadditiveYoneda
          Equations
          source
          instance CategoryTheory.faithful_preadditiveCoyoneda {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] :
          CategoryTheory.Faithful CategoryTheory.preadditiveCoyoneda
          Equations