ArithmeticAttachment110.lean

1 import PaperXI.ActualCharacterCandidate108
2 
3 /-! A genuine residue-rank-one specialization. The finite residue representation
4 is constructed, and the full extended support follows directly from character
5 support because GL_1(E) consists of field scalars. No Heisenberg intersection
6 dimension, BK lattice index, or supplied finite cuspidal representation occurs
7 as an input. The actual simple-character/model/category leaves remain explicit. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.ArithmeticAttachment110
11 open Matrix ValuativeRel Representation
12 open scoped TensorProduct
13 open ActualCharacterType61 ActualCharacterIdentification61 ActualCharacterResidue61
14 open ActualELatticeTopology60 ActualELatticeResidue59 ActualEmbeddedUniformizer58
15 open LatticeCongruenceTopology60 ActualFieldTypeQuotient69
16 open ActualCuspidalCandidate105
17 
18 def residueOne (k : Type*) [Field k] : Representation ℂ (GL (Fin 1) k) ℂ :=
19   Representation.trivial ℂ (GL (Fin 1) k) ℂ
20 
21 theorem residueOne_irreducible (k : Type*) [Field k] :
22     IsIrreducible (residueOne k) := by
23   apply RepresentationStability.irreducible_of_stable
24   intro S _
25   exact eq_bot_or_eq_top S
26 
27 theorem residueOne_cuspidal (k : Type*) [Field k] :
28     CuspidalCartan105.Cuspidal (residueOne k) := by
29   intro S hne hproper
30   exfalso
31   apply hproper
32   apply Finset.eq_univ_of_forall
33   intro i
34   obtain ⟨j, hj⟩ := hne
35   simpa only [Subsingleton.elim i j] using hj
36 
37 theorem gl_one_scalar {E : Type*} [CommRing E] (y : GL (Fin 1) E) :
38     y = GeneralLinearGroup.scalar (Fin 1) (GeneralLinearGroup.det y) := by
39   apply Units.ext
40   ext i j
41   fin_cases i
42   fin_cases j
43   simp [GeneralLinearGroup.scalar, GeneralLinearGroup.val_det_apply]
44 
45 def tensorUnitEquiv {J k W : Type*} [Group J] [Field k]
46     [AddCommGroup W] [Module ℂ W] (q : J →* GL (Fin 1) k)
47     (κ : Representation ℂ J W) :
48     Representation.Equiv (CompactTypeTensor58.action q κ (residueOne k)) κ := by
49   refine Representation.Equiv.mk (TensorProduct.rid ℂ W) ?_
50   intro g
51   ext w
52   simp [CompactTypeTensor58.action, residueOne, Representation.tprod_apply]
53 
54 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
55   [IsNonarchimedeanLocalField F] [Field E] [ValuativeRel E] [TopologicalSpace E]
56   [IsNonarchimedeanLocalField E] [Algebra F E]
57 variable (n : Type*) [Fintype n] [DecidableEq n] [Nonempty n]
58   (e : (Fin 1 → E) ≃L[F] (n → F))
59   (D : Subgroup (GL n F)) (θ : D →* ℂˣ)
60   (hDc : D ≤ matrixCongruence F E (Fin 1) n e)
61   (hmodel : compact F E (Fin 1) n e D θ ≤ matrixType F E (Fin 1) n e)
62 variable {W : Type*} [AddCommGroup W] [Module ℂ W] [FiniteDimensional ℂ W]
63   (κ : Representation ℂ (compact F E (Fin 1) n e D θ) W)
64 
65 omit [ValuativeRel F] [IsNonarchimedeanLocalField F] [Nonempty n] in
66 theorem integral_normalization_of_full_rank_one
67     (hfull : ∀ g : GL n F,
68       g ∈ CharacterNormalizer61.normalizer D θ ↔
69         ∃ a : Eˣ, ∃ j : compact F E (Fin 1) n e D θ,
70           unitsEmbedding F E n (scalarMatrixEmbedding F E (Fin 1) n e) a *
71             (j : GL n F) = g)
72     (u : GL (Fin 1) 𝒪[E]) :
73     (coordinateAut e).symm (integralMatrix F E (Fin 1) u) ∈
74       CharacterNormalizer61.normalizer D θ := by
75   rw [gl_one_scalar u]
76   have he : (coordinateAut e).symm (integralMatrix F E (Fin 1)
77       (GeneralLinearGroup.scalar (Fin 1) (GeneralLinearGroup.det u))) =
78       unitsEmbedding F E n (scalarMatrixEmbedding F E (Fin 1) n e)
79         (ActualLocalUnitTopology.unitEmbedding E (GeneralLinearGroup.det u)) := by
80     apply (coordinateAut e).injective
81     rw [MulEquiv.apply_symm_apply, coordinateAut_unitsEmbedding,
82       ActualELatticeFieldJoin59.integralMatrix_scalar]
83   rw [he]
84   apply (hfull _).mpr
85   exact ⟨ActualLocalUnitTopology.unitEmbedding E (GeneralLinearGroup.det u), 1,
86     by simp⟩
87 
88 theorem rank_one_candidate_exists
89     (hF : Continuous (algebraMap F E))
90     (hDo : IsOpen (D : Set (GL n F)))
91     (hfull : ∀ g : GL n F,
92       g ∈ CharacterNormalizer61.normalizer D θ ↔
93         ∃ a : Eˣ, ∃ j : compact F E (Fin 1) n e D θ,
94           unitsEmbedding F E n (scalarMatrixEmbedding F E (Fin 1) n e) a *
95             (j : GL n F) = g)
96     [IsIrreducible (κ.comp (firstSubgroup F E (Fin 1) n e D θ).subtype)]
97     (hκ : SmoothDegreeQuotient.IsSmooth κ)
98     (hβ : ∀ g : GL n F,
99       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
100       NormalizerIntertwining60.IntertwinedAt (compact F E (Fin 1) n e D θ) κ g)
101     (hc : ActualCharacterData108.Contains F E (Fin 1) n e D θ hDc κ)
102     (hθsupport : ∀ g : GL n F,
103       NormalizerIntertwining60.IntertwinedAt D (MonomialInduction.scalarRepresentation θ) g →
104       ∃ j₁ j₂ : compact F E (Fin 1) n e D θ, ∃ y : GL (Fin 1) E,
105         g = (j₁ : GL n F) * centralizerMap F E (Fin 1) n e y * (j₂ : GL n F)) :
106     FiniteDimensional ℂ (W ⊗[ℂ] ℂ) ∧
107     ∃ Λ : Representation ℂ (extended F E (Fin 1) n e D θ) (W ⊗[ℂ] ℂ),
108       (∀ j : compact F E (Fin 1) n e D θ,
109         Λ (PrescribedFieldType70.compactInclusion F E n
110           (scalarMatrixEmbedding F E (Fin 1) n e)
111           (compact F E (Fin 1) n e D θ) j) =
112           CompactTypeTensor58.action (reduction F E (Fin 1) n e D θ hmodel)
113             κ (residueOne 𝓀[E]) j) ∧
114       IsIrreducible Λ ∧ SmoothDegreeQuotient.IsSmooth Λ ∧
115       FullIntertwiningLocus69.locus (extended F E (Fin 1) n e D θ) Λ =
116         (extended F E (Fin 1) n e D θ : Set (GL n F)) ∧
117       Nontrivial (IndV (extended F E (Fin 1) n e D θ).subtype Λ) ∧
118       SmoothDegreeQuotient.IsSmooth (ind (extended F E (Fin 1) n e D θ).subtype Λ) ∧
119       IsIrreducible (ind (extended F E (Fin 1) n e D θ).subtype Λ) := by
120   let : IsIrreducible (residueOne 𝓀[E]) := residueOne_irreducible 𝓀[E]
121   have hB := integral_normalization_of_full_rank_one F E n e D θ hfull
122   obtain ⟨_, hfin, Λ, hr, _, hi, hs, _, _, _, hcategory⟩ :=
123     ActualPacketTypeRealization70.candidate_exists F E (Fin 1) n e D θ hmodel
124       κ (residueOne 𝓀[E]) hF hDo hB hfull hκ hβ
125   let : Nontrivial (W ⊗[ℂ] ℂ) := GeneratedIrreducibility.nontrivial_space Λ
126   have hDJ := ActualCharacterData108.domain_le_compact F E (Fin 1) n e D θ hDc
127   have hJH : compact F E (Fin 1) n e D θ ≤ extended F E (Fin 1) n e D θ :=
128     le_sup_left
129   have hDH : D ≤ extended F E (Fin 1) n e D θ := hDJ.trans hJH
130   have hk := ActualCharacterData108.scalar_restriction F E (Fin 1) n e D θ hDc κ hc
131   have hscalar : ∀ d : D,
132       Λ (Subgroup.inclusion hDH d) = (θ d : ℂ) • LinearMap.id := by
133     intro d
134     change Λ (PrescribedFieldType70.compactInclusion F E n
135       (scalarMatrixEmbedding F E (Fin 1) n e)
136       (compact F E (Fin 1) n e D θ)
137       (ActualCharacterData108.intoCompact F E (Fin 1) n e D θ hDc d)) = _
138     rw [hr]
139     ext w
140     simp [CompactTypeTensor58.action, residueOne, Representation.tprod_apply, hk,
141       TensorProduct.smul_tmul']
142   have hI : FullIntertwiningLocus69.locus (extended F E (Fin 1) n e D θ) Λ =
143       (extended F E (Fin 1) n e D θ : Set (GL n F)) := by
144     apply Set.Subset.antisymm
145     · intro g hg
146       have hgθ := CharacterAttachment108.character_of_scalar
147         (extended F E (Fin 1) n e D θ).subtype Λ D θ (Subgroup.inclusion hDH)
148         (fun _ => rfl) hscalar g
149         ((FullTypeIntertwining105.existsAt_iff_locus _ Λ g).mpr hg)
150       obtain ⟨j₁, j₂, y, he⟩ := hθsupport g hgθ
151       rw [he, gl_one_scalar y, centralizer_scalar]
152       exact (extended F E (Fin 1) n e D θ).mul_mem
153         ((extended F E (Fin 1) n e D θ).mul_mem (hJH j₁.property)
154           ((show (unitsEmbedding F E n (scalarMatrixEmbedding F E (Fin 1) n e)).range ≤
155             extended F E (Fin 1) n e D θ from le_sup_right)
156             ⟨GeneralLinearGroup.det y, rfl⟩)) (hJH j₂.property)
157     · exact FullIntertwiningLocus69.subgroup_subset _ Λ
158   obtain ⟨hn, hsm, hir, _⟩ := hcategory hI
159   exact ⟨hfin, Λ, hr, hi, hs, hI, hn, hsm, hir⟩
160 
161 end PaperXI.ArithmeticAttachment110

Back to source controls