preadditiveCoyoneda — Mathlib

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