SemisimpleDetection.lean

1 import Mathlib.RepresentationTheory.Maschke
2 import PaperXI.CharacterProjector
3 
4 /-! Maschke separation: literal elements of C[G] are detected on simple modules.
5 No choice of a complete irreducible character table is assumed. -/
6 set_option autoImplicit false
7 noncomputable section
8 open scoped MonoidAlgebra BigOperators
9 namespace PaperXI.SemisimpleDetection
10 universe u
11 variable {G : Type u} [Group G] [Fintype G]
12 
13 /-- Vanishing on all simple left ideals forces an element to be zero. -/
14 theorem eq_zero_of_simple_actions (a : MonoidAlgebra ℂ G)
15     (h : ∀ S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G),
16       IsSimpleModule (MonoidAlgebra ℂ G) S →
17       (Representation.ofModule (k := ℂ) (G := G) S).asAlgebraHom a = 0) : a = 0 := by
18   let A := MonoidAlgebra ℂ G
19   have : NeZero (Nat.card G : ℂ) := ⟨by exact_mod_cast (Nat.card_pos (α := G)).ne'⟩
20   have htop : (⊤ : Submodule ℂ A) ≤ (LinearMap.mulLeft ℂ a).ker := by
21     calc
22       ⊤ = (sSup {S : Submodule A A | IsSimpleModule A S}).restrictScalars ℂ := by
23         rw [IsSemisimpleModule.sSup_simples_eq_top, Submodule.restrictScalars_top]
24       _ = sSup (Submodule.restrictScalars ℂ '' {S : Submodule A A | IsSimpleModule A S}) :=
25         Submodule.restrictScalars_sSup ℂ _
26       _ ≤ (LinearMap.mulLeft ℂ a).ker := by
27         apply sSup_le
28         rintro T ⟨S, hS, rfl⟩ x hx
29         have hz := LinearMap.congr_fun (h S hS)
30           ((RestrictScalars.addEquiv ℂ A S).symm ⟨x, hx⟩)
31         rw [Representation.ofModule_asAlgebraHom_apply_apply] at hz
32         have hv := congrArg (fun z : RestrictScalars ℂ A S =>
33           ((RestrictScalars.addEquiv ℂ A S) z).val) hz
34         change a * x = 0 at hv
35         exact hv
36   have ha := htop (show (1 : A) ∈ (⊤ : Submodule ℂ A) from trivial)
37   simpa using ha
38 
39 set_option backward.isDefEq.respectTransparency false in
40 /-- It suffices to test actual finite-dimensional irreducible representations. -/
41 theorem eq_zero_of_irreducible_actions (a : MonoidAlgebra ℂ G)
42     (h : ∀ (W : Type u) [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
43       (σ : Representation ℂ G W) [Representation.IsIrreducible σ],
44       σ.asAlgebraHom a = 0) : a = 0 := by
45   apply eq_zero_of_simple_actions a
46   intro S hS
47   have : Representation.IsIrreducible (Representation.ofModule (k := ℂ) (G := G) S) :=
48     (Representation.isSimpleModule_iff_irreducible_ofModule (k := ℂ) (G := G) S).mp hS
49   let e : RestrictScalars ℂ (MonoidAlgebra ℂ G) S ≃ₗ[ℂ] S :=
50     { toAddEquiv := RestrictScalars.addEquiv ℂ (MonoidAlgebra ℂ G) S
51       map_smul' := by
52         intro c x
53         exact (RestrictScalars.addEquiv_map_smul ℂ (MonoidAlgebra ℂ G) S c x).trans
54           (IsScalarTower.algebraMap_smul (MonoidAlgebra ℂ G) c _) }
55   have : FiniteDimensional ℂ S :=
56     Module.Finite.of_injective (S.subtype.restrictScalars ℂ) S.subtype_injective
57   have : FiniteDimensional ℂ (RestrictScalars ℂ (MonoidAlgebra ℂ G) S) :=
58     Module.Finite.equiv e.symm
59   exact h _ (Representation.ofModule (k := ℂ) (G := G) S)
60 
61 /-- Equality of group-algebra elements can be checked on irreducibles. -/
62 theorem eq_of_irreducible_actions (a b : MonoidAlgebra ℂ G)
63     (h : ∀ (W : Type u) [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
64       (σ : Representation ℂ G W) [Representation.IsIrreducible σ],
65       σ.asAlgebraHom a = σ.asAlgebraHom b) : a = b := by
66   apply sub_eq_zero.mp
67   apply eq_zero_of_irreducible_actions
68   intro W _ _ _ σ _
69   rw [map_sub, h W σ, sub_self]
70 
71 end PaperXI.SemisimpleDetection

Back to source controls