preadditiveYoneda — Mathlib

Lean4
/-- 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`.
-/
@[simps obj]
def preadditiveYoneda : C ⥤ Cᵒᵖ ⥤ AddCommGrpCat.{v}
    where
  obj Y := preadditiveYonedaObj Y ⋙ forget₂ _ _
  map
    f :=
    { app := fun _ =>
        AddCommGrpCat.ofHom
          { toFun := fun g => g ≫ f
            map_zero' := Limits.zero_comp
            map_add' := fun _ _ => add_comp _ _ _ _ _ _ }
      naturality := fun _ _ _ => AddCommGrpCat.ext fun _ => Category.assoc _ _ _ }
Похожие утверждения