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} [CommRing k] {G : Type u} [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) (g : G) : W →ₗ[k] V

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

Equations

• LinearMap.conjugate π g = LinearMap.comp (LinearMap.comp (MonoidAlgebra.GroupSMul.linearMap k V g⁻¹) π) (MonoidAlgebra.GroupSMul.linearMap k W g)

theorem LinearMap.conjugate_apply {k : Type u} [CommRing k] {G : Type u} [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) (g : G) (v : W) : (LinearMap.conjugate π g) v = MonoidAlgebra.single g⁻¹ 1 • π (MonoidAlgebra.single g 1 • v)

theorem LinearMap.conjugate_i {k : Type u} [CommRing k] {G : Type u} [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) (i : V →ₗ[MonoidAlgebra k G] W) (h : ∀ (v : V), π (i v) = v) (g : G) (v : V) : (LinearMap.conjugate π g) (i v) = v

def LinearMap.sumOfConjugates {k : Type u} [CommRing k] (G : Type u) [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [Fintype G] : 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.)

Equations

• LinearMap.sumOfConjugates G π = Finset.sum Finset.univ fun (g : G) => LinearMap.conjugate π g

theorem LinearMap.sumOfConjugates_apply {k : Type u} [CommRing k] (G : Type u) [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [Fintype G] (v : W) : (LinearMap.sumOfConjugates G π) v = Finset.sum Finset.univ fun (g : G) => (LinearMap.conjugate π g) v

def LinearMap.sumOfConjugatesEquivariant {k : Type u} [CommRing k] (G : Type u) [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [Fintype G] : W →ₗ[MonoidAlgebra k G] V

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

Equations

• LinearMap.sumOfConjugatesEquivariant G π = MonoidAlgebra.equivariantOfLinearOfComm (LinearMap.sumOfConjugates G π) ⋯

theorem LinearMap.sumOfConjugatesEquivariant_apply {k : Type u} [CommRing k] (G : Type u) [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [Fintype G] (v : W) : (LinearMap.sumOfConjugatesEquivariant G π) v = Finset.sum Finset.univ fun (g : G) => (LinearMap.conjugate π g) v

def LinearMap.equivariantProjection {k : Type u} [CommRing k] (G : Type u) [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [Fintype G] [Invertible ↑(Fintype.card G)] : W →ₗ[MonoidAlgebra k G] V

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

Equations

• LinearMap.equivariantProjection G π = ⅟↑(Fintype.card G) • LinearMap.sumOfConjugatesEquivariant G π

theorem LinearMap.equivariantProjection_apply {k : Type u} [CommRing k] (G : Type u) [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [Fintype G] [Invertible ↑(Fintype.card G)] (v : W) : (LinearMap.equivariantProjection G π) v = ⅟↑(Fintype.card G) • Finset.sum Finset.univ fun (g : G) => (LinearMap.conjugate π g) v

theorem LinearMap.equivariantProjection_condition {k : Type u} [CommRing k] (G : Type u) [Group G] {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) (i : V →ₗ[MonoidAlgebra k G] W) (h : ∀ (v : V), π (i v) = v) [Fintype G] [Invertible ↑(Fintype.card G)] (v : V) : (LinearMap.equivariantProjection G π) (i v) = v

theorem MonoidAlgebra.exists_leftInverse_of_injective {k : Type u} [Field k] {G : Type u} [Fintype G] [Invertible ↑(Fintype.card G)] [Group G] {V : Type u} [AddCommGroup V] [Module (MonoidAlgebra k G) V] {W : Type u} [AddCommGroup W] [Module (MonoidAlgebra k G) W] (f : V →ₗ[MonoidAlgebra k G] W) (hf : LinearMap.ker f = ⊥) : ∃ (g : W →ₗ[MonoidAlgebra k G] V), LinearMap.comp g f = LinearMap.id

theorem MonoidAlgebra.Submodule.exists_isCompl {k : Type u} [Field k] {G : Type u} [Fintype G] [Invertible ↑(Fintype.card G)] [Group G] {V : Type u} [AddCommGroup V] [Module (MonoidAlgebra k G) V] (p : Submodule (MonoidAlgebra k G) V) : ∃ (q : Submodule (MonoidAlgebra k G) V), IsCompl p q

instance MonoidAlgebra.Submodule.complementedLattice {k : Type u} [Field k] {G : Type u} [Fintype G] [Invertible ↑(Fintype.card G)] [Group G] {V : Type u} [AddCommGroup V] [Module (MonoidAlgebra k G) V] : ComplementedLattice (Submodule (MonoidAlgebra k G) V)

This also implies instances IsSemisimpleModule (MonoidAlgebra k G) V and IsSemisimpleRing (MonoidAlgebra k G).

Equations

• ⋯ = ⋯

instance MonoidAlgebra.Submodule.instIsSemisimpleRingAddMonoidAlgebraToSemiringToDivisionSemiringToSemifieldRingToRingToDivisionRingToAddMonoidToSubNegMonoid {k : Type u} [Field k] {G : Type u} [Fintype G] [Invertible ↑(Fintype.card G)] [AddGroup G] : IsSemisimpleRing (AddMonoidAlgebra k G)

Equations

• ⋯ = ⋯