CentralCharacterIrreducible.lean

1 import PaperXI.CentralCharacterAction
2 import PaperXI.CentralCharacterRepresentation
3 import PaperXI.AlgebraActionModule
4 import PaperXI.RepresentationStability
5 
6 /-! Irreducibility of an actual central-character representation is equivalent
7 to simplicity of its constructed twisted-algebra module. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.CentralCharacter
11 open CentralExtension
12 
13 variable {Z H A W : Type*} [CommGroup Z] [Group H] [CommGroup A] [Fintype A]
14 variable [AddCommGroup W] [Module ℂ W]
15 
16 /-- The forward action preserves and reflects irreducibility, including the
17 nonzero-space condition. -/
18 theorem irreducible_iff_simple (D : Datum Z H A) (ζ : Z →* ℂˣ)
19     (σ : Representation ℂ H W)
20     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
21     Representation.IsIrreducible σ ↔
22       IsSimpleModule (Algebra D ζ)
23         (AlgebraActionModule.Space (B := ↥(Algebra D ζ)) (toAlgebraAction D ζ σ hcentral)) := by
24   rw [RepresentationStability.irreducible_iff, AlgebraActionModule.simple_iff]
25   apply and_congr_right
26   intro _
27   constructor
28   · intro h S hS
29     exact h S ((action_stable_iff D ζ σ hcentral S).mp hS)
30   · intro h S hS
31     exact h S ((action_stable_iff D ζ σ hcentral S).mpr hS)
32 
33 /-- An actual irreducible representation supplies an actual simple module. -/
34 theorem simpleModule (D : Datum Z H A) (ζ : Z →* ℂˣ)
35     (σ : Representation ℂ H W) [Representation.IsIrreducible σ]
36     (hcentral : ∀ z, σ (D.i z) = (ζ z : ℂ) • LinearMap.id) :
37     IsSimpleModule (Algebra D ζ)
38       (AlgebraActionModule.Space (B := ↥(Algebra D ζ)) (toAlgebraAction D ζ σ hcentral)) :=
39   (irreducible_iff_simple D ζ σ hcentral).mp inferInstance
40 
41 /-- The reverse action construction preserves and reflects simplicity. -/
42 theorem ofAlgebraAction_irreducible_iff (D : Datum Z H A) (ζ : Z →* ℂˣ)
43     (φ : Algebra D ζ →ₐ[ℂ] Module.End ℂ W) :
44     Representation.IsIrreducible (ofAlgebraAction D ζ φ) ↔
45       IsSimpleModule (Algebra D ζ) (AlgebraActionModule.Space (B := ↥(Algebra D ζ)) φ) := by
46   rw [irreducible_iff_simple D ζ (ofAlgebraAction D ζ φ) (ofAlgebraAction_central D ζ φ),
47     to_ofAlgebraAction]
48 
49 end PaperXI.CentralCharacter

Back to source controls