LineCharacter.lean

1 import PaperXI.PacketBasis
2 
3 /-! The actual scalar character on the stabilizer of a nonzero line. -/
4 set_option autoImplicit false
5 noncomputable section
6 namespace PaperXI.LineCharacter
7 open PaperXI.CyclicAction PaperXI.PacketTransport PaperXI.FrobeniusPeriod
8 open PaperXI.GeneratedIrreducibility PaperXI.TameOrbitTransitivity
9 variable {G V : Type*} [Group G] [AddCommGroup V] [Module ℂ V]
10 
11 theorem scalar_unique {v : V} (hv : v ≠ 0) {c d : ℂ} (h : c • v = d • v) : c = d := by
12   apply sub_eq_zero.mp
13   have hs : (c - d) • v = 0 := by rw [sub_smul, h, sub_self]
14   exact (smul_eq_zero.mp hs).resolve_right hv
15 
16 theorem scalar_ne_zero (π : Representation ℂ G V) {v : V} (hv : v ≠ 0)
17     {g : G} {c : ℂ} (hc : π g v = c • v) : c ≠ 0 := by
18   intro hz
19   rw [hz, zero_smul] at hc
20   exact hv ((π.apply_bijective g).injective (hc.trans (map_zero _).symm))
21 
22 def lineStabilizer (π : Representation ℂ G V) (v : V) : Subgroup G where
23   carrier := {g | ∃ c : ℂ, π g v = c • v}
24   one_mem' := ⟨1, by simp⟩
25   mul_mem' := by
26     rintro g h ⟨c, hc⟩ ⟨d, hd⟩
27     refine ⟨c * d, ?_⟩
28     simp [map_mul, Module.End.mul_apply, hd, hc, smul_smul, mul_comm]
29   inv_mem' := by
30     rintro g ⟨c, hc⟩
31     by_cases hv : v = 0
32     · exact ⟨1, by simp [hv]⟩
33     · have hc0 := scalar_ne_zero π hv hc
34       refine ⟨c⁻¹, ?_⟩
35       apply (π.apply_bijective g).injective
36       rw [π.self_inv_apply, map_smul, hc, smul_smul, inv_mul_cancel₀ hc0, one_smul]
37 
38 /-- This group is precisely the stabilizer of the line, not just a set of eigenvalues. -/
39 theorem mem_iff_preserves_line (π : Representation ℂ G V) (v : V) (g : G) :
40     g ∈ lineStabilizer π v ↔
41       (Submodule.span ℂ {v}).map (π g) = Submodule.span ℂ {v} := by
42   constructor
43   · intro hg
44     apply le_antisymm
45     · apply Submodule.map_le_iff_le_comap.mpr
46       apply Submodule.span_le.mpr
47       intro w hw
48       have heq : w = v := Set.mem_singleton_iff.mp hw
49       subst w
50       obtain ⟨c, hc⟩ := hg
51       change π g v ∈ Submodule.span ℂ {v}
52       exact Submodule.mem_span_singleton.mpr ⟨c, hc.symm⟩
53     · intro w hw
54       have hg' := (lineStabilizer π v).inv_mem hg
55       have hle : Submodule.span ℂ {v} ≤ (Submodule.span ℂ {v}).comap (π g⁻¹) := by
56         apply Submodule.span_le.mpr
57         intro x hx
58         have heq : x = v := Set.mem_singleton_iff.mp hx
59         subst x
60         obtain ⟨c, hc⟩ := hg'
61         exact Submodule.mem_span_singleton.mpr ⟨c, hc.symm⟩
62       exact ⟨π g⁻¹ w, hle hw, π.self_inv_apply g w⟩
63   · intro h
64     have hm : π g v ∈ (Submodule.span ℂ {v}).map (π g) :=
65       ⟨v, Submodule.subset_span (Set.mem_singleton v), rfl⟩
66     rw [h] at hm
67     obtain ⟨c, hc⟩ := Submodule.mem_span_singleton.mp hm
68     exact ⟨c, hc.symm⟩
69 
70 def scalar (π : Representation ℂ G V) (v : V) (g : lineStabilizer π v) : ℂ :=
71   Classical.choose g.property
72 
73 theorem scalar_spec (π : Representation ℂ G V) (v : V) (g : lineStabilizer π v) :
74     π g v = scalar π v g • v := Classical.choose_spec g.property
75 
76 /-- The scalar action on a nonzero line is a homomorphism to C units. -/
77 def character (π : Representation ℂ G V) (v : V) (hv : v ≠ 0) :
78     lineStabilizer π v →* ℂˣ where
79   toFun g := Units.mk0 (scalar π v g) (scalar_ne_zero π hv (scalar_spec π v g))
80   map_one' := by
81     apply Units.ext
82     change scalar π v 1 = 1
83     apply scalar_unique hv
84     rw [← scalar_spec]
85     simp
86   map_mul' g h := by
87     apply Units.ext
88     change scalar π v (g * h) = scalar π v g * scalar π v h
89     apply scalar_unique hv
90     rw [← scalar_spec]
91     change π ((g : G) * (h : G)) v = _
92     simp [map_mul, Module.End.mul_apply, scalar_spec, smul_smul, mul_comm]
93 
94 theorem character_action (π : Representation ℂ G V) (v : V) (hv : v ≠ 0)
95     (g : lineStabilizer π v) : π g v = (character π v hv g : ℂ) • v := scalar_spec π v g
96 
97 theorem power_action (π : Representation ℂ G V) (φ : G) (n : ℕ) (v : V) :
98     (actionEquiv π φ ^ n) v = π (φ ^ n) v := by
99   induction n with
100   | zero => simp
101   | succ n ih =>
102     rw [pow_succ', pow_succ', map_mul]
103     change actionEquiv π φ ((actionEquiv π φ ^ n) v) = π φ (π (φ ^ n) v)
104     rw [ih]
105     rfl
106 
107 variable {M : ℕ} [NeZero M]
108 
109 theorem inertia_mem (π : Representation ℂ G V)
110     (ι : Multiplicative (ZMod M) →* G) (j : ZMod M) {v : V}
111     (hv : v ∈ packet (tameRestriction π ι) j) (a : ZMod M) :
112     ι (Multiplicative.ofAdd a) ∈ lineStabilizer π v :=
113   ⟨ZMod.stdAddChar (j * a), hv a⟩
114 
115 omit [NeZero M] in
116 theorem return_mem (π : Representation ℂ G V) (φ : G) (q : (ZMod M)ˣ)
117     (j : ZMod M) {v : V} {c : ℂ}
118     (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
119     φ ^ period q j ∈ lineStabilizer π v := by
120   refine ⟨c, ?_⟩
121   rwa [power_action] at hclose
122 
123 theorem character_on_inertia (π : Representation ℂ G V)
124     (ι : Multiplicative (ZMod M) →* G) (j : ZMod M) {v : V}
125     (hv : v ∈ packet (tameRestriction π ι) j) (hv0 : v ≠ 0) (a : ZMod M) :
126     (character π v hv0 ⟨ι (Multiplicative.ofAdd a), inertia_mem π ι j hv a⟩ : ℂ) =
127       ZMod.stdAddChar (j * a) := by
128   apply scalar_unique hv0
129   rw [← character_action]
130   exact hv a
131 
132 omit [NeZero M] in
133 theorem character_on_return (π : Representation ℂ G V) (φ : G) (q : (ZMod M)ˣ)
134     (j : ZMod M) {v : V} (hv0 : v ≠ 0) {c : ℂ}
135     (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
136     (character π v hv0 ⟨φ ^ period q j, return_mem π φ q j hclose⟩ : ℂ) = c := by
137   apply scalar_unique hv0
138   rw [← character_action]
139   change π (φ ^ period q j) v = c • v
140   rwa [power_action] at hclose
141 
142 /-- The line character is defined on the actual stabilizer of the whole packet. -/
143 theorem packet_stabilizer_iff (π : Representation ℂ G V) [Representation.IsIrreducible π]
144     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
145     (hgen : Submonoid.closure (generators ι φ) = ⊤)
146     (hrel : φ⁻¹ * ι (Multiplicative.ofAdd (1 : ZMod M)) * φ =
147       ι (Multiplicative.ofAdd (q : ZMod M)))
148     (j : ZMod M) {v : V} (hv : v ∈ packet (tameRestriction π ι) j) (hv0 : v ≠ 0)
149     {c : ℂ} (hc : c ≠ 0) (hclose : (actionEquiv π φ ^ period q j) v = c • v) (g : G) :
150     g ∈ lineStabilizer π v ↔
151       (packet (tameRestriction π ι) j).map (π g) = packet (tameRestriction π ι) j := by
152   have htop := PaperXI.PacketLines.cycleSpan_eq_top π ι φ q hgen hrel j hv hv0 hc hclose
153   have hline := PaperXI.PacketLines.packet_eq_line_of_span_top (tameRestriction π ι)
154     (actionEquiv π φ) q (geometric_relation π ι φ q hrel) j hv htop
155   rw [hline]
156   exact mem_iff_preserves_line π v g
157 
158 /-- Inertia and the return power generate a subgroup of the packet stabilizer. -/
159 theorem expected_stabilizer_le (π : Representation ℂ G V)
160     (ι : Multiplicative (ZMod M) →* G) (φ : G) (q : (ZMod M)ˣ)
161     (j : ZMod M) {v : V} (hv : v ∈ packet (tameRestriction π ι) j) {c : ℂ}
162     (hclose : (actionEquiv π φ ^ period q j) v = c • v) :
163     Subgroup.closure (Set.range ι ∪ {φ ^ period q j}) ≤ lineStabilizer π v := by
164   rw [Subgroup.closure_le]
165   intro g hg
166   rcases hg with ⟨a, rfl⟩ | hg
167   · exact inertia_mem π ι j hv a.toAdd
168   · have heq : g = φ ^ period q j := hg
169     subst g
170     exact return_mem π φ q j hclose
171 
172 end PaperXI.LineCharacter

Back to source controls