# Documentation

Mathlib.RepresentationTheory.Maschke

# 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 Invertible (Fintype.card G : k).

We do the core computation in greater generality. For any [CommRing 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 π.

## Implementation Notes #

• These results assume Invertible (Fintype.card G : k) which is equivalent to the more familiar ¬(ringChar k ∣ Fintype.card G). It is possible to convert between them using invertibleOfRingCharNotDvd and not_ringChar_dvd_of_invertible.

## 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 • -).$$

def LinearMap.conjugate {k : Type u} [] {G : Type u} [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) (g : G) :

We define the conjugate of π by g, as a k-linear map.

Instances For
theorem LinearMap.conjugate_apply {k : Type u} [] {G : Type u} [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) (g : G) (v : W) :
↑() v = π ()
theorem LinearMap.conjugate_i {k : Type u} [] {G : Type u} [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) (i : V →ₗ[] W) (h : ∀ (v : V), π (i v) = v) (g : G) (v : V) :
↑() (i v) = v
def LinearMap.sumOfConjugates {k : Type u} [] (G : Type u) [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) [] :

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.)

Instances For
theorem LinearMap.sumOfConjugates_apply {k : Type u} [] (G : Type u) [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) [] (v : W) :
↑() v = Finset.sum Finset.univ fun g => ↑() v
def LinearMap.sumOfConjugatesEquivariant {k : Type u} [] (G : Type u) [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) [] :

In fact, the sum over g : G of the conjugate of π by g is a k[G]-linear map.

Instances For
theorem LinearMap.sumOfConjugatesEquivariant_apply {k : Type u} [] (G : Type u) [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) [] (v : W) :
= Finset.sum Finset.univ fun g => ↑() v
def LinearMap.equivariantProjection {k : Type u} [] (G : Type u) [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) [] [] :

We construct our k[G]-linear retraction of i as $$\frac{1}{|G|} \sum_{g \in G} g⁻¹ • π(g • -).$$

Instances For
theorem LinearMap.equivariantProjection_apply {k : Type u} [] (G : Type u) [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) [] [] (v : W) :
↑() v = ↑() Finset.sum Finset.univ fun g => ↑() v
theorem LinearMap.equivariantProjection_condition {k : Type u} [] (G : Type u) [] {V : Type v} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type w} [] [Module k W] [Module () W] [IsScalarTower k () W] (π : W →ₗ[k] V) (i : V →ₗ[] W) (h : ∀ (v : V), π (i v) = v) [] [] (v : V) :
↑() (i v) = v
theorem MonoidAlgebra.exists_leftInverse_of_injective {k : Type u} [] {G : Type u} [] [] [] {V : Type u} [] [Module k V] [Module () V] [IsScalarTower k () V] {W : Type u} [] [Module k W] [Module () W] [IsScalarTower k () W] (f : V →ₗ[] W) (hf : ) :
g, = LinearMap.id
theorem MonoidAlgebra.Submodule.exists_isCompl {k : Type u} [] {G : Type u} [] [] [] {V : Type u} [] [Module k V] [Module () V] [IsScalarTower k () V] (p : Submodule () V) :
q, IsCompl p q
instance MonoidAlgebra.Submodule.complementedLattice {k : Type u} [] {G : Type u} [] [] [] {V : Type u} [] [Module k V] [Module () V] [IsScalarTower k () V] :

This also implies an instance IsSemisimpleModule (MonoidAlgebra k G) V.