SemisimpleProjection.lean

1 import Mathlib.RepresentationTheory.Semisimple
2 import PaperXI.RepresentationStability
3 
4 /-! A multiplicity-one summand of a semisimple representation is preserved by
5 every invariant subspace.  The splitting used here is obtained from semisimplicity,
6 not imposed as an additional assumption on the invariant subspace. -/
7 
8 set_option autoImplicit false
9 noncomputable section
10 
11 namespace PaperXI.SemisimpleProjection
12 
13 section Modules
14 
15 variable {R M N : Type*} [Ring R] [AddCommGroup M] [Module R M]
16   [AddCommGroup N] [Module R N] [IsSemisimpleModule R M] [IsSimpleModule R N]
17 
18 /-- A submodule meeting a simple quotient nontrivially contains its unique section. -/
19 theorem module_range_le_of_nonzero
20     (i : N →ₗ[R] M) (p : M →ₗ[R] N) (hi : ∀ x, p (i x) = x)
21     (hno : ∀ f : N →ₗ[R] M, (∀ x, p (f x) = 0) → f = 0)
22     (S : Submodule R M) (hS : ∃ x ∈ S, p x ≠ 0) :
23     LinearMap.range i ≤ S := by
24   let q : S →ₗ[R] N := p.comp S.subtype
25   have hq : q ≠ 0 := by
26     rintro heq
27     obtain ⟨x, hx, hpx⟩ := hS
28     exact hpx (LinearMap.congr_fun heq ⟨x, hx⟩)
29   obtain ⟨s, hs⟩ := IsSemisimpleModule.lifting_property q
30     (LinearMap.surjective_of_ne_zero hq) (LinearMap.id : N →ₗ[R] N)
31   have hsi : S.subtype.comp s = i := by
32     apply sub_eq_zero.mp
33     apply hno
34     intro x
35     change p ((s x : M) - i x) = 0
36     rw [map_sub, hi]
37     exact sub_eq_zero.mpr (LinearMap.congr_fun hs x)
38   rintro x ⟨y, rfl⟩
39   rw [← hsi]
40   exact (s y).property
41 
42 /-- The associated projection preserves every submodule. -/
43 theorem module_projection_mem
44     (i : N →ₗ[R] M) (p : M →ₗ[R] N) (hi : ∀ x, p (i x) = x)
45     (hno : ∀ f : N →ₗ[R] M, (∀ x, p (f x) = 0) → f = 0)
46     (S : Submodule R M) {x : M} (hx : x ∈ S) : i (p x) ∈ S := by
47   by_cases hpx : p x = 0
48   · simp [hpx]
49   · exact module_range_le_of_nonzero i p hi hno S ⟨x, hx, hpx⟩ ⟨p x, rfl⟩
50 
51 end Modules
52 
53 section Representations
54 
55 open Representation
56 open scoped MonoidAlgebra
57 
58 variable {k G V W : Type*} [Field k] [Group G]
59   [AddCommGroup V] [Module k V] [AddCommGroup W] [Module k W]
60   (σ : Representation k G V) (τ : Representation k G W)
61   [IsIrreducible σ] [IsSemisimpleRepresentation τ]
62 
63 /-- For a semisimple representation, a stable subspace whose projection to a
64 simple summand is nonzero contains that summand, provided the complementary
65 kernel has no copy of the simple representation. -/
66 theorem range_le_of_nonzero
67     (i : IntertwiningMap σ τ) (p : IntertwiningMap τ σ)
68     (hi : ∀ v, p (i v) = v)
69     (hno : ∀ f : IntertwiningMap σ τ, (∀ v, p (f v) = 0) → f = 0)
70     (S : Submodule k W) (hS : RepresentationStability.Stable τ S)
71     (hne : ∃ w ∈ S, p w ≠ 0) : LinearMap.range i.toLinearMap ≤ S := by
72   let : IsSemisimpleModule k[G] τ.asModule :=
73     (isSemisimpleRepresentation_iff_isSemisimpleModule_asModule τ).mp inferInstance
74   let T : Subrepresentation τ := ⟨S, hS⟩
75   let im := IntertwiningMap.equivLinearMapAsModule σ τ i
76   let pm := IntertwiningMap.equivLinearMapAsModule τ σ p
77   have hn : ∀ f : σ.asModule →ₗ[k[G]] τ.asModule,
78       (∀ v, pm (f v) = 0) → f = 0 := by
79     intro f hf
80     have hh := hno ((IntertwiningMap.equivLinearMapAsModule σ τ).symm f) hf
81     exact (IntertwiningMap.equivLinearMapAsModule σ τ).symm.injective
82       (by simpa using hh)
83   exact module_range_le_of_nonzero im pm hi hn T.asSubmodule hne
84 
85 /-- The canonical projection onto the unique simple summand preserves each
86 stable subspace of the semisimple representation. -/
87 theorem projection_mem
88     (i : IntertwiningMap σ τ) (p : IntertwiningMap τ σ)
89     (hi : ∀ v, p (i v) = v)
90     (hno : ∀ f : IntertwiningMap σ τ, (∀ v, p (f v) = 0) → f = 0)
91     (S : Submodule k W) (hS : RepresentationStability.Stable τ S)
92     {w : W} (hw : w ∈ S) : i (p w) ∈ S := by
93   by_cases hpw : p w = 0
94   · simp [hpw]
95   · exact range_le_of_nonzero σ τ i p hi hno S hS ⟨w, hw, hpw⟩ ⟨p w, rfl⟩
96 
97 end Representations
98 
99 end PaperXI.SemisimpleProjection

Back to source controls