ActualEmbeddedUniformizer58.lean

1 import PaperXI.ActualDepthZeroExtension
2 import PaperXI.CompactDegreeSeparation
3 import Mathlib.Topology.Algebra.Module.FiniteDimension
4 
5 /-!
6 # Uniformizers of actual matrix-embedded local fields
7 
8 For a continuous algebra embedding of a local field `E` into matrices over
9 `F`, its actual uniformizer has nonzero determinant degree over `F`.
10 The proof uses actual compact integral units and actual uniformizer coordinates;
11 it does not assume a determinant-norm formula or a ramification index.
12 Consequently no nonzero power belongs to any compact matrix subgroup.
13 The embedding may be noncentral. No simple-type realization is asserted here.
14 -/
15 set_option autoImplicit false
16 noncomputable section
17 namespace PaperXI.ActualEmbeddedUniformizer58
18 
19 open Matrix ValuativeRel
20 open ActualLocalUnitTopology ActualLocalUnitDecomposition ActualDepthZeroExtension
21 
22 variable (F E : Type*) [Field F] [ValuativeRel F] [TopologicalSpace F]
23   [IsNonarchimedeanLocalField F]
24   [Field E] [ValuativeRel E] [TopologicalSpace E]
25   [IsNonarchimedeanLocalField E] [Algebra F E]
26 variable (n : Type*) [Fintype n] [DecidableEq n]
27 variable (ι : E →ₐ[F] Matrix n n F)
28 
29 /-- The literal map on invertible matrices induced by the field embedding. -/
30 def unitsEmbedding : Eˣ →* GeneralLinearGroup n F :=
31   Units.map ι.toMonoidHom
32 
33 /-- The actual `E`-uniformizer, as a matrix over `F`. -/
34 def embeddedUniformizer : GeneralLinearGroup n F :=
35   unitsEmbedding F E n ι (uniformizerUnit E)
36 
37 omit [ValuativeRel F] [IsNonarchimedeanLocalField F]
38   [ValuativeRel E] [IsNonarchimedeanLocalField E] in
39 theorem unitsEmbedding_continuous (hι : Continuous ι) :
40     Continuous (unitsEmbedding F E n ι) := hι.units_map _
41 
42 theorem determinantDegree_continuous : Continuous (determinantDegree F n) :=
43   (degree_continuous F).comp GeneralLinearGroup.continuous_det
44 
45 omit [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F]
46   [ValuativeRel E] [TopologicalSpace E] [IsNonarchimedeanLocalField E] in
47 /-- The algebra embedding carries scalars from `F` to literal scalar matrices. -/
48 @[simp] theorem unitsEmbedding_baseScalar (a : Fˣ) :
49     unitsEmbedding F E n ι (Units.map (algebraMap F E).toMonoidHom a) =
50       GeneralLinearGroup.scalar n a := by
51   apply Units.ext
52   change ι (algebraMap F E (a : F)) = Matrix.scalar n (a : F)
53   rw [ι.commutes]
54   rfl
55 
56 /-- Compact integral units have zero matrix determinant degree. -/
57 @[simp] theorem determinantDegree_integral_unit (hι : Continuous ι) (u : 𝒪[E]ˣ) :
58     determinantDegree F n (unitsEmbedding F E n ι (unitEmbedding E u)) = 1 := by
59   let δ : Eˣ →* Multiplicative ℤ :=
60     (determinantDegree F n).comp (unitsEmbedding F E n ι)
61   have hδ : Continuous δ :=
62     (determinantDegree_continuous F n).comp (unitsEmbedding_continuous F E n ι hι)
63   exact CompactDegreeSeparation.compact_le_degree_ker (compactUnitSubgroup E) δ hδ
64     (isCompact_compactUnitSubgroup E) (show unitEmbedding E u ∈ compactUnitSubgroup E from
65       ⟨u, rfl⟩)
66 
67 variable [Nonempty n]
68 
69 /-- Continuity of the matrix embedding follows from the compatible local-field
70 algebra topology. Finite dimensionality is derived from the embedding itself. -/
71 theorem algebraEmbedding_continuous (hF : Continuous (algebraMap F E)) :
72     Continuous ι := by
73   let := IsTopologicalAddGroup.rightUniformSpace F
74   have := isUniformAddGroup_of_addCommGroup (G := F)
75   let : (Valued.v (R := F)).RankOne :=
76     { hom' := ValuativeRel.IsRankLeOne.nonempty.some.emb (R := F).comp
77         MonoidWithZeroHom.ValueGroup₀.embedding
78       strictMono' := ValuativeRel.IsRankLeOne.nonempty.some.strictMono.comp
79         MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
80   let : ContinuousSMul F E := continuousSMul_of_algebraMap F E hF
81   let : T2Space E := localFieldT2Space E
82   let : FiniteDimensional F E := FiniteDimensional.of_injective ι.toLinearMap ι.injective
83   open scoped Valued in
84     exact ι.toLinearMap.continuous_of_finiteDimensional
85 
86 /-- An embedded local-field uniformizer has nonzero ambient determinant degree.
87 If its degree vanished, unit/uniformizer decomposition would kill every element
88 of `Eˣ`, contradicting the known positive degree of the scalar `F`-uniformizer. -/
89 theorem embeddedUniformizer_degree_ne_one (hι : Continuous ι) :
90     determinantDegree F n (embeddedUniformizer F E n ι) ≠ 1 := by
91   intro ht
92   have hzero (a : Eˣ) : determinantDegree F n (unitsEmbedding F E n ι a) = 1 := by
93     obtain ⟨⟨u, r⟩, rfl⟩ := (normalFormEquiv E).surjective a
94     rw [normalFormEquiv_apply, map_mul, map_zpow, map_mul, map_zpow,
95       determinantDegree_integral_unit F E n ι hι u]
96     change 1 * determinantDegree F n (embeddedUniformizer F E n ι) ^ r.toAdd = 1
97     rw [ht, one_zpow, mul_one]
98   have hscalar := hzero (Units.map (algebraMap F E).toMonoidHom (uniformizerUnit F))
99   rw [unitsEmbedding_baseScalar] at hscalar
100   change determinantDegree F n (scalarUniformizer F n) = 1 at hscalar
101   rw [determinantDegree_scalarUniformizer] at hscalar
102   have hcard : (Fintype.card n : ℤ) = 0 := congrArg Multiplicative.toAdd hscalar
103   exact (Nat.ne_of_gt (Fintype.card_pos)).elim (Int.ofNat_eq_zero.mp hcard)
104 
105 /-- No nonzero power of the genuine matrix uniformizer belongs to a compact
106 matrix subgroup, without any centrality hypothesis. -/
107 theorem embeddedUniformizer_free (hι : Continuous ι)
108     (J : Subgroup (GeneralLinearGroup n F))
109     (hJ : IsCompact (J : Set (GeneralLinearGroup n F))) :
110     ∀ r : ℤ, embeddedUniformizer F E n ι ^ r ∈ J → r = 0 :=
111   CompactDegreeSeparation.hfree_from_compact_degree J (determinantDegree F n)
112     (determinantDegree_continuous F n) hJ (embeddedUniformizer F E n ι)
113     (embeddedUniformizer_degree_ne_one F E n ι hι)
114 
115 /-- The freeness theorem under the actual compatible extension topology,
116 with matrix-embedding continuity proved rather than supplied. -/
117 theorem embeddedUniformizer_free_of_algebraMap
118     (hF : Continuous (algebraMap F E))
119     (J : Subgroup (GeneralLinearGroup n F))
120     (hJ : IsCompact (J : Set (GeneralLinearGroup n F))) :
121     ∀ r : ℤ, embeddedUniformizer F E n ι ^ r ∈ J → r = 0 :=
122   embeddedUniformizer_free F E n ι (algebraEmbedding_continuous F E n ι hF) J hJ
123 
124 /-- The coordinates `t^r j` in actual matrices are unique for every compact
125 subgroup `J`; no normalization hypothesis is needed for uniqueness. -/
126 theorem normalForm_injective (hF : Continuous (algebraMap F E))
127     (J : Subgroup (GeneralLinearGroup n F))
128     (hJ : IsCompact (J : Set (GeneralLinearGroup n F))) :
129     Function.Injective (fun p : ℤ × J =>
130       embeddedUniformizer F E n ι ^ p.1 * (p.2 : GeneralLinearGroup n F)) := by
131   rintro ⟨r, j⟩ ⟨s, k⟩ h
132   let t := embeddedUniformizer F E n ι
133   change t ^ r * (j : GeneralLinearGroup n F) = t ^ s * k at h
134   have hpow : t ^ (r - s) = (k : GeneralLinearGroup n F) * (j : GeneralLinearGroup n F)⁻¹ := by
135     calc
136       t ^ (r - s) = t ^ (-s) * t ^ r := by rw [← zpow_add]; congr 1; omega
137       _ = t ^ (-s) * (t ^ r * j) * (j : GeneralLinearGroup n F)⁻¹ := by group
138       _ = t ^ (-s) * (t ^ s * k) * (j : GeneralLinearGroup n F)⁻¹ := by rw [h]
139       _ = (k : GeneralLinearGroup n F) * (j : GeneralLinearGroup n F)⁻¹ := by
140         rw [zpow_neg]; group
141   have hrs : r - s = 0 := embeddedUniformizer_free_of_algebraMap F E n ι hF J hJ
142     (r - s) (hpow ▸ J.mul_mem k.property (J.inv_mem j.property))
143   have hsr : r = s := sub_eq_zero.mp hrs
144   subst s
145   have hjk : j = k := Subtype.ext (mul_left_cancel h)
146   subst k
147   rfl
148 
149 omit [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [Nonempty n] in
150 /-- Every literal element of `Eˣ J` has uniformizer coordinates once the actual
151 integral units of `E` map into `J`. -/
152 theorem field_product_normalForm
153     (J : Subgroup (GeneralLinearGroup n F))
154     (hunits : ∀ u : 𝒪[E]ˣ, unitsEmbedding F E n ι (unitEmbedding E u) ∈ J)
155     (a : Eˣ) (j : J) :
156     ∃ r : ℤ, ∃ k : J, unitsEmbedding F E n ι a * (j : GeneralLinearGroup n F) =
157       embeddedUniformizer F E n ι ^ r * (k : GeneralLinearGroup n F) := by
158   obtain ⟨⟨u, r⟩, rfl⟩ := (normalFormEquiv E).surjective a
159   refine ⟨r.toAdd, ⟨unitsEmbedding F E n ι (unitEmbedding E u) * j,
160     J.mul_mem (hunits u) j.property⟩, ?_⟩
161   rw [normalFormEquiv_apply, mul_comm (unitEmbedding E u), map_mul, map_zpow, mul_assoc]
162   rfl
163 
164 /-- The actual product `Eˣ J` has unique integral-exponent/compact coordinates.
165 This is the coordinate input for a noncentral type-normalizer extension. -/
166 theorem field_product_unique_normalForm
167     (hF : Continuous (algebraMap F E))
168     (J : Subgroup (GeneralLinearGroup n F))
169     (hJ : IsCompact (J : Set (GeneralLinearGroup n F)))
170     (hunits : ∀ u : 𝒪[E]ˣ, unitsEmbedding F E n ι (unitEmbedding E u) ∈ J)
171     (a : Eˣ) (j : J) :
172     ∃! p : ℤ × J, unitsEmbedding F E n ι a * (j : GeneralLinearGroup n F) =
173       embeddedUniformizer F E n ι ^ p.1 * (p.2 : GeneralLinearGroup n F) := by
174   obtain ⟨r, k, h⟩ := field_product_normalForm F E n ι J hunits a j
175   exact ⟨(r, k), h, fun q hq => normalForm_injective F E n ι hF J hJ (hq.symm.trans h)⟩
176 
177 end PaperXI.ActualEmbeddedUniformizer58

Back to source controls