Theorems · Definition · category theory

CategoryTheory.preadditiveYoneda

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] → CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ AddCommGrpCat)

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.

Defined in

Mathlib.CategoryTheory.Preadditive.Yoneda.Basic

Cited by

17 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive