English
The category Action V G is itself a preadditive category; in particular, each Hom-set carries an abelian group structure compatible with composition and with addition of morphisms.
Русский
Категория Action V G сама является предаддитивной категорией; в частности, для любых X,Y множество морфизмов имеет структуру абелевой группы, совместимую со сложением и композициями.
LaTeX
$$$ \text{Preadditive}(\mathrm{Action}(V,G))$$$
Lean4
instance : Preadditive (Action V G)
where
homGroup X
Y := hom_injective.addCommGroup (M₂ := X.V ⟶ Y.V) _ zero_hom add_hom neg_hom sub_hom (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
add_comp := by intros; ext; exact Preadditive.add_comp _ _ _ _ _ _
comp_add := by intros; ext; exact Preadditive.comp_add _ _ _ _ _ _
