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 [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 π.

Implementation Notes #

These results assume invertible (fintype.card G : k) which is equivalent to the more familiar ¬(ring_char k ∣ fintype.card G). It is possible to convert between them using invertible_of_ring_char_not_dvd and not_ring_char_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 • -). $$

source

noncomputable def linear_map.conjugate {k : Type u} [comm_ring k] {G : Type u} [group G] {V : Type u} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] {W : Type u} [add_comm_group W] [module k W] [module (monoid_algebra k G) W] [is_scalar_tower k (monoid_algebra k G) W] (π : W →ₗ[k] V) (g : G) :

W →ₗ[k] V

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)

source

theorem linear_map.conjugate_i {k : Type u} [comm_ring k] {G : Type u} [group G] {V : Type u} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] {W : Type u} [add_comm_group W] [module k W] [module (monoid_algebra k G) W] [is_scalar_tower k (monoid_algebra k G) W] (π : W →ₗ[k] V) (i : V →ₗ[monoid_algebra k G] W) (h : ∀ (v : V), ⇑π (⇑i v) = v) (g : G) (v : V) :

⇑(π.conjugate g) (⇑i v) = v

source

noncomputable def linear_map.sum_of_conjugates {k : Type u} [comm_ring k] (G : Type u) [group G] {V : Type u} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] {W : Type u} [add_comm_group W] [module k W] [module (monoid_algebra k G) W] [is_scalar_tower k (monoid_algebra 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

linear_map.sum_of_conjugates G π = finset.univ.sum (λ (g : G), π.conjugate g)

source

noncomputable def linear_map.sum_of_conjugates_equivariant {k : Type u} [comm_ring k] (G : Type u) [group G] {V : Type u} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] {W : Type u} [add_comm_group W] [module k W] [module (monoid_algebra k G) W] [is_scalar_tower k (monoid_algebra k G) W] (π : W →ₗ[k] V) [fintype G] :

W →ₗ[monoid_algebra k G] V

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

Equations

linear_map.sum_of_conjugates_equivariant G π = monoid_algebra.equivariant_of_linear_of_comm (linear_map.sum_of_conjugates G π) _

source

noncomputable def linear_map.equivariant_projection {k : Type u} [comm_ring k] (G : Type u) [group G] {V : Type u} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] {W : Type u} [add_comm_group W] [module k W] [module (monoid_algebra k G) W] [is_scalar_tower k (monoid_algebra k G) W] (π : W →ₗ[k] V) [fintype G] [inv : invertible ↑(fintype.card G)] :

W →ₗ[monoid_algebra k G] V

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

Equations

linear_map.equivariant_projection G π = ⅟ ↑(fintype.card G) • linear_map.sum_of_conjugates_equivariant G π

source

theorem linear_map.equivariant_projection_condition {k : Type u} [comm_ring k] (G : Type u) [group G] {V : Type u} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] {W : Type u} [add_comm_group W] [module k W] [module (monoid_algebra k G) W] [is_scalar_tower k (monoid_algebra k G) W] (π : W →ₗ[k] V) (i : V →ₗ[monoid_algebra k G] W) (h : ∀ (v : V), ⇑π (⇑i v) = v) [fintype G] [inv : invertible ↑(fintype.card G)] (v : V) :

⇑(linear_map.equivariant_projection G π) (⇑i v) = v

source

@[protected, instance]

def char_zero.fintype.card.invertible {k : Type u} [field k] {G : Type u} [fintype G] [group G] [char_zero k] :

invertible ↑(fintype.card G)

Equations

char_zero.fintype.card.invertible = invertible_of_ring_char_not_dvd char_zero.fintype.card.invertible._proof_1

source

theorem monoid_algebra.exists_left_inverse_of_injective {k : Type u} [field k] {G : Type u} [fintype G] [invertible ↑(fintype.card G)] [group G] {V : Type u} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] {W : Type u} [add_comm_group W] [module k W] [module (monoid_algebra k G) W] [is_scalar_tower k (monoid_algebra k G) W] (f : V →ₗ[monoid_algebra k G] W) (hf : linear_map.ker f = ⊥) :

∃ (g : W →ₗ[monoid_algebra k G] V), g.comp f = linear_map.id

source

theorem monoid_algebra.submodule.exists_is_compl {k : Type u} [field k] {G : Type u} [fintype G] [invertible ↑(fintype.card G)] [group G] {V : Type u} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] (p : submodule (monoid_algebra k G) V) :

∃ (q : submodule (monoid_algebra k G) V), is_compl p q

source

@[protected, instance]

def monoid_algebra.submodule.complemented_lattice {k : Type u} [field k] {G : Type u} [fintype G] [invertible ↑(fintype.card G)] [group G] {V : Type u} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] :

complemented_lattice (submodule (monoid_algebra k G) V)

This also implies an instance is_semisimple_module (monoid_algebra k G) V.