Maschke's theorem
We prove Maschke's theorem for finite groups,
in the formulation that every submodule of a k[G] module has a complement,
when k is a field with ¬(ring_char k ∣ fintype.card G).
We do the core computation in greater generality.
For any [comm_ring k] in which [invertible (fintype.card G : k)],
and a k[G]-linear map i : V → W which admits a k-linear retraction π,
we produce a k[G]-linear retraction by
taking the average over G of the conjugates of π.
Future work
It's not so far to give the usual statement, that every finite dimensional representation of a finite group is semisimple (i.e. a direct sum of irreducibles).
We now do the key calculation in Maschke's theorem.
Given V → W, an inclusion of k[G] modules,,
assume we have some retraction π (i.e. ∀ v, π (i v) = v),
just as a k-linear map.
(When k is a field, this will be available cheaply, by choosing a basis.)
We now construct a retraction of the inclusion as a k[G]-linear map,
by the formula
$$ \frac{1}{|G|} \sum_{g \in G} g⁻¹ • π(g • -). $$
We define the conjugate of π by g, as a k-linear map.
Equations
- conjugate «π» g = ((monoid_algebra.group_smul.linear_map k V g⁻¹).comp «π»).comp (monoid_algebra.group_smul.linear_map k W g)
The sum of the conjugates of π by each element g : G, as a k-linear map.
(We postpone dividing by the size of the group as long as possible.)
Equations
- sum_of_conjugates «π» = ∑ (g : G), conjugate «π» g
In fact, the sum over g : G of the conjugate of π by g is a k[G]-linear map.
Equations
We construct our k[G]-linear retraction of i as
$$ \frac{1}{|G|} \sum_{g in G} g⁻¹ • π(g • -). $$
Equations
- equivariant_projection «π» = ⅟ ↑(fintype.card G) • sum_of_conjugates_equivariant «π»