HeisenbergCharacterProfile111.lean

1 import PaperXI.DegreeIndex110
2 import Mathlib.Algebra.Group.AddChar
3 import Mathlib.Tactic.Group
4 
5 /-! The original type-side quotient/form datum derives trace support through
6 actual commutators. Character intertwining of the original one-dimensional
7 theta is equivalent to its covariance on the literal intersection. Neither
8 result assumes the desired eta intertwiner or eta intersection dimension. -/
9 set_option autoImplicit false
10 noncomputable section
11 namespace PaperXI.HeisenbergCharacterProfile111
12 open Representation
13 
14 section QuotientForm
15 variable {K k X W : Type*} [Group K] [Field k] [AddCommGroup X] [Module k X]
16   [AddCommGroup W] [Module ℂ W]
17   (H : Subgroup K) [H.Normal]
18 
19 /-- Literal coordinates on the original K/H quotient, not on a substitute
20 finite group. Their multiplicative target is the additive vector-space group. -/
21 def coordinate (τ : (K ⧸ H) ≃* Multiplicative X) (x : K) : X :=
22   Multiplicative.toAdd (τ (QuotientGroup.mk' H x))
23 
24 theorem coordinate_surjective (τ : (K ⧸ H) ≃* Multiplicative X) :
25     Function.Surjective (coordinate H τ) := by
26   intro v
27   obtain ⟨a, ha⟩ := τ.surjective (Multiplicative.ofAdd v)
28   obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective a
29   exact ⟨x, congrArg Multiplicative.toAdd ha⟩
30 
31 theorem coordinate_eq_zero_iff (τ : (K ⧸ H) ≃* Multiplicative X) (x : K) :
32     coordinate H τ x = 0 ↔ x ∈ H := by
33   change τ (QuotientGroup.mk' H x) = 1 ↔ x ∈ H
34   constructor
35   · intro h
36     apply (QuotientGroup.eq_one_iff (N := H) x).mp
37     exact τ.injective (h.trans (map_one τ).symm)
38   · intro h
39     have hh : QuotientGroup.mk' H x = 1 := (QuotientGroup.eq_one_iff (N := H) x).mpr h
40     exact hh ▸ map_one τ
41 
42 /-- A vector-space coordinate isomorphism makes every original commutator
43 belong to H. No commutator-membership premise is supplied separately. -/
44 theorem commutator_mem (τ : (K ⧸ H) ≃* Multiplicative X) (x y : K) :
45     x * y * x⁻¹ * y⁻¹ ∈ H := by
46   apply (QuotientGroup.eq_one_iff (N := H) _).mp
47   apply τ.injective
48   simp [map_mul, map_inv, mul_assoc]
49 
50 /-- Theta evaluated on the actual group commutator, with source convention
51 `[x,y] = x*y*x⁻¹*y⁻¹`. -/
52 def characterCommutator (τ : (K ⧸ H) ≃* Multiplicative X)
53     (θ : H →* ℂˣ) (x y : K) : ℂˣ :=
54   θ ⟨x * y * x⁻¹ * y⁻¹, commutator_mem H τ x y⟩
55 
56 /-- Nondegeneracy of the declared field-valued commutator form produces an
57 actual trace detector. A nontrivial additive character need not be faithful:
58 scaling the detecting vector reaches a value on which that character is nontrivial. -/
59 theorem commutator_detection_of_nondegenerate_form
60     (τ : (K ⧸ H) ≃* Multiplicative X) (θ : H →* ℂˣ)
61     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
62     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
63     (hform : ∀ x y : K,
64       ψ (B (coordinate H τ x) (coordinate H τ y)) = characterCommutator H τ θ x y)
65     (x : K) (hx : x ∉ H) :
66     ∃ y : K, ∃ z : H, y * x * y⁻¹ = (z : K) * x ∧ θ z ≠ 1 := by
67   have hxv : coordinate H τ x ≠ 0 := fun h => hx ((coordinate_eq_zero_iff H τ x).mp h)
68   obtain ⟨u, hu⟩ : ∃ u : X, B u (coordinate H τ x) ≠ 0 := by
69     by_contra hn
70     push Not at hn
71     exact hxv (hnd (coordinate H τ x) hn)
72   obtain ⟨t, ht⟩ : ∃ t : k, ψ t ≠ 1 := by
73     by_contra hn
74     apply hψ
75     apply AddChar.ext
76     intro t
77     exact not_not.mp (not_exists.mp hn t)
78   let a := t / B u (coordinate H τ x)
79   obtain ⟨y, hy⟩ := coordinate_surjective H τ (a • u)
80   let z : H := ⟨y * x * y⁻¹ * x⁻¹, commutator_mem H τ y x⟩
81   refine ⟨y, z, ?_, ?_⟩
82   · change y * x * y⁻¹ = (y * x * y⁻¹ * x⁻¹) * x
83     group
84   · have hf := hform y x
85     rw [hy] at hf
86     have hb : B (a • u) (coordinate H τ x) = t := by
87       simp only [map_smul, LinearMap.smul_apply, smul_eq_mul]
88       exact div_mul_cancel₀ t hu
89     rw [hb] at hf
90     exact fun hz => ht (hf.trans hz)
91 
92 /-- The literal quotient/form datum of original §10 derives trace support for
93 the prescribed action, once its theta scalar restriction is attached. -/
94 theorem trace_support_of_nondegenerate_form
95     (τ : (K ⧸ H) ≃* Multiplicative X) (θ : H →* ℂˣ)
96     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
97     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
98     (hform : ∀ x y : K,
99       ψ (B (coordinate H τ x) (coordinate H τ y)) = characterCommutator H τ θ x y)
100     (η : Representation ℂ K W)
101     (hscalar : ∀ h : H, η h = (θ h : ℂ) • LinearMap.id)
102     (x : K) (hx : x ∉ H) : η.character x = 0 :=
103   HeisenbergTrace108.character_off_subgroup H θ η hscalar
104     (commutator_detection_of_nondegenerate_form H τ θ B ψ hψ hnd hform) x hx
105 
106 end QuotientForm
107 
108 section FormTransport
109 variable {K L k X : Type*} [Group K] [Group L] [Field k]
110   [AddCommGroup X] [Module k X]
111   (H : Subgroup K) (N : Subgroup L) [H.Normal] [N.Normal]
112   (ε : K ≃* L) (hmap : H.map ε.toMonoidHom = N)
113 
114 /-- Transport the declared canonical quotient through a literal group
115 dictionary that sends the original scalar subgroup to its original domain. -/
116 def transportedQuotient (τ : (L ⧸ N) ≃* Multiplicative X) :
117     (K ⧸ H) ≃* Multiplicative X :=
118   (QuotientGroup.congr H N ε hmap).trans τ
119 
120 theorem coordinate_transport (τ : (L ⧸ N) ≃* Multiplicative X) (x : K) :
121     coordinate H (transportedQuotient H N ε hmap τ) x = coordinate N τ (ε x) := rfl
122 
123 /-- The same canonical theta, pulled through the literal subgroup dictionary. -/
124 def pulledBackCharacter (φ : N →* ℂˣ) : H →* ℂˣ :=
125   φ.comp ((ε.toMonoidHom.comp H.subtype).codRestrict N
126     (fun h => hmap ▸ Subgroup.mem_map_of_mem ε.toMonoidHom h.property))
127 
128 theorem characterCommutator_transport (τ : (L ⧸ N) ≃* Multiplicative X)
129     (φ : N →* ℂˣ) (x y : K) :
130     characterCommutator H (transportedQuotient H N ε hmap τ)
131       (pulledBackCharacter H N ε hmap φ) x y =
132     characterCommutator N τ φ (ε x) (ε y) := by
133   apply congrArg φ
134   apply Subtype.ext
135   change ε (x * y * x⁻¹ * y⁻¹) = ε x * ε y * (ε x)⁻¹ * (ε y)⁻¹
136   simp only [map_mul, map_inv]
137 
138 /-- Original form coherence transfers through the quotient/subgroup
139 dictionary; it need not be independently assumed again on the actual group. -/
140 theorem form_transport (τ : (L ⧸ N) ≃* Multiplicative X) (φ : N →* ℂˣ)
141     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ)
142     (hform : ∀ x y : L,
143       ψ (B (coordinate N τ x) (coordinate N τ y)) = characterCommutator N τ φ x y)
144     (x y : K) :
145     ψ (B (coordinate H (transportedQuotient H N ε hmap τ) x)
146       (coordinate H (transportedQuotient H N ε hmap τ) y)) =
147     characterCommutator H (transportedQuotient H N ε hmap τ)
148       (pulledBackCharacter H N ε hmap φ) x y := by
149   rw [coordinate_transport, coordinate_transport, hform,
150     characterCommutator_transport]
151 
152 end FormTransport
153 
154 section CharacterIntertwining
155 variable {G : Type*} [Group G]
156 open InductionIrreducibility NormalizerIntertwining60
157 
158 /-- A nonzero intertwiner of the original one-dimensional theta is exactly
159 theta covariance on its literal conjugate intersection. Eta is absent. -/
160 theorem character_intertwinedAt_iff_covariance (D : Subgroup G) (θ : D →* ℂˣ) (g : G) :
161     IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g ↔
162       ∀ h : intersectionSubgroup D g,
163         θ (h : D) = θ (intersectionConjugation D g h) := by
164   constructor
165   · rintro ⟨T, hT⟩
166     have ht : ∀ z : ℂ, T z = z * T 1 := by
167       intro z
168       change T.toLinearMap z = z * T.toLinearMap 1
169       simpa only [smul_eq_mul, mul_one] using T.map_smul z (1 : ℂ)
170     have hn : T 1 ≠ 0 := by
171       intro h
172       apply hT
173       apply IntertwiningMap.ext
174       apply LinearMap.ext
175       intro z
176       change T z = 0
177       rw [ht, h, mul_zero]
178     intro h
179     have he := IntertwiningMap.isIntertwining _ _ T h (1 : ℂ)
180     change T ((θ (h : D) : ℂ) * 1) =
181       (θ (intersectionConjugation D g h) : ℂ) * T 1 at he
182     rw [mul_one, ht] at he
183     apply Units.ext
184     exact mul_right_cancel₀ hn he
185   · exact character_intertwinedAt g D θ
186 
187 theorem character_values_of_intertwinedAt
188     (D : Subgroup G) (θ : D →* ℂˣ) (g : G)
189     (hg : IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g)
190     (a b : G) (ha : a ∈ D) (hb : b ∈ D) (he : b = g * a * g⁻¹) :
191     θ ⟨a, ha⟩ = θ ⟨b, hb⟩ := by
192   let h : intersectionSubgroup D g := ⟨⟨a, ha⟩, by
193     change g * a * g⁻¹ ∈ D
194     rw [← he]
195     exact hb⟩
196   have hc := (character_intertwinedAt_iff_covariance D θ g).mp hg h
197   have hi : intersectionConjugation D g h = ⟨b, hb⟩ := Subtype.ext he.symm
198   rw [hi] at hc
199   exact hc
200 
201 end CharacterIntertwining
202 
203 section Actual
204 open Matrix ValuativeRel IntersectionModel108
205 open ActualCharacterType61 ActualCuspidalCandidate105 DegreeIndex110 ActualELatticeTopology60
206 
207 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
208   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
209   [IsNonarchimedeanLocalField E] [Algebra F E]
210 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
211   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
212   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
213 
214 /-- The actual scalar subgroup is normal in the actual first subgroup, since
215 the latter is contained in the literal domain-character pair normalizer. -/
216 instance actualScalarSubgroup_normal :
217     (actualScalarSubgroup F E m n e D θ).Normal where
218   conj_mem := by
219     intro a ha b
220     change ActualIntersection108.embedding F E m n e D θ (b * a * b⁻¹) ∈ D
221     rw [map_mul, map_mul, map_inv]
222     have hb : ActualIntersection108.embedding F E m n e D θ b ∈
223         CharacterNormalizer61.normalizer D θ := b.val.property.1
224     exact CharacterNormalizer61.conjugation_mem D θ hb
225       ⟨ActualIntersection108.embedding F E m n e D θ a, ha⟩
226 
227 variable {k X W : Type*} [Field k] [AddCommGroup X] [Module k X]
228   [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
229   (hDc : D ≤ matrixCongruence F E m n e)
230   (κ : Representation ℂ (compact F E m n e D θ) W)
231 
232 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m]
233   [Nonempty n] [FiniteDimensional ℂ W] in
234 /-- Attach the original canonical quotient and commutator form to the literal
235 actual first subgroup. Theta occurrence and irreducibility derive scalar action;
236 trace support is then a conclusion, rather than an independent profile premise. -/
237 theorem actual_trace_support_of_quotient_form
238     [IsIrreducible (ActualIntersection108.restriction F E m n e D θ κ)]
239     (hcontains : ActualCharacterData108.Contains F E m n e D θ hDc κ)
240     (τ : ((firstSubgroup F E m n e D θ) ⧸
241       actualScalarSubgroup F E m n e D θ) ≃* Multiplicative X)
242     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
243     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
244     (hform : ∀ x y : firstSubgroup F E m n e D θ,
245       ψ (B (coordinate (actualScalarSubgroup F E m n e D θ) τ x)
246         (coordinate (actualScalarSubgroup F E m n e D θ) τ y)) =
247       characterCommutator (actualScalarSubgroup F E m n e D θ) τ
248         (actualScalarCharacter F E m n e D θ) x y)
249     (x : firstSubgroup F E m n e D θ)
250     (hx : x ∉ actualScalarSubgroup F E m n e D θ) :
251     Representation.character (ActualIntersection108.restriction F E m n e D θ κ) x = 0 := by
252   exact trace_support_of_nondegenerate_form
253     (actualScalarSubgroup F E m n e D θ) τ (actualScalarCharacter F E m n e D θ)
254     B ψ hψ hnd hform (ActualIntersection108.restriction F E m n e D θ κ)
255     (actual_scalar F E m n e D θ hDc κ hcontains) x hx
256 
257 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m] [DecidableEq m]
258   [Nonempty n] in
259 /-- An intertwiner of the original scalar theta representation gives covariance
260 on the actual pair support. This hypothesis concerns theta, never eta. -/
261 theorem actual_covariance_of_character_intertwining (g : GL n F)
262     (hg : NormalizerIntertwining60.IntertwinedAt D
263       (MonomialInduction.scalarRepresentation θ) g)
264     (p : pairs (ActualIntersection108.embedding F E m n e D θ) g)
265     (h₁ : left (ActualIntersection108.embedding F E m n e D θ) g p ∈
266       actualScalarSubgroup F E m n e D θ)
267     (h₂ : right (ActualIntersection108.embedding F E m n e D θ) g p ∈
268       actualScalarSubgroup F E m n e D θ) :
269     actualScalarCharacter F E m n e D θ
270       ⟨left (ActualIntersection108.embedding F E m n e D θ) g p, h₁⟩ =
271     actualScalarCharacter F E m n e D θ
272       ⟨right (ActualIntersection108.embedding F E m n e D θ) g p, h₂⟩ := by
273   exact character_values_of_intertwinedAt D θ g hg
274     (ActualIntersection108.embedding F E m n e D θ
275       (left (ActualIntersection108.embedding F E m n e D θ) g p))
276     (ActualIntersection108.embedding F E m n e D θ
277       (right (ActualIntersection108.embedding F E m n e D θ) g p))
278     h₁ h₂ p.property
279 
280 /-- The candidate's actual eta Hom-line condition follows from the original
281 Heisenberg quotient/form, theta intertwining in the full field centralizer,
282 and the oriented ambient index identity. Trace and covariance are derived. -/
283 theorem actual_eta_dimension_from_quotient_form
284     [IsIrreducible (ActualIntersection108.restriction F E m n e D θ κ)]
285     (hF : Continuous (algebraMap F E)) (hDo : IsOpen (D : Set (GL n F)))
286     (hκ : SmoothDegreeQuotient.IsSmooth κ)
287     (hcontains : ActualCharacterData108.Contains F E m n e D θ hDc κ)
288     (τ : ((firstSubgroup F E m n e D θ) ⧸
289       actualScalarSubgroup F E m n e D θ) ≃* Multiplicative X)
290     (B : X →ₗ[k] X →ₗ[k] k) (ψ : AddChar k ℂˣ) (hψ : ψ ≠ 1)
291     (hnd : ∀ v : X, (∀ u : X, B u v = 0) → v = 0)
292     (hform : ∀ x y : firstSubgroup F E m n e D θ,
293       ψ (B (coordinate (actualScalarSubgroup F E m n e D θ) τ x)
294         (coordinate (actualScalarSubgroup F E m n e D θ) τ y)) =
295       characterCommutator (actualScalarSubgroup F E m n e D θ) τ
296         (actualScalarCharacter F E m n e D θ) x y)
297     (hθcentralizer : ∀ y : GL m E, NormalizerIntertwining60.IntertwinedAt D
298       (MonomialInduction.scalarRepresentation θ) (centralizerMap F E m n e y))
299     (hindex : ∀ y : GL m E,
300       ((ActualIntersection108.embedding F E m n e D θ).range ⊓
301         (ActualIntersection108.embedding F E m n e D θ).range.comap
302           (MulAut.conj (centralizerMap F E m n e y)).toMonoidHom).relIndex
303             (ActualIntersection108.embedding F E m n e D θ).range =
304       (D ⊓ D.comap (MulAut.conj (centralizerMap F E m n e y)).toMonoidHom).relIndex D) :
305     ∀ y : GL m E, Module.finrank ℂ (IntertwiningSpace107.space
306       (ActualIntersection108.embedding F E m n e D θ)
307       (ActualIntersection108.restriction F E m n e D θ κ)
308       (centralizerMap F E m n e y)) = 1 := by
309   exact actual_eta_dimension_ambient F E m n e D θ hDc κ hF hDo hκ hcontains
310     (actual_trace_support_of_quotient_form F E m n e D θ hDc κ hcontains
311       τ B ψ hψ hnd hform)
312     (fun y => actual_covariance_of_character_intertwining F E m n e D θ
313       (centralizerMap F E m n e y) (hθcentralizer y)) hindex
314 
315 end Actual
316 
317 end PaperXI.HeisenbergCharacterProfile111

Back to source controls