English
For V a k[G]-module and a group element g ∈ G, the map sending v to single g 1 • v defines a k-linear map from V to V; more explicitly, v ↦ (single g 1) • v, and this map respects addition and scalar action.
Русский
Для V — модуль над k[G] и для g ∈ G, отображение v ↦ (single g 1) · v является k-линейным отображением V → V; то есть линейность по сложению и по скалярному действию сохраняются.
LaTeX
$$$\\text{linearMap}_{k,G}(g): V \\to V, \\; v \\mapsto (\\mathrm{single}\\; g\\; 1) \\cdot v$$$
Lean4
/-- When `V` is a `k[G]`-module, multiplication by a group element `g` is a `k`-linear map. -/
def linearMap [Monoid G] [CommSemiring k] (V : Type*) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V]
[IsScalarTower k (MonoidAlgebra k G) V] (g : G) : V →ₗ[k] V
where
toFun v := single g (1 : k) • v
map_add' x y := smul_add (single g (1 : k)) x y
map_smul' _c _x := smul_algebra_smul_comm _ _ _
