CanonicalDVRValuation.lean

1 import PaperXI.LocalFieldResidueExtension
2 import Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
3 
4 /-!
5 # The canonical adic valuation of the constructed upper DVR
6 
7 The fraction field constructed in `LocalFieldResidueExtension` is literally the
8 fraction field of the constructed DVR.  Consequently Mathlib's maximal-ideal
9 valuation identifies that DVR with the valuation unit ball.  This file records
10 that identification and proves the unit/uniformizer normalization required by
11 the local-field attachment.
12 -/
13 
14 set_option autoImplicit false
15 noncomputable section
16 
17 namespace PaperXI.CanonicalDVRValuation
18 
19 open IsLocalRing IsDiscreteValuationRing Valuation ValuativeRel
20 open scoped WithZero
21 
22 section Generic
23 
24 variable (A F : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
25   [Field F] [Algebra A F] [IsFractionRing A F]
26 
27 /-- The maximal-ideal valuation on the fraction field of a DVR. -/
28 abbrev canonicalValuation : Valuation F ℤᵐ⁰ :=
29   (IsDiscreteValuationRing.maximalIdeal A).valuation F
30 
31 /-- The DVR is canonically isomorphic to the unit ball of its adic valuation. -/
32 def integerRingEquiv :
33     A ≃+* (canonicalValuation A F).valuationSubring :=
34   IsDiscreteValuationRing.equivValuationSubring
35 
36 @[simp]
37 theorem integerRingEquiv_coe (x : A) :
38     (((integerRingEquiv A F x : (canonicalValuation A F).valuationSubring) : F)) =
39       algebraMap A F x := by
40   rfl
41 
42 /-- Literal equality of the embedded DVR and the canonical valuation unit ball. -/
43 theorem integerRing_image :
44     Subring.map (algebraMap A F) ⊤ =
45       (canonicalValuation A F).valuationSubring.toSubring :=
46   IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring
47 
48 /-- An element of the fraction field is integral exactly when it is represented
49 by an element of the DVR. -/
50 theorem integer_iff_exists_lift (x : F) :
51     canonicalValuation A F x ≤ 1 ↔
52       ∃ a : A, algebraMap A F a = x := by
53   constructor
54   · exact fun hx => IsDiscreteValuationRing.exists_lift_of_le_one hx
55   · rintro ⟨a, rfl⟩
56     exact (IsDiscreteValuationRing.maximalIdeal A).valuation_le_one (K := F) a
57 
58 /-- Every DVR unit has canonical valuation one. -/
59 theorem unit_value (u : A) (hu : IsUnit u) :
60     canonicalValuation A F (algebraMap A F u) = 1 := by
61   exact Valuation.Integers.one_of_isUnit' hu
62     (fun x => (IsDiscreteValuationRing.maximalIdeal A).valuation_le_one (K := F) x)
63 
64 /-- Membership in the DVR maximal ideal is detected by strict valuation. -/
65 theorem maximalIdeal_iff_value_lt_one (x : A) :
66     canonicalValuation A F (algebraMap A F x) < 1 ↔
67       x ∈ IsLocalRing.maximalIdeal A := by
68   exact (IsDiscreteValuationRing.maximalIdeal A).valuation_lt_one_iff_mem (K := F) x
69 
70 /-- A chosen generator of the DVR maximal ideal is a uniformizer for the
71 canonical fraction-field valuation. -/
72 theorem uniformizer_isUniformizer (π : A)
73     (hπ : Ideal.span {π} = IsLocalRing.maximalIdeal A) :
74     (canonicalValuation A F).IsUniformizer (algebraMap A F π) := by
75   let e := integerRingEquiv A F
76   have hgen : IsLocalRing.maximalIdeal (canonicalValuation A F).valuationSubring =
77       Ideal.span {e π} := by
78     rw [← IsLocalRing.map_ringEquiv_maximalIdeal e, ← hπ, Ideal.map_span]
79     simp
80   have h := Valuation.isUniformizer_of_maximalIdeal_eq_span (canonicalValuation A F) hgen
81   rw [Valuation.IsUniformizer.iff] at h ⊢
82   simpa [e, integerRingEquiv_coe] using h
83 
84 /-- Exact normalization of a maximal-ideal generator. -/
85 theorem uniformizer_value (π : A)
86     (hπ : Ideal.span {π} = IsLocalRing.maximalIdeal A) :
87     canonicalValuation A F (algebraMap A F π) =
88       (IsRankOneDiscrete.generator (canonicalValuation A F) : ℤᵐ⁰) :=
89   Valuation.IsUniformizer.iff.mp (uniformizer_isUniformizer A F π hπ)
90 
91 /-- A maximal-ideal generator has value strictly below one. -/
92 theorem uniformizer_value_lt_one (π : A)
93     (hπ : Ideal.span {π} = IsLocalRing.maximalIdeal A) :
94     canonicalValuation A F (algebraMap A F π) < 1 :=
95   (uniformizer_isUniformizer A F π hπ).val_lt_one
96 
97 end Generic
98 
99 section Constructed
100 
101 open PaperXI.LocalFieldResidueExtension PaperXI.ResidueExtensionRealization
102 
103 variable (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K]
104   [IsUniformAddGroup K] [IsNonarchimedeanLocalField K]
105 variable (s : Type*) [Field s] [Algebra 𝓀[K] s]
106   [FiniteDimensional 𝓀[K] s]
107 
108 abbrev upperRing := LocalFieldResidueExtension.ring K s
109 abbrev upperField := LocalFieldResidueExtension.field K s
110 abbrev upperValuation : Valuation (upperField K s) ℤᵐ⁰ :=
111   canonicalValuation (upperRing K s) (upperField K s)
112 
113 /-- The constructed upper DVR is the valuation ring of its canonical adic
114 valuation on the constructed fraction field. -/
115 def upperIntegerRingEquiv :
116     upperRing K s ≃+* (upperValuation K s).valuationSubring :=
117   integerRingEquiv (upperRing K s) (upperField K s)
118 
119 omit [IsUniformAddGroup K] in
120 @[simp]
121 theorem upperIntegerRingEquiv_coe (x : upperRing K s) :
122     (((upperIntegerRingEquiv K s x : (upperValuation K s).valuationSubring) :
123       upperField K s)) = algebraMap (upperRing K s) (upperField K s) x := by
124   rfl
125 
126 omit [IsUniformAddGroup K] in
127 /-- Literal ambient-field equality between the embedded constructed DVR and the
128 canonical valuation unit ball. -/
129 theorem upper_integerRing_image :
130     Subring.map (algebraMap (upperRing K s) (upperField K s)) ⊤ =
131       (upperValuation K s).valuationSubring.toSubring :=
132   integerRing_image (upperRing K s) (upperField K s)
133 
134 omit [IsUniformAddGroup K] in
135 /-- Concrete integrality criterion for the constructed fraction field. -/
136 theorem upper_integer_iff_exists_lift (x : upperField K s) :
137     upperValuation K s x ≤ 1 ↔
138       ∃ a : upperRing K s,
139         algebraMap (upperRing K s) (upperField K s) a = x :=
140   integer_iff_exists_lift (upperRing K s) (upperField K s) x
141 
142 omit [IsUniformAddGroup K] in
143 /-- Every unit of the constructed upper DVR has value one. -/
144 theorem upper_unit_value (u : upperRing K s) (hu : IsUnit u) :
145     upperValuation K s
146       (algebraMap (upperRing K s) (upperField K s) u) = 1 :=
147   unit_value (upperRing K s) (upperField K s) u hu
148 
149 omit [IsUniformAddGroup K] in
150 /-- Every unit of the original local-field integer ring retains value one after
151 mapping through the constructed upper DVR into its fraction field. -/
152 theorem base_unit_value (u : 𝒪[K]) (hu : IsUnit u) :
153     upperValuation K s
154       (algebraMap (upperRing K s) (upperField K s)
155         (algebraMap 𝒪[K] (upperRing K s) u)) = 1 := by
156   apply upper_unit_value K s
157   exact hu.map (algebraMap 𝒪[K] (upperRing K s))
158 
159 omit [IsUniformAddGroup K] in
160 /-- Any base uniformizer remains a generator of the upper maximal ideal. -/
161 theorem base_uniformizer_generates_upper (π : 𝒪[K])
162     (hπ : Ideal.span {π} = IsLocalRing.maximalIdeal 𝒪[K]) :
163     Ideal.span {algebraMap 𝒪[K] (upperRing K s) π} =
164       IsLocalRing.maximalIdeal (upperRing K s) := by
165   exact PaperXI.UnramifiedPolynomial.uniformizer
166     (ResidueExtensionRealization.liftedPolynomial 𝒪[K] s) π hπ
167 
168 omit [IsUniformAddGroup K] in
169 /-- A base uniformizer is a uniformizer for the canonical valuation of the
170 constructed upper fraction field. -/
171 theorem base_uniformizer_isUniformizer (π : 𝒪[K])
172     (hπ : Ideal.span {π} = IsLocalRing.maximalIdeal 𝒪[K]) :
173     (upperValuation K s).IsUniformizer
174       (algebraMap (upperRing K s) (upperField K s)
175         (algebraMap 𝒪[K] (upperRing K s) π)) := by
176   exact uniformizer_isUniformizer (upperRing K s) (upperField K s)
177     (algebraMap 𝒪[K] (upperRing K s) π)
178     (base_uniformizer_generates_upper K s π hπ)
179 
180 omit [IsUniformAddGroup K] in
181 /-- Exact canonical value of an inherited base uniformizer. -/
182 theorem base_uniformizer_value (π : 𝒪[K])
183     (hπ : Ideal.span {π} = IsLocalRing.maximalIdeal 𝒪[K]) :
184     upperValuation K s
185       (algebraMap (upperRing K s) (upperField K s)
186         (algebraMap 𝒪[K] (upperRing K s) π)) =
187       (IsRankOneDiscrete.generator (upperValuation K s) : ℤᵐ⁰) :=
188   Valuation.IsUniformizer.iff.mp (base_uniformizer_isUniformizer K s π hπ)
189 
190 /-- Choose one base uniformizer from the actual DVR of integers. -/
191 def chosenBaseUniformizer : 𝒪[K] :=
192   Classical.choose (IsDiscreteValuationRing.exists_irreducible 𝒪[K])
193 
194 omit [IsUniformAddGroup K] in
195 theorem chosenBaseUniformizer_irreducible :
196     Irreducible (chosenBaseUniformizer K) :=
197   Classical.choose_spec (IsDiscreteValuationRing.exists_irreducible 𝒪[K])
198 
199 omit [IsUniformAddGroup K] in
200 theorem chosenBaseUniformizer_span :
201     Ideal.span {chosenBaseUniformizer K} = IsLocalRing.maximalIdeal 𝒪[K] := by
202   exact (IsDiscreteValuationRing.irreducible_iff_uniformizer
203     (chosenBaseUniformizer K)).mp (chosenBaseUniformizer_irreducible K) |>.symm
204 
205 omit [IsUniformAddGroup K] in
206 /-- The chosen base uniformizer gives an actual canonical upper uniformizer. -/
207 theorem chosenBaseUniformizer_isUpperUniformizer :
208     (upperValuation K s).IsUniformizer
209       (algebraMap (upperRing K s) (upperField K s)
210         (algebraMap 𝒪[K] (upperRing K s) (chosenBaseUniformizer K))) :=
211   base_uniformizer_isUniformizer K s (chosenBaseUniformizer K)
212     (chosenBaseUniformizer_span K)
213 
214 omit [IsUniformAddGroup K] in
215 /-- Exact normalization for the chosen inherited upper uniformizer. -/
216 theorem chosenBaseUniformizer_value :
217     upperValuation K s
218       (algebraMap (upperRing K s) (upperField K s)
219         (algebraMap 𝒪[K] (upperRing K s) (chosenBaseUniformizer K))) =
220       (IsRankOneDiscrete.generator (upperValuation K s) : ℤᵐ⁰) :=
221   Valuation.IsUniformizer.iff.mp (chosenBaseUniformizer_isUpperUniformizer K s)
222 
223 end Constructed
224 
225 end PaperXI.CanonicalDVRValuation

Back to source controls