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 Fintype.card G
invertible in k
.
We do the core computation in greater generality.
For any commutative ring k
in which Fintype.card G
is invertible,
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 π
.
Implementation Notes #
- These results assume
IsUnit (Fintype.card G : k)
which is equivalent to the more familiar¬(ringChar k ∣ Fintype.card G)
.
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 = MonoidAlgebra.GroupSMul.linearMap k V g⁻¹ ∘ₗ π ∘ₗ MonoidAlgebra.GroupSMul.linearMap k W g
Instances For
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
- LinearMap.sumOfConjugates G π = ∑ g : G, π.conjugate g
Instances For
In fact, the sum over g : G
of the conjugate of π
by g
is a k[G]
-linear map.
Equations
Instances For
We construct our k[G]
-linear retraction of i
as
$$ \frac{1}{|G|} \sum_{g \in G} g⁻¹ • π(g • -). $$
Equations
Instances For
This also implies instances IsSemisimpleModule (MonoidAlgebra k G) V
and
IsSemisimpleRing (MonoidAlgebra k G)
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯