SpectralLocalField.lean

1 import PaperXI.CanonicalDVRValuation
2 import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
3 import Mathlib.Analysis.Normed.Module.FiniteDimension
4 import Mathlib.NumberTheory.LocalField.Basic
5 
6 /-!
7 # Spectral local-field structure on the constructed unramified fraction field
8 
9 The upper field is finite over the given nonarchimedean local field. This file
10 installs its spectral norm, proves completeness and local compactness, and
11 packages the norm valuation as an actual nonarchimedean local-field structure.
12 The canonical DVR valuation remains a separate explicitly named valuation; the
13 comparison of the two valued structures is not hidden in an instance.
14 -/
15 
16 set_option autoImplicit false
17 noncomputable section
18 
19 namespace PaperXI.SpectralLocalField
20 
21 open PaperXI.LocalFieldResidueExtension
22 open ValuativeRel
23 open scoped WithZero
24 
25 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
26   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
27 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
28   [FiniteDimensional 𝓀[K] s]
29 
30 private local instance baseValued : Valued K (ValueGroupWithZero K) := inferInstance
31 
32 private local instance baseRankOne :
33     Valuation.RankOne (Valued.v (R := K) (Γ₀ := ValueGroupWithZero K)) :=
34   { hom' := IsRankLeOne.nonempty.some.emb (R := K).comp
35       MonoidWithZeroHom.ValueGroup₀.embedding
36     strictMono' := IsRankLeOne.nonempty.some.strictMono.comp
37       MonoidWithZeroHom.ValueGroup₀.embedding_strictMono }
38 
39 private local instance baseNormedField : NormedField K :=
40   Valued.toNormedField K (ValueGroupWithZero K)
41 
42 private local instance baseNontriviallyNormedField : NontriviallyNormedField K :=
43   Valued.toNontriviallyNormedField K (ValueGroupWithZero K)
44 
45 abbrev UpperField := LocalFieldResidueExtension.field K s
46 
47 /-- The spectral normed-field structure on the constructed finite extension. -/
48 noncomputable instance upperNormedField : NormedField (UpperField K s) :=
49   spectralNorm.normedField K (UpperField K s)
50 
51 /-- The spectral norm is nontrivial because it extends the base-field norm. -/
52 noncomputable instance upperNontriviallyNormedField :
53     NontriviallyNormedField (UpperField K s) :=
54   spectralNorm.nontriviallyNormedField K (UpperField K s)
55 
56 /-- The upper field is a normed space over the base through the spectral norm. -/
57 noncomputable instance upperNormedSpace : NormedSpace K (UpperField K s) :=
58   spectralNorm.normedSpace K (UpperField K s)
59 
60 /-- The algebra map is norm-compatible for the spectral norm. -/
61 noncomputable instance upperNormedAlgebra : NormedAlgebra K (UpperField K s) :=
62   spectralNorm.normedAlgebra K (UpperField K s)
63 
64 /-- The spectral norm extends the original norm exactly. -/
65 theorem norm_algebraMap (x : K) :
66     ‖algebraMap K (UpperField K s) x‖ = ‖x‖ := by
67   exact_mod_cast spectralNorm_extends (K := K) (L := UpperField K s) x
68 
69 /-- The installed norm is definitionally the finite-extension spectral norm. -/
70 theorem norm_eq_spectralNorm (x : UpperField K s) :
71     ‖x‖ = (spectralNorm K (UpperField K s) x : ℝ) := rfl
72 
73 /-- The base-field embedding is an isometry for the spectral extension norm. -/
74 theorem algebraMap_isometry :
75     Isometry (algebraMap K (UpperField K s)) := by
76   refine Isometry.of_dist_eq ?_
77   intro x y
78   rw [dist_eq_norm, dist_eq_norm, ← map_sub, norm_algebraMap]
79 
80 /-- The spectral norm on the upper field is nonarchimedean. -/
81 instance upperUltrametric : IsUltrametricDist (UpperField K s) := by
82   constructor
83   intro x y z
84   change (spectralNorm K (UpperField K s) (x - z) : ℝ) ≤
85     max (spectralNorm K (UpperField K s) (x - y) : ℝ)
86       (spectralNorm K (UpperField K s) (y - z) : ℝ)
87   rw [← sub_add_sub_cancel x y z]
88   exact_mod_cast
89     (isNonarchimedean_spectralNorm (K := K) (L := UpperField K s)
90       (x - y) (y - z))
91 
92 /-- Finite extensions are complete for the spectral norm. -/
93 instance upperComplete : CompleteSpace (UpperField K s) :=
94   spectralNorm.completeSpace K (UpperField K s)
95 
96 /-- Finite extensions of a locally compact normed field are proper. -/
97 instance upperProper : ProperSpace (UpperField K s) :=
98   FiniteDimensional.proper K (UpperField K s)
99 
100 /-- In particular the spectral upper field is locally compact. -/
101 instance upperLocallyCompact : LocallyCompactSpace (UpperField K s) := by
102   infer_instance
103 
104 /-- The valued-field structure associated to the spectral norm. -/
105 private noncomputable instance upperNormValued : Valued (UpperField K s) NNReal :=
106   NormedField.toValued
107 
108 /-- The valuative relation induced by the spectral norm valuation. -/
109 noncomputable instance upperValuativeRel : ValuativeRel (UpperField K s) :=
110   ValuativeRel.ofValuation (NormedField.valuation (K := UpperField K s))
111 
112 private instance upperNormValuationCompatible :
113     (NormedField.valuation (K := UpperField K s)).Compatible :=
114   Valuation.Compatible.ofValuation _
115 
116 /-- The spectral norm topology is the topology induced by its norm valuation. -/
117 instance upperIsValuativeTopology : IsValuativeTopology (UpperField K s) := by
118   exact IsValuativeTopology.of_mem_nhds_zero_iff_vle
119     (NormedField.valuation (K := UpperField K s)) (by
120       intro U
121       exact Valued.mem_nhds_zero)
122 
123 /-- The norm valuation is nontrivial. -/
124 instance upperValuativeNontrivial :
125     ValuativeRel.IsNontrivial (UpperField K s) := by
126   exact (ValuativeRel.isNontrivial_iff_isNontrivial
127     (NormedField.valuation (K := UpperField K s))).mpr inferInstance
128 
129 /-- The canonical valuation attached to the valuative relation and the original
130 norm valuation have exactly the same integer subring. -/
131 theorem relation_integer_eq_norm_integer :
132     (ValuativeRel.valuation (UpperField K s)).integer =
133       (NormedField.valuation (K := UpperField K s)).integer := by
134   ext x
135   simp only [Valuation.mem_integer_iff]
136   simpa using
137     (ValuativeRel.isEquiv
138       (NormedField.valuation (K := UpperField K s))
139       (ValuativeRel.valuation (UpperField K s)) x 1).symm
140 
141 /-- Membership in the local-field integer ring is equivalent to spectral norm
142 at most one. -/
143 theorem mem_integer_iff_norm_le_one (x : UpperField K s) :
144     x ∈ (ValuativeRel.valuation (UpperField K s)).integer ↔ ‖x‖ ≤ 1 := by
145   rw [relation_integer_eq_norm_integer K s, Valuation.mem_integer_iff]
146   change ‖x‖₊ ≤ 1 ↔ ‖x‖ ≤ 1
147   exact NNReal.coe_le_coe
148 
149 /-- The finite spectral extension is an actual nonarchimedean local field. -/
150 instance upperIsNonarchimedeanLocalField :
151     IsNonarchimedeanLocalField (UpperField K s) where
152   toIsValuativeTopology := inferInstance
153   toLocallyCompactSpace := inferInstance
154   toIsNontrivial := inferInstance
155 
156 /-- The residue field of the spectral upper local field is finite. -/
157 instance upperFiniteResidue : Finite 𝓀[UpperField K s] := by
158   infer_instance
159 
160 /-- The local-field integer ring is a discrete valuation ring. -/
161 instance upperIntegerIsDVR :
162     IsDiscreteValuationRing 𝒪[UpperField K s] := by
163   infer_instance
164 
165 /-- The local-field value group is canonically order-isomorphic to `ℤᵐ⁰`. -/
166 def upperValueGroupIsoInt :
167     ValueGroupWithZero (UpperField K s) ≃*o ℤᵐ⁰ :=
168   IsNonarchimedeanLocalField.valueGroupWithZeroIsoInt (UpperField K s)
169 
170 /-- The spectral normed field has the already constructed extension degree. -/
171 theorem finrank_eq_residue_finrank :
172     Module.finrank K (UpperField K s) = Module.finrank 𝓀[K] s :=
173   LocalFieldResidueExtension.degree K s
174 
175 end PaperXI.SpectralLocalField

Back to source controls