instPreadditiveSingleObj — Mathlib

English

In the category with one object and endomorphisms forming a ring, the preadditive structure on the single-object category is given by the ring multiplication acting on morphisms.

Русский

В категории с одним объектом и концевыми морфизмами образующей кольцо, предаддитивная структура задаётся умножением кольца на морфизмы.

LaTeX

$$$\text{Preadditive}((\text{SingleObj } \alpha))$ defined by ring operations$$

Lean4

instance : Preadditive (SingleObj α) where
  add_comp _ _ _ f f' g := mul_add g f f'
  comp_add _ _ _ f g g' := add_mul g g' f

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