Theorem. Extending a group action on a ring module [fdip-003N]

Let \(k\) be a commutative unital ring, \(G\) a group and \(M\) a unital \(k\)-module. A linear action \(\rho :G\to \operatorname {Aut}_k(M)\) extends uniquely to a unital \(k\)-algebra homomorphism \[\widehat \rho :k[G]\longrightarrow \operatorname {End}_k(M),\qquad \widehat \rho \left (\sum _g a_g[g]\right )=\sum _g a_g\rho (g).\] Products of endomorphisms compose right to left. This extends the Group Algebra universal property to the actual module action; no finiteness of \(G\) is assumed.

Consequently linear \(G\)-actions correspond to unital left \(k[G]\)-module structures whose restriction along \(c\mapsto c[1_G]\) is the given scalar action. Under this correspondence, a \(k\)-linear map \(f:M\to N\) is a module map exactly when \(f\rho _M(g)=\rho _N(g)f\) for every \(g\).

[sengupta2010representations, Sections 3.1-3.2, pp. 39-41] presents the field case, with finite support for an arbitrary group. The proof above is the ring adaptation of representation/module correspondence. Mathlib's Representation.asAlgebraHom and Representation.asAlgebraHom_single supply the linear extension and its value on basis monomials. They do not assert that an arbitrary faithful group action has a faithful algebra extension. For example, \(C_2\to \mathbb R^\times \), \(r\mapsto -1\), is injective, but its algebra extension annihilates the nonzero element \(1+[r]\).