English
In a preadditive category C, the hom-sets are naturally modules over the natural numbers, and composition is bilinear with respect to this ℕ-action.
Русский
В преддобавительной категории C осуществляется естественная ℕ-модулярность для множеств гомоморфизмов, и композиция линейна по отношению к этому действию ℕ.
LaTeX
$$$\\text{In a preadditive category }C,\\ \\forall X,Y: \\mathrm{Obj}(C),\\ \\mathrm{Hom}_C(X,Y) \\in \\mathrm{Mod}_{\\mathbb{N}} \\text{ and } \\circ: \\mathrm{Hom}(Y,Z) \\times \\mathrm{Hom}(X,Y) \\to \\mathrm{Hom}(X,Z) \\text{ is } \\mathbb{N}\\text{-bilinear}.$$$
Lean4
instance preadditiveNatLinear : Linear ℕ C
where
smul_comp X _Y _Z r f g := by exact (Preadditive.rightComp X g).map_nsmul f r
comp_smul _X _Y Z f r g := by exact (Preadditive.leftComp Z f).map_nsmul g r
