forget₂_addCommGrp_additive — Mathlib

English

The forgetful functor forget₂ : ModuleCat R → AddCommGrpCat is additive; it preserves addition of morphisms and the zero morphism.

Русский

Функтор забывания forget₂: ModuleCat R → AddCommGrpCat сохраняет сложение гомоморфизмов и нулевой морфизм.

LaTeX

$$$F = \mathrm{forget}_{\,2} : \mathrm{ModuleCat}(R) \to \mathrm{AddCommGrpCat}$ is additive, i.e. F(f+g) = F(f) + F(g) and F(0) = 0.$$

Lean4

instance forget₂_addCommGrp_additive : (forget₂ (ModuleCat.{v} R) AddCommGrpCat).Additive where

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