The category of additive commutative groups is preadditive.

instance AddCommGroupCat.instAddCommGroupHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategory (P : AddCommGroupCat) (Q : AddCommGroupCat) : AddCommGroup (P ⟶ Q)

Equations

• AddCommGroupCat.instAddCommGroupHomAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategory P Q = inferInstance

@[simp]

theorem AddCommGroupCat.hom_add_apply {P : AddCommGroupCat} {Q : AddCommGroupCat} (f : P ⟶ Q) (g : P ⟶ Q) (x : ↑P) : (f + g) x = f x + g x

instance AddCommGroupCat.instPreadditiveAddCommGroupCatInstAddCommGroupCatLargeCategory : CategoryTheory.Preadditive AddCommGroupCat

Equations

• AddCommGroupCat.instPreadditiveAddCommGroupCatInstAddCommGroupCatLargeCategory = CategoryTheory.Preadditive.mk