ActualIntegralGeneralLinear.lean

1 import PaperXI.ActualResidueGeneralLinear
2 import PaperXI.QuotientRepresentation
3 import PaperXI.SmoothDegreeQuotient
4 import PaperXI.FiniteRepresentation
5 import Mathlib.Topology.Algebra.Group.Matrix
6 import Mathlib.Topology.Algebra.Ring.Compact
7 
8 /-!
9 # The actual compact open integral subgroup of `GL_n(K)`
10 
11 The subgroup is the image of `GL_n(𝒪[K])` in the given local field's matrix
12 group. Its compactness, openness and actual residue quotient are derived from
13 the entrywise maps. Inflation therefore gives smooth irreducible actions on
14 this actual subgroup from actual irreducible finite residue representations.
15 -/
16 set_option autoImplicit false
17 noncomputable section
18 namespace PaperXI.ActualIntegralGeneralLinear
19 
20 open Matrix ValuativeRel Topology
21 open ActualResidueGeneralLinear
22 
23 variable (K : Type*) [Field K] [ValuativeRel K]
24 variable (n : Type*) [Fintype n] [DecidableEq n]
25 
26 /-- Entrywise inclusion into the actual ambient general linear group. -/
27 def embedding : GeneralLinearGroup n 𝒪[K] →* GeneralLinearGroup n K :=
28   GeneralLinearGroup.map (valuation K).integer.subtype
29 
30 @[simp] theorem embedding_apply (g : GeneralLinearGroup n 𝒪[K]) (i j : n) :
31     embedding K n g i j = (g i j : K) := rfl
32 
33 theorem embedding_injective : Function.Injective (embedding K n) := by
34   intro g h he
35   apply GeneralLinearGroup.ext
36   intro i j
37   apply Subtype.ext
38   exact congrArg (fun A : GeneralLinearGroup n K => A i j) he
39 
40 /-- The actual integral subgroup inside `GL_n(K)`. -/
41 def integralSubgroup : Subgroup (GeneralLinearGroup n K) := (embedding K n).range
42 
43 /-- Integral matrices are identified with their actual ambient subgroup. -/
44 def integralEquiv : GeneralLinearGroup n 𝒪[K] ≃* integralSubgroup K n :=
45   MonoidHom.ofInjective (embedding_injective K n)
46 
47 @[simp] theorem integralEquiv_coe (g : GeneralLinearGroup n 𝒪[K]) :
48     (integralEquiv K n g : GeneralLinearGroup n K) = embedding K n g := rfl
49 
50 @[simp] theorem embedding_integralEquiv_symm (g : integralSubgroup K n) :
51     embedding K n ((integralEquiv K n).symm g) = g :=
52   congrArg Subtype.val ((integralEquiv K n).apply_symm_apply g)
53 
54 /-- Membership is exactly integrality of both the matrix and its inverse. -/
55 theorem mem_integralSubgroup (g : GeneralLinearGroup n K) :
56     g ∈ integralSubgroup K n ↔
57       (∀ i j, g i j ∈ (valuation K).integer) ∧
58       (∀ i j, g⁻¹ i j ∈ (valuation K).integer) := by
59   constructor
60   · rintro ⟨h, rfl⟩
61     exact ⟨fun i j => (h i j).property, fun i j => (h⁻¹ i j).property⟩
62   · rintro ⟨hg, hi⟩
63     let A : Matrix n n 𝒪[K] := fun i j => ⟨g i j, hg i j⟩
64     let B : Matrix n n 𝒪[K] := fun i j => ⟨g⁻¹ i j, hi i j⟩
65     have hA : A.map ((valuation K).integer.subtype) = (g : Matrix n n K) := rfl
66     have hB : B.map ((valuation K).integer.subtype) =
67         ((g⁻¹ : GeneralLinearGroup n K) : Matrix n n K) := rfl
68     have hab : A * B = 1 := by
69       apply Matrix.map_injective Subtype.val_injective
70       change (RingHom.mapMatrix (valuation K).integer.subtype) (A * B) =
71         (RingHom.mapMatrix (valuation K).integer.subtype) 1
72       rw [map_mul, map_one]
73       exact g.mul_inv
74     have hba : B * A = 1 := by
75       apply Matrix.map_injective Subtype.val_injective
76       change (RingHom.mapMatrix (valuation K).integer.subtype) (B * A) =
77         (RingHom.mapMatrix (valuation K).integer.subtype) 1
78       rw [map_mul, map_one]
79       exact g.inv_mul
80     exact ⟨⟨A, B, hab, hba⟩, Units.ext hA⟩
81 
82 variable [TopologicalSpace K] [IsNonarchimedeanLocalField K]
83 
84 theorem field_t2Space : T2Space K := by
85   let := IsTopologicalAddGroup.rightUniformSpace K
86   have := isUniformAddGroup_of_addCommGroup (G := K)
87   infer_instance
88 
89 local instance : T2Space K := field_t2Space K
90 
91 omit [IsNonarchimedeanLocalField K] in
92 theorem embedding_isEmbedding : IsEmbedding (embedding K n) :=
93   (IsEmbedding.subtypeVal : IsEmbedding ((valuation K).integer.subtype)).generalLinearGroup_map
94 
95 omit [IsNonarchimedeanLocalField K] in
96 theorem embedding_continuous : Continuous (embedding K n) :=
97   (embedding_isEmbedding K n).continuous
98 
99 omit [IsNonarchimedeanLocalField K] in
100 theorem integralEquiv_symm_continuous : Continuous (integralEquiv K n).symm := by
101   apply (embedding_isEmbedding K n).continuous_iff.mpr
102   have he : embedding K n ∘ (integralEquiv K n).symm =
103       (Subtype.val : integralSubgroup K n → GeneralLinearGroup n K) := by
104     funext g
105     exact embedding_integralEquiv_symm K n g
106   rw [he]
107   exact continuous_subtype_val
108 
109 /-- Compactness is inherited from finite matrices over the actual compact
110 integer ring and the topology on units. -/
111 theorem integralSubgroup_compact : IsCompact (integralSubgroup K n : Set (GeneralLinearGroup n K)) := by
112   let : CompactSpace 𝒪[K] := inferInstance
113   let : CompactSpace (Matrix n n 𝒪[K]) := inferInstanceAs (CompactSpace (n → n → 𝒪[K]))
114   let : T1Space (Matrix n n 𝒪[K]) := inferInstance
115   let : ContinuousMul (Matrix n n 𝒪[K]) := inferInstance
116   let : CompactSpace (GeneralLinearGroup n 𝒪[K]) := inferInstance
117   exact isCompact_range (embedding_continuous K n)
118 
119 /-- Integrality of a matrix and its inverse are open entrywise conditions. -/
120 theorem integralSubgroup_open : IsOpen (integralSubgroup K n : Set (GeneralLinearGroup n K)) := by
121   let U : Submonoid (Matrix n n K) := (valuation K).integer.matrix.toSubmonoid
122   have he : (integralSubgroup K n : Set (GeneralLinearGroup n K)) =
123       (U.units : Set (GeneralLinearGroup n K)) := by
124     ext g
125     exact mem_integralSubgroup K n g
126   rw [he]
127   apply Submonoid.isOpen_units
128   exact (Valuation.isOpen_integer (v := valuation K)).matrix
129 
130 /-- Literal residue reduction on the actual subgroup of the ambient group. -/
131 def reductionOnSubgroup : integralSubgroup K n →* GeneralLinearGroup n 𝓀[K] :=
132   (reduction K n).comp (integralEquiv K n).symm.toMonoidHom
133 
134 @[simp] theorem reductionOnSubgroup_integralEquiv (g : GeneralLinearGroup n 𝒪[K]) :
135     reductionOnSubgroup K n (integralEquiv K n g) = reduction K n g := by
136   simp [reductionOnSubgroup]
137 
138 theorem reductionOnSubgroup_surjective : Function.Surjective (reductionOnSubgroup K n) :=
139   (reduction_surjective K n).comp (integralEquiv K n).symm.surjective
140 
141 /-- The congruence kernel is given by entrywise congruence to the identity. -/
142 theorem mem_reduction_kernel (g : GeneralLinearGroup n 𝒪[K]) :
143     g ∈ (reduction K n).ker ↔
144       ∀ i j, g i j - (1 : Matrix n n 𝒪[K]) i j ∈ IsLocalRing.maximalIdeal 𝒪[K] := by
145   change reduction K n g = 1 ↔ _
146   rw [GeneralLinearGroup.ext_iff]
147   simp only [reduction_apply, GeneralLinearGroup.coe_one]
148   apply forall_congr'
149   intro i
150   apply forall_congr'
151   intro j
152   rw [← IsLocalRing.residue_eq_zero_iff, map_sub, sub_eq_zero]
153   simp [Matrix.one_apply]
154 
155 /-- The principal congruence kernel is open in the actual integral group. -/
156 theorem reduction_kernel_open : IsOpen ((reduction K n).ker : Set (GeneralLinearGroup n 𝒪[K])) := by
157   have he : ((reduction K n).ker : Set (GeneralLinearGroup n 𝒪[K])) =
158       ⋂ i, ⋂ j, {g : GeneralLinearGroup n 𝒪[K] |
159         g i j - (1 : Matrix n n 𝒪[K]) i j ∈ IsLocalRing.maximalIdeal 𝒪[K]} := by
160     ext g
161     simp only [Set.mem_iInter, Set.mem_ofPred_eq]
162     exact mem_reduction_kernel K n g
163   rw [he]
164   apply isOpen_iInter_of_finite
165   intro i
166   apply isOpen_iInter_of_finite
167   intro j
168   apply (IsLocalRing.isOpen_maximalIdeal 𝒪[K]).preimage
169   fun_prop
170 
171 theorem reductionOnSubgroup_kernel_open :
172     IsOpen ((reductionOnSubgroup K n).ker : Set (integralSubgroup K n)) :=
173   (reduction_kernel_open K n).preimage (integralEquiv_symm_continuous K n)
174 
175 /-- The actual principal-congruence quotient is the full finite residue
176 general linear group, by the proved surjectivity of entrywise reduction. -/
177 def residueQuotientEquiv :
178     integralSubgroup K n ⧸ (reductionOnSubgroup K n).ker ≃* GeneralLinearGroup n 𝓀[K] :=
179   QuotientGroup.quotientKerEquivOfSurjective (reductionOnSubgroup K n)
180     (reductionOnSubgroup_surjective K n)
181 
182 theorem finite_residue_quotient :
183     Finite (integralSubgroup K n ⧸ (reductionOnSubgroup K n).ker) :=
184   Finite.of_injective (residueQuotientEquiv K n) (residueQuotientEquiv K n).injective
185 
186 variable {V : Type*} [AddCommGroup V] [Module ℂ V]
187 variable (σ : Representation ℂ (GeneralLinearGroup n 𝓀[K]) V)
188 
189 /-- Inflation on the actual ambient integral subgroup, using its literal
190 entrywise residue quotient. -/
191 def inflated : Representation ℂ (integralSubgroup K n) V :=
192   σ.comp (reductionOnSubgroup K n)
193 
194 @[simp] theorem inflated_integralEquiv (g : GeneralLinearGroup n 𝒪[K]) :
195     inflated K n σ (integralEquiv K n g) = σ (reduction K n g) := by
196   simp [inflated]
197 
198 /-- Irreducibility is preserved by the proved surjective actual residue map. -/
199 theorem inflated_irreducible [Representation.IsIrreducible σ] :
200     Representation.IsIrreducible (inflated K n σ) :=
201   (QuotientRepresentation.irreducible_comp_iff (reductionOnSubgroup K n)
202     (reductionOnSubgroup_surjective K n) σ).mpr inferInstance
203 
204 /-- The open principal-congruence kernel fixes every vector after inflation. -/
205 theorem inflated_isSmooth : SmoothDegreeQuotient.IsSmooth (inflated K n σ) := by
206   intro v
207   apply Subgroup.isOpen_mono (H₁ := (reductionOnSubgroup K n).ker) _
208     (reductionOnSubgroup_kernel_open K n)
209   intro g hg
210   change σ (reductionOnSubgroup K n g) v = v
211   rw [show reductionOnSubgroup K n g = 1 from hg, map_one]
212   rfl
213 
214 /-- Finite dimension follows from the actual finite residue group and
215 irreducibility of its supplied representation. -/
216 theorem inflated_finiteDimensional [Representation.IsIrreducible σ] :
217     FiniteDimensional ℂ V := FiniteRepresentation.finiteDimensional σ
218 
219 end PaperXI.ActualIntegralGeneralLinear

Back to source controls