feat: port RepresentationTheory.Maschke (#2986)

Author: urkud

Mathlib.lean

@@ -1325,6 +1325,7 @@ import Mathlib.Order.WellFoundedSet
 import Mathlib.Order.WithBot
 import Mathlib.Order.Zorn
 import Mathlib.Order.ZornAtoms
+import Mathlib.RepresentationTheory.Maschke
 import Mathlib.RingTheory.Adjoin.Basic
 import Mathlib.RingTheory.AlgebraTower
 import Mathlib.RingTheory.Congruence

Mathlib/Algebra/Module/LinearMap.lean

@@ -206,8 +206,7 @@ variable [Module R M] [Module R M₂] [Module S M₃]
 
 variable {σ : R →+* S}
 
-instance : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
-    where
+instance : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃ where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -58,7 +58,7 @@ open Finset
 
 open Finsupp hiding single mapDomain
 
-universe u₁ u₂ u₃
+universe u₁ u₂ u₃ u₄
 
 variable (k : Type u₁) (G : Type u₂) {R : Type _}
 
@@ -997,7 +997,7 @@ section
 
 variable {k}
 
-variable [Monoid G] [CommSemiring k] {V W : Type u₃} [AddCommMonoid V] [Module k V]
+variable [Monoid G] [CommSemiring k] {V : Type u₃} {W : Type u₄} [AddCommMonoid V] [Module k V]
   [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] [AddCommMonoid W]
   [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W]
   (f : V →ₗ[k] W)

Mathlib/Data/Fintype/Card.lean

@@ -549,6 +549,8 @@ theorem card_ne_zero [Nonempty α] : card α ≠ 0 :=
   _root_.ne_of_gt card_pos
 #align fintype.card_ne_zero Fintype.card_ne_zero
 
+instance [Nonempty α] : NeZero (card α) := ⟨card_ne_zero⟩
+
 theorem card_le_one_iff : card α ≤ 1 ↔ ∀ a b : α, a = b :=
   let n := card α
   have hn : n = card α := rfl

Mathlib/RepresentationTheory/Maschke.lean

@@ -0,0 +1,183 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+
+! This file was ported from Lean 3 source module representation_theory.maschke
+! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.MonoidAlgebra.Basic
+import Mathlib.Algebra.CharP.Invertible
+import Mathlib.LinearAlgebra.Basis
+
+/-!
+# 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).
+-/
+
+
+universe u v w
+
+noncomputable section
+
+open Module MonoidAlgebra BigOperators
+
+/-!
+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 • -). $$
+-/
+
+namespace LinearMap
+
+set_option synthInstance.etaExperiment true
+
+-- At first we work with any `[CommRing k]`, and add the assumption that
+-- `[Invertible (Fintype.card G : k)]` when it is required.
+variable {k : Type u} [CommRing k] {G : Type u} [Group G]
+variable {V : Type v} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V]
+variable [IsScalarTower k (MonoidAlgebra k G) V]
+variable {W : Type w} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W]
+variable [IsScalarTower k (MonoidAlgebra k G) W]
+
+variable (π : W →ₗ[k] V)
+
+/-- We define the conjugate of `π` by `g`, as a `k`-linear map. -/
+def conjugate (g : G) : W →ₗ[k] V :=
+  .comp (.comp (GroupSmul.linearMap k V g⁻¹) π) (GroupSmul.linearMap k W g)
+#align linear_map.conjugate LinearMap.conjugate
+
+theorem conjugate_apply (g : G) (v : W) :
+    π.conjugate g v = MonoidAlgebra.single g⁻¹ (1 : k) • π (MonoidAlgebra.single g (1 : k) • v) :=
+  rfl
+
+variable (i : V →ₗ[MonoidAlgebra k G] W) (h : ∀ v : V, (π : W → V) (i v) = v)
+
+section
+
+theorem conjugate_i (g : G) (v : V) : (conjugate π g : W → V) (i v) = v := by
+  rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, mul_left_inv,
+    ← one_def, one_smul]
+#align linear_map.conjugate_i LinearMap.conjugate_i
+
+end
+
+variable (G) [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.)
+-/
+def sumOfConjugates : W →ₗ[k] V :=
+  ∑ g : G, π.conjugate g
+#align linear_map.sum_of_conjugates LinearMap.sumOfConjugates
+
+lemma sumOfConjugates_apply (v : W) : π.sumOfConjugates G v = ∑ g : G, π.conjugate g v :=
+  LinearMap.sum_apply _ _ _
+
+/-- In fact, the sum over `g : G` of the conjugate of `π` by `g` is a `k[G]`-linear map.
+-/
+def sumOfConjugatesEquivariant : W →ₗ[MonoidAlgebra k G] V :=
+  MonoidAlgebra.equivariantOfLinearOfComm (π.sumOfConjugates G) fun g v => by
+    simp only [sumOfConjugates_apply, Finset.smul_sum, conjugate_apply]
+    refine Fintype.sum_bijective (· * g) (Group.mulRight_bijective g) _ _ fun i ↦ ?_
+    simp only [smul_smul, single_mul_single, mul_inv_rev, mul_inv_cancel_left, one_mul]
+#align linear_map.sum_of_conjugates_equivariant LinearMap.sumOfConjugatesEquivariant
+
+theorem sumOfConjugatesEquivariant_apply (v : W) :
+    π.sumOfConjugatesEquivariant G v = ∑ g : G, π.conjugate g v :=
+  π.sumOfConjugates_apply G v
+
+section
+
+variable [Invertible (Fintype.card G : k)]
+
+/-- We construct our `k[G]`-linear retraction of `i` as
+$$ \frac{1}{|G|} \sum_{g \in G} g⁻¹ • π(g • -). $$
+-/
+def equivariantProjection : W →ₗ[MonoidAlgebra k G] V :=
+  ⅟(Fintype.card G : k) • π.sumOfConjugatesEquivariant G
+#align linear_map.equivariant_projection LinearMap.equivariantProjection
+
+theorem equivariantProjection_apply (v : W) :
+    π.equivariantProjection G v = ⅟(Fintype.card G : k) • ∑ g : G, π.conjugate g v := by
+  simp only [equivariantProjection, smul_apply, sumOfConjugatesEquivariant_apply]
+
+theorem equivariantProjection_condition (v : V) : (π.equivariantProjection G) (i v) = v := by
+  rw [equivariantProjection_apply]
+  simp only [conjugate_i π i h]
+  rw [Finset.sum_const, Finset.card_univ, nsmul_eq_smul_cast k, smul_smul,
+    Invertible.invOf_mul_self, one_smul]
+#align linear_map.equivariant_projection_condition LinearMap.equivariantProjection_condition
+
+end
+
+end LinearMap
+
+end
+
+namespace MonoidAlgebra
+
+-- Now we work over a `[Field k]`.
+variable {k : Type u} [Field k] {G : Type u} [Fintype G] [Invertible (Fintype.card G : k)]
+variable [Group G]
+variable {V : Type u} [AddCommGroup V] [Module k V] [Module (MonoidAlgebra k G) V]
+variable [IsScalarTower k (MonoidAlgebra k G) V]
+variable {W : Type u} [AddCommGroup W] [Module k W] [Module (MonoidAlgebra k G) W]
+variable [IsScalarTower k (MonoidAlgebra k G) W]
+
+theorem exists_leftInverse_of_injective (f : V →ₗ[MonoidAlgebra k G] W)
+    (hf : LinearMap.ker f = ⊥) :
+    ∃ g : W →ₗ[MonoidAlgebra k G] V, g.comp f = LinearMap.id := by
+  obtain ⟨φ, hφ⟩ := (f.restrictScalars k).exists_leftInverse_of_injective <| by
+    simp only [hf, Submodule.restrictScalars_bot, LinearMap.ker_restrictScalars]
+  refine ⟨φ.equivariantProjection G, FunLike.ext _ _ ?_⟩
+  exact φ.equivariantProjection_condition G _ <| FunLike.congr_fun hφ
+#align monoid_algebra.exists_left_inverse_of_injective MonoidAlgebra.exists_leftInverse_of_injective
+
+namespace Submodule
+
+theorem exists_isCompl (p : Submodule (MonoidAlgebra k G) V) :
+    ∃ q : Submodule (MonoidAlgebra k G) V, IsCompl p q := by
+  have : IsScalarTower k (MonoidAlgebra k G) p := p.isScalarTower'
+  rcases MonoidAlgebra.exists_leftInverse_of_injective p.subtype p.ker_subtype with ⟨f, hf⟩
+  refine ⟨LinearMap.ker f, LinearMap.isCompl_of_proj ?_⟩
+  exact FunLike.congr_fun hf
+#align monoid_algebra.submodule.exists_is_compl MonoidAlgebra.Submodule.exists_isCompl
+
+/-- This also implies an instance `IsSemisimpleModule (MonoidAlgebra k G) V`. -/
+instance complementedLattice : ComplementedLattice (Submodule (MonoidAlgebra k G) V) :=
+  ⟨exists_isCompl⟩
+#align monoid_algebra.submodule.complemented_lattice MonoidAlgebra.Submodule.complementedLattice
+
+end Submodule
+
+end MonoidAlgebra