proposition. the canonical grading of a Group Algebra [fgap-001U]

✍️source

AddMonoidAlgebra.grade.isInternalAddMonoidAlgebra.grade.gradedAlgebraAddMonoidAlgebra.single_mem_grade

L∃∀NAGENTDRAFTED

For each \(g\in G\), let \(A_g=k[g]\) be the 1-dimensional subspace spanned by the basis element \([g]\). Then \[ k[G]=\bigoplus _{g\in G}A_g, \qquad A_gA_h\subseteq A_{gh}. \] Thus \(k[G]\) is canonically graded by the group \(G\). In Lean's additive graded-algebra interface this statement is expressed after passing from the multiplicative index \(G\) to its additive copy; each single basis element lies in its corresponding grade.

The basis and multiplication law in the Group Algebra and its universal extension give the decomposition and product containment directly; compare the construction in [sengupta2010representations, secs. 3.1--3.2, pp. 39--41]. It is distinct from the Hopf structure in the standard Hopf structure on a Group Algebra: the grading records where products land, while the coalgebra maps record how a basis element is copied and inverted.