DegreeIndex110.lean

1 import PaperXI.FiniteProfileBridge109
2 import PaperXI.CompactIntersection108
3 import PaperXI.ActualIntersection108
4 import PaperXI.PairIndex110
5 
6 /-! The degree-square identity from the original irreducible character profile,
7 and the positive-index cancellation that supplies the intersection Hom line.
8 Arithmetic trace support, character covariance, and the oriented lattice-index
9 identity remain explicit hypotheses. Schur is used only on the entire action. -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.DegreeIndex110
13 open Representation FiniteProfileBridge109 IntersectionModel108
14 
15 variable {K Q G W : Type*} [Group K] [Group Q] [Group G]
16   [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
17 
18 /-- A finite model of the entire irreducible representation, with its original
19 scalar/trace profile, derives the degree-square index identity. -/
20 theorem degree_square_of_finite_model [Finite Q]
21     (q : K →* Q) (hq : Function.Surjective q)
22     (ρ : Representation ℂ Q W) [IsIrreducible ρ]
23     (H : Subgroup K) (θ : H →* ℂˣ)
24     (hd : 0 < Module.finrank ℂ W)
25     (hscalar : ∀ h : H, (ρ.comp q) h = (θ h : ℂ) • LinearMap.id)
26     (hz : ∀ x : K, x ∉ H → Representation.character (ρ.comp q) x = 0) :
27     Module.finrank ℂ W * Module.finrank ℂ W = H.index := by
28   classical
29   let : Fintype Q := Fintype.ofFinite Q
30   have he := (dimension_one_iff_of_original_profiles q hq ρ ρ H H θ θ hd
31     hscalar hscalar hz hz (fun _ _ _ => rfl)).mp
32       (Representation.IsIrreducible.finrank_intertwiningMap_self (ρ := ρ))
33   simp only [inf_idem] at he
34   have hk : q.ker ≤ H := (quotient_kernel_le_action_kernel q ρ).trans
35     (kernel_le_of_trace_support (ρ.comp q) H hd hz)
36   have hc := (H.map q).index_mul_card
37   have hp : 0 < Nat.card (H.map q) := Nat.card_pos
38   have hi : Module.finrank ℂ W * Module.finrank ℂ W = (H.map q).index :=
39     Nat.eq_of_mul_eq_mul_right hp (he.trans hc.symm)
40   exact hi.trans (image_index q hq H hk)
41 
42 /-- Irreducibility supplies positive degree, and survives the surjective
43 quotient of the entire action. No degree-square premise is supplied. -/
44 theorem degree_square_of_finite_kernel_quotient
45     (η : Representation ℂ K W) [IsIrreducible η] [Finite (K ⧸ η.ker)]
46     (H : Subgroup K) (θ : H →* ℂˣ)
47     (hscalar : ∀ h : H, η h = (θ h : ℂ) • LinearMap.id)
48     (hz : ∀ x : K, x ∉ H → η.character x = 0) :
49     Module.finrank ℂ W * Module.finrank ℂ W = H.index := by
50   let : Nontrivial W := GeneratedIrreducibility.nontrivial_space η
51   let ρ := QuotientRepresentation.descend η.ker η le_rfl
52   let : IsIrreducible ρ := QuotientRepresentation.descend_irreducible η.ker η le_rfl
53   exact degree_square_of_finite_model (QuotientGroup.mk' η.ker)
54     QuotientGroup.mk_surjective ρ H θ Module.finrank_pos hscalar hz
55 
56 /-- Compactness and smoothness construct the finite whole-action model needed
57 to derive the original Heisenberg degree identity. -/
58 theorem degree_square [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K]
59     (η : Representation ℂ K W) [IsIrreducible η]
60     (hη : SmoothDegreeQuotient.IsSmooth η)
61     (H : Subgroup K) (θ : H →* ℂˣ)
62     (hscalar : ∀ h : H, η h = (θ h : ℂ) • LinearMap.id)
63     (hz : ∀ x : K, x ∉ H → η.character x = 0) :
64     Module.finrank ℂ W * Module.finrank ℂ W = H.index := by
65   let : Finite (K ⧸ η.ker) := η.ker.quotient_finite_of_isOpen
66     (SmoothDegreeQuotient.isOpen_kernel_of_smooth η hη)
67   exact degree_square_of_finite_kernel_quotient η H θ hscalar hz
68 
69 /-- The oriented BK index identity, with a positive (therefore finite) outer
70 index, cancels the two subgroup towers. No orders of infinite groups occur. -/
71 theorem intersection_index_of_oriented_identity
72     (H I C : Subgroup K) (hCH : C ≤ H) (hCI : C ≤ I)
73     (hI : 0 < I.index) (horiented : I.index = C.relIndex H) :
74     C.relIndex I = H.index := by
75   have he : I.index * C.relIndex I = I.index * H.index := by
76     calc
77       I.index * C.relIndex I = C.index := by
78         simpa only [Nat.mul_comm] using (Subgroup.relIndex_mul_index hCI)
79       _ = C.relIndex H * H.index := (Subgroup.relIndex_mul_index hCH).symm
80       _ = I.index * H.index := by rw [← horiented]
81   exact Nat.eq_of_mul_eq_mul_left hI he
82 
83 /-- The original-profile finite character criterion is exactly the index
84 condition on the original support intersection. -/
85 theorem dimension_one_iff_original_index [Finite Q]
86     (q : K →* Q) (hq : Function.Surjective q)
87     (ρ σ : Representation ℂ Q W)
88     (H₁ H₂ : Subgroup K) (θ₁ : H₁ →* ℂˣ) (θ₂ : H₂ →* ℂˣ)
89     (hd : 0 < Module.finrank ℂ W)
90     (h₁ : ∀ h : H₁, (ρ.comp q) h = (θ₁ h : ℂ) • LinearMap.id)
91     (h₂ : ∀ h : H₂, (σ.comp q) h = (θ₂ h : ℂ) • LinearMap.id)
92     (hz₁ : ∀ p : K, p ∉ H₁ → Representation.character (ρ.comp q) p = 0)
93     (hz₂ : ∀ p : K, p ∉ H₂ → Representation.character (σ.comp q) p = 0)
94     (hc : ∀ p : K, ∀ h₁ : p ∈ H₁, ∀ h₂ : p ∈ H₂,
95       θ₁ ⟨p, h₁⟩ = θ₂ ⟨p, h₂⟩) :
96     Module.finrank ℂ (IntertwiningMap ρ σ) = 1 ↔
97       (H₁ ⊓ H₂).index = Module.finrank ℂ W * Module.finrank ℂ W := by
98   classical
99   let : Fintype Q := Fintype.ofFinite Q
100   have hk₁ : q.ker ≤ H₁ := (quotient_kernel_le_action_kernel q ρ).trans
101     (kernel_le_of_trace_support (ρ.comp q) H₁ hd hz₁)
102   have hk₂ : q.ker ≤ H₂ := (quotient_kernel_le_action_kernel q σ).trans
103     (kernel_le_of_trace_support (σ.comp q) H₂ hd hz₂)
104   have hi := image_index q hq (H₁ ⊓ H₂) (le_inf hk₁ hk₂)
105   have hcard := ((H₁ ⊓ H₂).map q).index_mul_card
106   have hp : 0 < Nat.card ((H₁ ⊓ H₂).map q) := Nat.card_pos
107   rw [dimension_one_iff_of_original_profiles q hq ρ σ H₁ H₂ θ₁ θ₂
108     hd h₁ h₂ hz₁ hz₂ hc]
109   constructor
110   · intro he
111     have heq := Nat.eq_of_mul_eq_mul_right hp (hcard.trans he.symm)
112     exact hi.symm.trans heq
113   · intro he
114     rw [hi, he] at hcard
115     exact hcard
116 
117 /-- The actual conjugate-intersection Hom line follows from profiles on the
118 original eta and compatibility of its pulled-back scalar characters, once the
119 original paired-support intersection has the correct index. -/
120 theorem intersection_dimension_one_of_index
121     (ι : K →* G) (η : Representation ℂ K W) (g : G)
122     (H : Subgroup K) (θ : H →* ℂˣ)
123     (hd : 0 < Module.finrank ℂ W)
124     (hscalar : ∀ h : H, η h = (θ h : ℂ) • LinearMap.id)
125     (hz : ∀ x : K, x ∉ H → η.character x = 0)
126     (hc : ∀ p : pairs ι g,
127       ∀ h₁ : left ι g p ∈ H, ∀ h₂ : right ι g p ∈ H,
128       θ ⟨left ι g p, h₁⟩ = θ ⟨right ι g p, h₂⟩)
129     [Finite (FiniteJointQuotient108.quotient
130       (η.comp (left ι g)) (η.comp (right ι g)))]
131     (hindex : (H.comap (left ι g) ⊓ H.comap (right ι g)).index =
132       Module.finrank ℂ W * Module.finrank ℂ W) :
133     Module.finrank ℂ (IntertwiningSpace107.space ι η g) = 1 := by
134   let A := H.comap (left ι g)
135   let B := H.comap (right ι g)
136   let θ₁ : A →* ℂˣ := θ.comp (((left ι g).comp A.subtype).codRestrict H (fun p => p.property))
137   let θ₂ : B →* ℂˣ := θ.comp (((right ι g).comp B.subtype).codRestrict H (fun p => p.property))
138   rw [CompactIntersection108.finrank_quotient ι η g]
139   apply (dimension_one_iff_original_index
140     (QuotientGroup.mk' (FiniteJointQuotient108.kernel
141       (η.comp (left ι g)) (η.comp (right ι g)))) QuotientGroup.mk_surjective
142     (FiniteJointQuotient108.first (η.comp (left ι g)) (η.comp (right ι g)))
143     (FiniteJointQuotient108.second (η.comp (left ι g)) (η.comp (right ι g)))
144     A B θ₁ θ₂ hd
145     (fun p => hscalar ⟨left ι g p, p.property⟩)
146     (fun p => hscalar ⟨right ι g p, p.property⟩)
147     (fun p hp => hz (left ι g p) hp)
148     (fun p hp => hz (right ι g p) hp) hc).mpr
149   exact hindex
150 
151 /-- Profiles on the original irreducible eta and the oriented arithmetic
152 index equality give the line on the literal conjugate-intersection space.
153 The degree and all finite quotient/profile transport premises are derived. -/
154 theorem intersection_dimension_one
155     [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K]
156     [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
157     (ι : K →* G) (hι : Function.Injective ι) (hi : Continuous ι)
158     (η : Representation ℂ K W) [IsIrreducible η]
159     (hη : SmoothDegreeQuotient.IsSmooth η) (g : G)
160     (H : Subgroup K) (θ : H →* ℂˣ)
161     (hscalar : ∀ h : H, η h = (θ h : ℂ) • LinearMap.id)
162     (hz : ∀ x : K, x ∉ H → η.character x = 0)
163     (hc : ∀ p : pairs ι g,
164       ∀ h₁ : left ι g p ∈ H, ∀ h₂ : right ι g p ∈ H,
165       θ ⟨left ι g p, h₁⟩ = θ ⟨right ι g p, h₂⟩)
166     (hI : 0 < (PairIndex110.intersection ι g).index)
167     (horiented : (PairIndex110.intersection ι g).index =
168       (PairIndex110.scalarIntersection ι H g).relIndex H) :
169     Module.finrank ℂ (IntertwiningSpace107.space ι η g) = 1 := by
170   let : Nontrivial W := GeneratedIrreducibility.nontrivial_space η
171   let : Finite (FiniteJointQuotient108.quotient
172       (η.comp (left ι g)) (η.comp (right ι g))) :=
173     CompactIntersection108.finite_quotient ι hi η hη g
174   have hd := degree_square η hη H θ hscalar hz
175   have hcindex := intersection_index_of_oriented_identity H
176     (PairIndex110.intersection ι g) (PairIndex110.scalarIntersection ι H g)
177     (PairIndex110.scalarIntersection_le ι H g)
178     (PairIndex110.scalarIntersection_le_intersection ι H g) hI horiented
179   apply intersection_dimension_one_of_index ι η g H θ Module.finrank_pos hscalar hz hc
180   exact (PairIndex110.pairSupport_index ι H g hι).trans (hcindex.trans hd.symm)
181 
182 omit [FiniteDimensional ℂ W] in
183 /-- An open embedded compact subgroup has a finite positive intersection
184 index at every ambient element. This discharges the cancellation positivity
185 premise in the actual open-subgroup application. -/
186 theorem intersection_index_pos
187     [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K]
188     [TopologicalSpace G] [IsTopologicalGroup G]
189     (ι : K →* G) (hi : Continuous ι) (ho : IsOpen (ι.range : Set G)) (g : G) :
190     0 < (PairIndex110.intersection ι g).index := by
191   have hI : IsOpen (PairIndex110.intersection ι g : Set K) :=
192     ho.preimage ((continuous_const.mul hi).mul continuous_const)
193   let : Finite (K ⧸ PairIndex110.intersection ι g) :=
194     (PairIndex110.intersection ι g).quotient_finite_of_isOpen hI
195   exact Nat.pos_of_ne_zero (Subgroup.index_ne_zero_of_finite)
196 
197 /-- The outer index in the original compact group is the corresponding
198 relative index of the literal first-coordinate ambient intersection. -/
199 theorem intersection_index_ambient (ι : K →* G) (hι : Function.Injective ι) (g : G) :
200     (PairIndex110.intersection ι g).index =
201       (ι.range ⊓ ι.range.comap (MulAut.conj g).toMonoidHom).relIndex ι.range := by
202   rw [← PairIndex110.intersection_image, MonoidHom.range_eq_map,
203     Subgroup.relIndex_map_map_of_injective _ _ hι, Subgroup.relIndex_top_right]
204 
205 theorem scalarIntersection_index_ambient
206     (ι : K →* G) (hι : Function.Injective ι) (H : Subgroup K) (g : G) :
207     (PairIndex110.scalarIntersection ι H g).relIndex H =
208       (H.map ι ⊓ (H.map ι).comap (MulAut.conj g).toMonoidHom).relIndex (H.map ι) := by
209   rw [← PairIndex110.scalarIntersection_image,
210     Subgroup.relIndex_map_map_of_injective _ _ hι]
211 
212 /-- An arithmetic identity stated on the original ambient subgroup images
213 supplies exactly the oriented identity used by the cancellation theorem. -/
214 theorem oriented_identity_of_ambient
215     (ι : K →* G) (hι : Function.Injective ι) (H : Subgroup K) (g : G)
216     (h : (ι.range ⊓ ι.range.comap (MulAut.conj g).toMonoidHom).relIndex ι.range =
217       (H.map ι ⊓ (H.map ι).comap (MulAut.conj g).toMonoidHom).relIndex (H.map ι)) :
218     (PairIndex110.intersection ι g).index =
219       (PairIndex110.scalarIntersection ι H g).relIndex H :=
220   (intersection_index_ambient ι hι g).trans
221     (h.trans (scalarIntersection_index_ambient ι hι H g).symm)
222 
223 section Actual
224 open Matrix ValuativeRel
225 open ActualCharacterType61 ActualCuspidalCandidate105 LatticeCongruenceTopology60
226 open ActualELatticeTopology60
227 
228 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
229   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
230   [IsNonarchimedeanLocalField E] [Algebra F E]
231 variable (m n : Type*) [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
232   [Nonempty n] (e : (m → E) ≃L[F] (n → F))
233   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
234 
235 /-- The original character domain inside the actual first subgroup. -/
236 def actualScalarSubgroup : Subgroup (firstSubgroup F E m n e D θ) :=
237   D.comap (ActualIntersection108.embedding F E m n e D θ)
238 
239 /-- The same original theta, carried through the actual nested subgroup map. -/
240 def actualScalarCharacter : actualScalarSubgroup F E m n e D θ →* ℂˣ :=
241   θ.comp (((ActualIntersection108.embedding F E m n e D θ).comp
242     (actualScalarSubgroup F E m n e D θ).subtype).codRestrict D (fun p => p.property))
243 
244 variable (hDc : D ≤ matrixCongruence F E m n e)
245   (κ : Representation ℂ (compact F E m n e D θ) W)
246 
247 omit [FiniteDimensional ℂ W] [ValuativeRel F] [IsNonarchimedeanLocalField F]
248   [Fintype m] [DecidableEq m] [Nonempty n] in
249 /-- Existing occurrence and restricted irreducibility supply scalar action
250 on the actual scalar subgroup; no new scalar action premise is introduced. -/
251 theorem actual_scalar
252     [IsIrreducible (ActualIntersection108.restriction F E m n e D θ κ)]
253     (hc : ActualCharacterData108.Contains F E m n e D θ hDc κ)
254     (h : actualScalarSubgroup F E m n e D θ) :
255     ActualIntersection108.restriction F E m n e D θ κ h =
256       (actualScalarCharacter F E m n e D θ h : ℂ) • LinearMap.id := by
257   exact ActualCharacterData108.scalar_restriction F E m n e D θ hDc κ hc
258     ⟨ActualIntersection108.embedding F E m n e D θ h, h.property⟩
259 
260 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Fintype m]
261   [DecidableEq m] [Nonempty n] in
262 include hDc in
263 /-- The scalar subgroup image is exactly the original character domain D. -/
264 theorem actualScalarSubgroup_image :
265     (actualScalarSubgroup F E m n e D θ).map
266       (ActualIntersection108.embedding F E m n e D θ) = D := by
267   apply Subgroup.map_comap_eq_self
268   intro d hd
269   let dc := ActualCharacterData108.intoCompact F E m n e D θ hDc ⟨d, hd⟩
270   have hf : dc ∈ firstSubgroup F E m n e D θ :=
271     ActualCharacterData108.intoCompact_mem_first F E m n e D θ hDc ⟨d, hd⟩
272   exact ⟨⟨dc, hf⟩, rfl⟩
273 
274 /-- The literal first-subgroup embedding has open range in the ambient group. -/
275 theorem actual_embedding_range_open
276     (hF : Continuous (algebraMap F E)) (hDo : IsOpen (D : Set (GL n F))) :
277     IsOpen ((ActualIntersection108.embedding F E m n e D θ).range : Set (GL n F)) := by
278   have hrange : ((ActualIntersection108.embedding F E m n e D θ).range : Set (GL n F)) =
279       (compact F E m n e D θ).subtype ''
280         (firstSubgroup F E m n e D θ : Set (compact F E m n e D θ)) := by
281     ext x
282     constructor
283     · rintro ⟨a, rfl⟩
284       exact ⟨(a : compact F E m n e D θ), a.property, rfl⟩
285     · rintro ⟨a, ha, rfl⟩
286       exact ⟨⟨a, ha⟩, rfl⟩
287   rw [hrange]
288   exact (compactGroup_compact_open F E m n e D θ hF hDo).2.isOpenMap_subtype_val _
289     (firstSubgroup_open F E m n e D θ hF)
290 
291 /-- Conditional discharge of the candidate's literal eta-dimension premise
292 at one ambient element, for the same prescribed kappa and original theta.
293 Only trace support, character covariance, and the positive oriented arithmetic
294 index identity remain to be instantiated by the simple-character model. -/
295 theorem actual_eta_dimension_one
296     [IsIrreducible (ActualIntersection108.restriction F E m n e D θ κ)]
297     (hF : Continuous (algebraMap F E)) (hDo : IsOpen (D : Set (GL n F)))
298     (hκ : SmoothDegreeQuotient.IsSmooth κ)
299     (hcontains : ActualCharacterData108.Contains F E m n e D θ hDc κ)
300     (hz : ∀ x : firstSubgroup F E m n e D θ,
301       x ∉ actualScalarSubgroup F E m n e D θ →
302       Representation.character (ActualIntersection108.restriction F E m n e D θ κ) x = 0)
303     (g : GL n F)
304     (hc : ∀ p : pairs (ActualIntersection108.embedding F E m n e D θ) g,
305       ∀ h₁ : ActualIntersection108.embedding F E m n e D θ
306         (left (ActualIntersection108.embedding F E m n e D θ) g p) ∈ D,
307       ∀ h₂ : ActualIntersection108.embedding F E m n e D θ
308         (right (ActualIntersection108.embedding F E m n e D θ) g p) ∈ D,
309       θ ⟨ActualIntersection108.embedding F E m n e D θ
310         (left (ActualIntersection108.embedding F E m n e D θ) g p), h₁⟩ =
311       θ ⟨ActualIntersection108.embedding F E m n e D θ
312         (right (ActualIntersection108.embedding F E m n e D θ) g p), h₂⟩)
313     (hI : 0 < (PairIndex110.intersection
314       (ActualIntersection108.embedding F E m n e D θ) g).index)
315     (horiented : (PairIndex110.intersection
316       (ActualIntersection108.embedding F E m n e D θ) g).index =
317       (PairIndex110.scalarIntersection (ActualIntersection108.embedding F E m n e D θ)
318         (actualScalarSubgroup F E m n e D θ) g).relIndex
319           (actualScalarSubgroup F E m n e D θ)) :
320     Module.finrank ℂ (IntertwiningSpace107.space
321       (ActualIntersection108.embedding F E m n e D θ)
322       (ActualIntersection108.restriction F E m n e D θ κ) g) = 1 := by
323   let : CompactSpace (compact F E m n e D θ) := isCompact_iff_compactSpace.mp
324     (compactGroup_compact_open F E m n e D θ hF hDo).1
325   let : CompactSpace (firstSubgroup F E m n e D θ) := isCompact_iff_compactSpace.mp
326     ((firstSubgroup F E m n e D θ).isClosed_of_isOpen
327       (firstSubgroup_open F E m n e D θ hF)).isCompact
328   have hι : Function.Injective (ActualIntersection108.embedding F E m n e D θ) := by
329     intro a b h
330     exact Subtype.ext (Subtype.ext h)
331   exact intersection_dimension_one (ActualIntersection108.embedding F E m n e D θ)
332     hι (continuous_subtype_val.comp continuous_subtype_val)
333     (ActualIntersection108.restriction F E m n e D θ κ)
334     (CompactIntersection108.smooth_comp κ hκ
335       (firstSubgroup F E m n e D θ).subtype continuous_subtype_val) g
336     (actualScalarSubgroup F E m n e D θ) (actualScalarCharacter F E m n e D θ)
337     (actual_scalar F E m n e D θ hDc κ hcontains) hz hc hI horiented
338 
339 /-- The exact universally quantified eta-dimension input of the prescribed
340 candidate, from its original theta profile, covariance at every centralizer
341 element, and the oriented lattice-index identity. Positive finite indices,
342 the degree-square identity, and the common finite model are all derived. -/
343 theorem actual_eta_dimension
344     [IsIrreducible (ActualIntersection108.restriction F E m n e D θ κ)]
345     (hF : Continuous (algebraMap F E)) (hDo : IsOpen (D : Set (GL n F)))
346     (hκ : SmoothDegreeQuotient.IsSmooth κ)
347     (hcontains : ActualCharacterData108.Contains F E m n e D θ hDc κ)
348     (hz : ∀ x : firstSubgroup F E m n e D θ,
349       x ∉ actualScalarSubgroup F E m n e D θ →
350       Representation.character (ActualIntersection108.restriction F E m n e D θ κ) x = 0)
351     (hc : ∀ y : GL m E,
352       ∀ p : pairs (ActualIntersection108.embedding F E m n e D θ)
353         (centralizerMap F E m n e y),
354       ∀ h₁ : left (ActualIntersection108.embedding F E m n e D θ)
355         (centralizerMap F E m n e y) p ∈ actualScalarSubgroup F E m n e D θ,
356       ∀ h₂ : right (ActualIntersection108.embedding F E m n e D θ)
357         (centralizerMap F E m n e y) p ∈ actualScalarSubgroup F E m n e D θ,
358       actualScalarCharacter F E m n e D θ
359         ⟨left (ActualIntersection108.embedding F E m n e D θ)
360           (centralizerMap F E m n e y) p, h₁⟩ =
361       actualScalarCharacter F E m n e D θ
362         ⟨right (ActualIntersection108.embedding F E m n e D θ)
363           (centralizerMap F E m n e y) p, h₂⟩)
364     (horiented : ∀ y : GL m E,
365       (PairIndex110.intersection (ActualIntersection108.embedding F E m n e D θ)
366         (centralizerMap F E m n e y)).index =
367       (PairIndex110.scalarIntersection (ActualIntersection108.embedding F E m n e D θ)
368         (actualScalarSubgroup F E m n e D θ)
369           (centralizerMap F E m n e y)).relIndex (actualScalarSubgroup F E m n e D θ)) :
370     ∀ y : GL m E, Module.finrank ℂ (IntertwiningSpace107.space
371       (ActualIntersection108.embedding F E m n e D θ)
372       (ActualIntersection108.restriction F E m n e D θ κ)
373       (centralizerMap F E m n e y)) = 1 := by
374   let : CompactSpace (compact F E m n e D θ) := isCompact_iff_compactSpace.mp
375     (compactGroup_compact_open F E m n e D θ hF hDo).1
376   let : CompactSpace (firstSubgroup F E m n e D θ) := isCompact_iff_compactSpace.mp
377     ((firstSubgroup F E m n e D θ).isClosed_of_isOpen
378       (firstSubgroup_open F E m n e D θ hF)).isCompact
379   intro y
380   exact actual_eta_dimension_one F E m n e D θ hDc κ hF hDo hκ hcontains hz
381     (centralizerMap F E m n e y) (hc y)
382     (intersection_index_pos (ActualIntersection108.embedding F E m n e D θ)
383       (continuous_subtype_val.comp continuous_subtype_val)
384       (actual_embedding_range_open F E m n e D θ hF hDo)
385       (centralizerMap F E m n e y)) (horiented y)
386 
387 /-- The candidate's exact eta-dimension input from an arithmetic index identity
388 on the original ambient D and actual first-subgroup image. All other generic
389 degree, quotient, index, and scalar-attachment premises are derived. -/
390 theorem actual_eta_dimension_ambient
391     [IsIrreducible (ActualIntersection108.restriction F E m n e D θ κ)]
392     (hF : Continuous (algebraMap F E)) (hDo : IsOpen (D : Set (GL n F)))
393     (hκ : SmoothDegreeQuotient.IsSmooth κ)
394     (hcontains : ActualCharacterData108.Contains F E m n e D θ hDc κ)
395     (hz : ∀ x : firstSubgroup F E m n e D θ,
396       x ∉ actualScalarSubgroup F E m n e D θ →
397       Representation.character (ActualIntersection108.restriction F E m n e D θ κ) x = 0)
398     (hc : ∀ y : GL m E,
399       ∀ p : pairs (ActualIntersection108.embedding F E m n e D θ)
400         (centralizerMap F E m n e y),
401       ∀ h₁ : left (ActualIntersection108.embedding F E m n e D θ)
402         (centralizerMap F E m n e y) p ∈ actualScalarSubgroup F E m n e D θ,
403       ∀ h₂ : right (ActualIntersection108.embedding F E m n e D θ)
404         (centralizerMap F E m n e y) p ∈ actualScalarSubgroup F E m n e D θ,
405       actualScalarCharacter F E m n e D θ
406         ⟨left (ActualIntersection108.embedding F E m n e D θ)
407           (centralizerMap F E m n e y) p, h₁⟩ =
408       actualScalarCharacter F E m n e D θ
409         ⟨right (ActualIntersection108.embedding F E m n e D θ)
410           (centralizerMap F E m n e y) p, h₂⟩)
411     (hindex : ∀ y : GL m E,
412       ((ActualIntersection108.embedding F E m n e D θ).range ⊓
413         (ActualIntersection108.embedding F E m n e D θ).range.comap
414           (MulAut.conj (centralizerMap F E m n e y)).toMonoidHom).relIndex
415             (ActualIntersection108.embedding F E m n e D θ).range =
416       (D ⊓ D.comap (MulAut.conj (centralizerMap F E m n e y)).toMonoidHom).relIndex D) :
417     ∀ y : GL m E, Module.finrank ℂ (IntertwiningSpace107.space
418       (ActualIntersection108.embedding F E m n e D θ)
419       (ActualIntersection108.restriction F E m n e D θ κ)
420       (centralizerMap F E m n e y)) = 1 := by
421   apply actual_eta_dimension F E m n e D θ hDc κ hF hDo hκ hcontains hz hc
422   intro y
423   have hι : Function.Injective (ActualIntersection108.embedding F E m n e D θ) := by
424     intro a b h
425     exact Subtype.ext (Subtype.ext h)
426   apply oriented_identity_of_ambient (ActualIntersection108.embedding F E m n e D θ)
427     hι (actualScalarSubgroup F E m n e D θ) (centralizerMap F E m n e y)
428   simpa only [actualScalarSubgroup_image F E m n e D θ hDc] using hindex y
429 
430 end Actual
431 
432 end PaperXI.DegreeIndex110

Back to source controls