GeneratedIrreducibility.lean

1 import PaperXI.CyclicAction
2 import Mathlib.RepresentationTheory.Irreducible
3 
4 /-! Pass from stability under explicit group generators to Mathlib's actual
5 representation irreducibility. No orbit-transitivity assumption occurs here. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.GeneratedIrreducibility
9 variable {K G V : Type*} [Field K] [Group G] [AddCommGroup V] [Module K V]
10 
11 theorem nontrivial_space (π : Representation K G V) [Representation.IsIrreducible π] :
12     Nontrivial V := by
13   by_contra h
14   have : Subsingleton V := not_nontrivial_iff_subsingleton.mp h
15   have hbt : (⊥ : Subrepresentation π) = ⊤ :=
16     Subrepresentation.toSubmodule_injective (Subsingleton.elim _ _)
17   exact bot_ne_top hbt
18 
19 /-- The invertible linear action of an actual group element. -/
20 def actionEquiv (π : Representation K G V) (g : G) : V ≃ₗ[K] V where
21   toLinearMap := π g
22   invFun := π g⁻¹
23   left_inv := π.inv_self_apply g
24   right_inv := π.self_inv_apply g
25 
26 @[simp] theorem actionEquiv_apply (π : Representation K G V) (g : G) (v : V) :
27     actionEquiv π g v = π g v := rfl
28 
29 @[simp] theorem actionEquiv_symm_apply (π : Representation K G V) (g : G) (v : V) :
30     (actionEquiv π g).symm v = π g⁻¹ v := rfl
31 
32 theorem stable_of_generators (π : Representation K G V) (s : Set G)
33     (hgen : Submonoid.closure s = ⊤) (S : Submodule K V)
34     (hs : ∀ g ∈ s, ∀ v ∈ S, π g v ∈ S) (g : G) {v : V} (hv : v ∈ S) :
35     π g v ∈ S := by
36   have hg : g ∈ Submonoid.closure s := by rw [hgen]; trivial
37   have h : ∀ w ∈ S, π g w ∈ S := by
38     induction hg using Submonoid.closure_induction with
39     | mem g hg => exact hs g hg
40     | one => intro w hw; simpa using hw
41     | mul a b _ _ ha hb =>
42       intro w hw
43       simpa [map_mul, Module.End.mul_apply] using ha (π b w) (hb w hw)
44   exact h v hv
45 
46 /-- Irreducibility is used only through the simple lattice of subrepresentations. -/
47 theorem eq_bot_or_top (π : Representation K G V) [Representation.IsIrreducible π]
48     (s : Set G) (hgen : Submonoid.closure s = ⊤) (S : Submodule K V)
49     (hs : ∀ g ∈ s, ∀ v ∈ S, π g v ∈ S) : S = ⊥ ∨ S = ⊤ := by
50   let R : Subrepresentation π := ⟨S, fun g _ hv => stable_of_generators π s hgen S hs g hv⟩
51   rcases eq_bot_or_eq_top R with h | h
52   · exact Or.inl (congrArg Subrepresentation.toSubmodule h)
53   · exact Or.inr (congrArg Subrepresentation.toSubmodule h)
54 
55 end PaperXI.GeneratedIrreducibility

Back to source controls