RepresentationStability.lean

1 import PaperXI.GeneratedIrreducibility
2 
3 /-! An explicit invariant-subspace criterion for actual irreducibility. This
4 interface keeps the nonzero-space condition when comparing group actions and
5 algebra actions. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.RepresentationStability
9 
10 variable {k G W : Type*} [Field k] [Group G] [AddCommGroup W] [Module k W]
11 
12 /-- Invariance under every actual group operator. -/
13 def Stable (ρ : Representation k G W) (S : Submodule k W) : Prop :=
14   ∀ g w, w ∈ S → ρ g w ∈ S
15 
16 /-- Every stable subspace in an irreducible representation is zero or the whole space. -/
17 theorem eq_bot_or_top (ρ : Representation k G W) [Representation.IsIrreducible ρ]
18     (S : Submodule k W) (hS : Stable ρ S) : S = ⊥ ∨ S = ⊤ := by
19   let T : Subrepresentation ρ := ⟨S, hS⟩
20   rcases eq_bot_or_eq_top T with h | h
21   · exact Or.inl (congrArg Subrepresentation.toSubmodule h)
22   · exact Or.inr (congrArg Subrepresentation.toSubmodule h)
23 
24 /-- The stable-subspace condition together with nontriviality proves irreducibility. -/
25 theorem irreducible_of_stable (ρ : Representation k G W) [Nontrivial W]
26     (h : ∀ S : Submodule k W, Stable ρ S → S = ⊥ ∨ S = ⊤) :
27     Representation.IsIrreducible ρ := by
28   let : Nontrivial (Subrepresentation ρ) :=
29     ⟨⟨⊥, ⊤, fun heq => bot_ne_top (congrArg Subrepresentation.toSubmodule heq)⟩⟩
30   refine ⟨fun S => ?_⟩
31   rcases h S.toSubmodule S.apply_mem_toSubmodule with hS | hS
32   · exact Or.inl (Subrepresentation.toSubmodule_injective hS)
33   · exact Or.inr (Subrepresentation.toSubmodule_injective hS)
34 
35 /-- No zero representation is hidden in the invariant-subspace formulation. -/
36 theorem irreducible_iff (ρ : Representation k G W) :
37     Representation.IsIrreducible ρ ↔ Nontrivial W ∧
38       ∀ S : Submodule k W, Stable ρ S → S = ⊥ ∨ S = ⊤ := by
39   constructor
40   · intro h
41     let : Representation.IsIrreducible ρ := h
42     exact ⟨GeneratedIrreducibility.nontrivial_space ρ, eq_bot_or_top ρ⟩
43   · rintro ⟨hW, h⟩
44     let : Nontrivial W := hW
45     exact irreducible_of_stable ρ h
46 
47 end PaperXI.RepresentationStability

Back to source controls