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 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 #

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

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

Equations
Instances For
    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) :
    (π.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) :
    (π.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] :

    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
    Instances For
      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 = g : G, (π.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] :

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

      Equations
      Instances For
        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 = g : G, (π.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] :

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

        Equations
        Instances For
          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] (v : W) :
          (LinearMap.equivariantProjection G π) v = Ring.inverse (Fintype.card G) g : G, (π.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) [Fintype G] (hcard : IsUnit (Fintype.card G)) (h : ∀ (v : V), π (i v) = v) (v : V) :
          theorem MonoidAlgebra.exists_leftInverse_of_injective {k : Type u} [Field k] {G : Type u} [Fintype G] [NeZero (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), g ∘ₗ f = LinearMap.id
          theorem MonoidAlgebra.Submodule.exists_isCompl {k : Type u} [Field k] {G : Type u} [Fintype G] [NeZero (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

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

          Equations
          • =