preadditiveIntLinear — Mathlib

English

In a preadditive category C, the hom-sets are modules over the integers Z, and composition is bilinear with respect to the Z-action.

Русский

В преддобавительной категории C множество гомоморфизмов образует модуль над целыми числами Z, и композиция линейна по отношению к Z-действию.

LaTeX

$$$\\forall X,Y,Z:\\, \\mathrm{Hom}_C(X,Y) \\in \\mathrm{Mod}_{\\mathbb{Z}} \\text{ and } \\circ: \\mathrm{Hom}(Y,Z) \\times \\mathrm{Hom}(X,Y) \\to \\mathrm{Hom}(X,Z) \\text{ is } \\mathbb{Z}\\text{-bilinear}.$$$

Lean4

instance preadditiveIntLinear : Linear ℤ C
    where
  smul_comp X _Y _Z r f g := by exact (Preadditive.rightComp X g).map_zsmul f r
  comp_smul _X _Y Z f r g := by exact (Preadditive.leftComp Z f).map_zsmul g r

Похожие утверждения