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 #

@[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) }

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

    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

      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]

        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
          @[simp]

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

          @[simp]

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