forget₂_additive — Mathlib

English

The forgetful functor forget₂ from Action V G to V is additive when V has forgetful structure, i.e., it preserves sums of morphisms.

Русский

Функтор forget₂ от Action V G к V аддитивен, если V обладает структурой забывания; он сохраняет суммы морфизмов.

LaTeX

$$$(\mathrm{forget}_2 (\mathrm{Action}(V,G))\, V).\mathrm{Additive}$$$

Lean4

instance forget₂_additive [HasForget V] : Functor.Additive (forget₂ (Action V G) V) where

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