Skip to content

Commit 1692ef2

Browse files
xgenereuxxgenereux
committed
chore(FunctionField): move inftyValuation and FqtInfty to RatFunc namespace (#38030)
From [this discussion](#37894 (comment)). Move `RatFunc` results from `FunctionField` field to `RatFunc` folder and namespace. Note : I used Claude Code to produce the deprecations. Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>
1 parent d8630ef commit 1692ef2

File tree

4 files changed

+205
-107
lines changed

4 files changed

+205
-107
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4398,6 +4398,7 @@ public import Mathlib.FieldTheory.RatFunc.Defs
43984398
public import Mathlib.FieldTheory.RatFunc.Degree
43994399
public import Mathlib.FieldTheory.RatFunc.IntermediateField
44004400
public import Mathlib.FieldTheory.RatFunc.Luroth
4401+
public import Mathlib.FieldTheory.RatFunc.Valuation
44014402
public import Mathlib.FieldTheory.Relrank
44024403
public import Mathlib.FieldTheory.Separable
44034404
public import Mathlib.FieldTheory.SeparableClosure

‎Mathlib/FieldTheory/RatFunc/Valuation.lean‎

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
/-
2+
Copyright (c) 2021 Anne Baanen. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Anne Baanen, Ashvni Narayanan
5+
-/
6+
module
7+
8+
public import Mathlib.FieldTheory.RatFunc.Degree
9+
10+
/-!
11+
# Valuations on F(t)
12+
13+
This file defines the valuation at infinity on the field of rational functions `F(t)`.
14+
15+
## Main definitions
16+
17+
- `RatFunc.inftyValuation` : The place at infinity on `F(t)` is the nonarchimedean
18+
valuation on `F(t)` with uniformizer `1/t`.
19+
- `RatFunc.CompletionAtInfty` : The completion `F((t⁻¹))` of `F(t)` with respect to the
20+
valuation at infinity.
21+
22+
## References
23+
* [D. Marcus, *Number Fields*][marcus1977number]
24+
* [J.W.S. Cassels, A. Fröhlich, *Algebraic Number Theory*][cassels1967algebraic]
25+
* [P. Samuel, *Algebraic Theory of Numbers*][samuel1967]
26+
27+
## Tags
28+
function field, ring of integers
29+
-/
30+
31+
@[expose] public section
32+
33+
34+
public noncomputable section
35+
36+
namespace RatFunc
37+
38+
variable (F K : Type*) [Field F] [Field K]
39+
40+
/-! ### The place at infinity on F(t) -/
41+
42+
section InftyValuation
43+
44+
open Multiplicative WithZero Polynomial
45+
46+
variable [DecidableEq (RatFunc F)]
47+
48+
/-- The valuation at infinity is the nonarchimedean valuation on `F(t)` with uniformizer `1/t`.
49+
Explicitly, if `f/g ∈ F(t)` is a nonzero quotient of polynomials, its valuation at infinity is
50+
`exp (degree(f) - degree(g))`. -/
51+
def inftyValuationDef (r : RatFunc F) : ℤᵐ⁰ :=
52+
if r = 0 then 0 else exp r.intDegree
53+
54+
theorem InftyValuation.map_zero' : inftyValuationDef F 0 = 0 :=
55+
if_pos rfl
56+
57+
theorem InftyValuation.map_one' : inftyValuationDef F 1 = 1 :=
58+
(if_neg one_ne_zero).trans <| by simp
59+
60+
theorem InftyValuation.map_mul' (x y : RatFunc F) :
61+
inftyValuationDef F (x * y) = inftyValuationDef F x * inftyValuationDef F y := by
62+
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
63+
by_cases hx : x = 0
64+
· rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
65+
· by_cases hy : y = 0
66+
· rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
67+
· simp_all [RatFunc.intDegree_mul]
68+
69+
theorem InftyValuation.map_add_le_max' (x y : RatFunc F) :
70+
inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y) := by
71+
by_cases hx : x = 0
72+
· rw [hx, zero_add]
73+
conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]
74+
rw [max_eq_right (WithZero.zero_le (inftyValuationDef F y))]
75+
· by_cases hy : y = 0
76+
· rw [hy, add_zero]
77+
conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
78+
rw [max_eq_right (WithZero.zero_le (inftyValuationDef F x))]
79+
· by_cases hxy : x + y = 0
80+
· rw [inftyValuationDef, if_pos hxy]; exact zero_le'
81+
· rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy,
82+
if_neg hxy]
83+
simpa using RatFunc.intDegree_add_le hy hxy
84+
85+
@[simp]
86+
theorem inftyValuation_of_nonzero {x : RatFunc F} (hx : x ≠ 0) :
87+
inftyValuationDef F x = exp x.intDegree := by
88+
rw [inftyValuationDef, if_neg hx]
89+
90+
/-- The valuation at infinity on `F(t)`. -/
91+
def inftyValuation : Valuation (RatFunc F) ℤᵐ⁰ where
92+
toFun := inftyValuationDef F
93+
map_zero' := InftyValuation.map_zero' F
94+
map_one' := InftyValuation.map_one' F
95+
map_mul' := InftyValuation.map_mul' F
96+
map_add_le_max' := InftyValuation.map_add_le_max' F
97+
98+
theorem inftyValuation_apply {x : RatFunc F} : inftyValuation F x = inftyValuationDef F x :=
99+
rfl
100+
101+
@[simp]
102+
theorem inftyValuation.C {k : F} (hk : k ≠ 0) :
103+
inftyValuation F (RatFunc.C k) = 1 := by
104+
simp [inftyValuation_apply, hk]
105+
106+
@[simp]
107+
theorem inftyValuation.X : inftyValuation F RatFunc.X = exp 1 := by
108+
simp [inftyValuation_apply, inftyValuationDef, if_neg RatFunc.X_ne_zero, RatFunc.intDegree_X]
109+
110+
lemma inftyValuation.X_zpow (m : ℤ) : inftyValuation F (RatFunc.X ^ m) = exp m := by simp
111+
112+
theorem inftyValuation.X_inv : inftyValuation F (1 / RatFunc.X) = exp (-1) := by
113+
rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]
114+
115+
-- Dropped attribute `@[simp]` due to issue described here:
116+
-- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60synthInstance.2EmaxHeartbeats.60.20error.20but.20only.20in.20.60simpNF.60
117+
theorem inftyValuation.polynomial {p : F[X]} (hp : p ≠ 0) :
118+
inftyValuationDef F (algebraMap F[X] (RatFunc F) p) = exp (p.natDegree : ℤ) := by
119+
rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]
120+
121+
instance : Valuation.IsNontrivial (inftyValuation F) := ⟨RatFunc.X, by simp⟩
122+
123+
instance : Valuation.IsTrivialOn F (inftyValuation F) :=
124+
⟨fun _ hx ↦ by simp [inftyValuation.C _ hx]⟩
125+
126+
/-- The valued field `F(t)` with the valuation at infinity. -/
127+
@[implicit_reducible]
128+
def inftyValued : Valued (RatFunc F) ℤᵐ⁰ :=
129+
Valued.mk' <| inftyValuation F
130+
131+
theorem inftyValued.def {x : RatFunc F} :
132+
(inftyValued F).v x = inftyValuationDef F x :=
133+
rfl
134+
135+
namespace CompletionAtInfty
136+
137+
/- We temporarily disable the existing valued instance coming from the ideal `X` to avoid diamonds
138+
with the uniform space structure coming from the valuation at infinity. -/
139+
attribute [-instance] RatFunc.valuedRatFunc
140+
141+
/- Locally add the uniform space structure coming from the valuation at infinity. This instance
142+
is scoped in the `CompletionAtInfty` namescape in case it is needed in the future. -/
143+
/-- The uniform space structure on `RatFunc F` coming from the valuation at infinity. -/
144+
scoped instance : UniformSpace (RatFunc F) := (inftyValued F).toUniformSpace
145+
146+
/-- The completion `F((t⁻¹))` of `F(t)` with respect to the valuation at infinity. -/
147+
def _root_.RatFunc.CompletionAtInfty := UniformSpace.Completion (RatFunc F)
148+
deriving Field, Algebra (RatFunc F), Coe (RatFunc F), Inhabited
149+
150+
end CompletionAtInfty
151+
152+
/-- The valuation at infinity on `k(t)` extends to a valuation on `CompletionAtInfty`. -/
153+
instance : Valued (CompletionAtInfty F) ℤᵐ⁰ := (inftyValued F).valuedCompletion
154+
155+
theorem valuedCompletionAtInfty.def {x : CompletionAtInfty F} :
156+
Valued.v x = (inftyValued F).extensionValuation x := rfl
157+
158+
end InftyValuation
159+
160+
end RatFunc

‎Mathlib/NumberTheory/FunctionField.lean‎

Lines changed: 42 additions & 105 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ public import Mathlib.RingTheory.DedekindDomain.IntegralClosure
1010
public import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
1111
public import Mathlib.Topology.Algebra.Valued.ValuedField
1212
public import Mathlib.Topology.Algebra.InfiniteSum.Defs
13+
public import Mathlib.FieldTheory.RatFunc.Valuation -- for deprecation to `RatFunc.inftyValuation` and `RatFunc.CompletionAtInfty`
1314

1415
/-!
1516
# Function fields
@@ -22,10 +23,6 @@ This file defines a function field and the ring of integers corresponding to it.
2223
i.e. it is a finite extension of the field of rational functions in one variable over `F`.
2324
- `FunctionField.ringOfIntegers` defines the ring of integers corresponding to a function field
2425
as the integral closure of `F[X]` in the function field.
25-
- `FunctionField.inftyValuation` : The place at infinity on `F(t)` is the nonarchimedean
26-
valuation on `F(t)` with uniformizer `1/t`.
27-
- `FunctionField.FqtInfty` : The completion `F((t⁻¹))` of `F(t)` with respect to the
28-
valuation at infinity.
2926
3027
## Implementation notes
3128
The definitions that involve a field of fractions choose a canonical field of fractions,
@@ -138,125 +135,65 @@ instance [Algebra.IsSeparable (RatFunc F) K] : IsDedekindDomain (ringOfIntegers
138135

139136
end ringOfIntegers
140137

141-
/-! ### The place at infinity on F(t) -/
138+
section deprecated
142139

140+
@[deprecated RatFunc.inftyValuationDef (since := "2026-04-14")]
141+
alias inftyValuationDef := RatFunc.inftyValuationDef
143142

144-
section InftyValuation
145-
146-
open Multiplicative WithZero
147-
148-
variable [DecidableEq (RatFunc F)]
149-
150-
/-- The valuation at infinity is the nonarchimedean valuation on `F(t)` with uniformizer `1/t`.
151-
Explicitly, if `f/g ∈ F(t)` is a nonzero quotient of polynomials, its valuation at infinity is
152-
`exp (degree(f) - degree(g))`. -/
153-
def inftyValuationDef (r : RatFunc F) : ℤᵐ⁰ :=
154-
if r = 0 then 0 else exp r.intDegree
155-
156-
theorem InftyValuation.map_zero' : inftyValuationDef F 0 = 0 :=
157-
if_pos rfl
158-
159-
theorem InftyValuation.map_one' : inftyValuationDef F 1 = 1 :=
160-
(if_neg one_ne_zero).trans <| by simp
143+
@[deprecated RatFunc.InftyValuation.map_zero' (since := "2026-04-14")]
144+
alias InftyValuation.map_zero' := RatFunc.InftyValuation.map_zero'
161145

162-
theorem InftyValuation.map_mul' (x y : RatFunc F) :
163-
inftyValuationDef F (x * y) = inftyValuationDef F x * inftyValuationDef F y := by
164-
rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
165-
by_cases hx : x = 0
166-
· rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
167-
· by_cases hy : y = 0
168-
· rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
169-
· simp_all [RatFunc.intDegree_mul]
146+
@[deprecated RatFunc.InftyValuation.map_one' (since := "2026-04-14")]
147+
alias InftyValuation.map_one' := RatFunc.InftyValuation.map_one'
170148

171-
theorem InftyValuation.map_add_le_max' (x y : RatFunc F) :
172-
inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y) := by
173-
by_cases hx : x = 0
174-
· rw [hx, zero_add]
175-
conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]
176-
rw [max_eq_right (WithZero.zero_le (inftyValuationDef F y))]
177-
· by_cases hy : y = 0
178-
· rw [hy, add_zero]
179-
conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
180-
rw [max_eq_right (WithZero.zero_le (inftyValuationDef F x))]
181-
· by_cases hxy : x + y = 0
182-
· rw [inftyValuationDef, if_pos hxy]; exact zero_le'
183-
· rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy,
184-
if_neg hxy]
185-
simpa using RatFunc.intDegree_add_le hy hxy
149+
@[deprecated RatFunc.InftyValuation.map_mul' (since := "2026-04-14")]
150+
alias InftyValuation.map_mul' := RatFunc.InftyValuation.map_mul'
186151

187-
@[simp]
188-
theorem inftyValuation_of_nonzero {x : RatFunc F} (hx : x ≠ 0) :
189-
inftyValuationDef F x = exp x.intDegree := by
190-
rw [inftyValuationDef, if_neg hx]
152+
@[deprecated RatFunc.InftyValuation.map_add_le_max' (since := "2026-04-14")]
153+
alias InftyValuation.map_add_le_max' := RatFunc.InftyValuation.map_add_le_max'
191154

192-
/-- The valuation at infinity on `F(t)`. -/
193-
def inftyValuation : Valuation (RatFunc F) ℤᵐ⁰ where
194-
toFun := inftyValuationDef F
195-
map_zero' := InftyValuation.map_zero' F
196-
map_one' := InftyValuation.map_one' F
197-
map_mul' := InftyValuation.map_mul' F
198-
map_add_le_max' := InftyValuation.map_add_le_max' F
155+
@[deprecated RatFunc.inftyValuation_of_nonzero (since := "2026-04-14")]
156+
alias inftyValuation_of_nonzero := RatFunc.inftyValuation_of_nonzero
199157

200-
theorem inftyValuation_apply {x : RatFunc F} : inftyValuation F x = inftyValuationDef F x :=
201-
rfl
158+
@[deprecated RatFunc.inftyValuation (since := "2026-04-14")]
159+
alias inftyValuation := RatFunc.inftyValuation
202160

203-
@[simp]
204-
theorem inftyValuation.C {k : F} (hk : k ≠ 0) :
205-
inftyValuation F (RatFunc.C k) = 1 := by
206-
simp [inftyValuation_apply, hk]
161+
@[deprecated RatFunc.inftyValuation_apply (since := "2026-04-14")]
162+
alias inftyValuation_apply := RatFunc.inftyValuation_apply
207163

208-
@[simp]
209-
theorem inftyValuation.X : inftyValuation F RatFunc.X = exp 1 := by
210-
simp [inftyValuation_apply, inftyValuationDef, if_neg RatFunc.X_ne_zero, RatFunc.intDegree_X]
164+
@[deprecated RatFunc.inftyValuation.C (since := "2026-04-14")]
165+
alias inftyValuation.C := RatFunc.inftyValuation.C
211166

212-
lemma inftyValuation.X_zpow (m : ℤ) : inftyValuation F (RatFunc.X ^ m) = exp m := by simp
167+
@[deprecated RatFunc.inftyValuation.X (since := "2026-04-14")]
168+
alias inftyValuation.X := RatFunc.inftyValuation.X
213169

214-
theorem inftyValuation.X_inv : inftyValuation F (1 / RatFunc.X) = exp (-1) := by
215-
rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]
170+
@[deprecated RatFunc.inftyValuation.X_zpow (since := "2026-04-14")]
171+
alias inftyValuation.X_zpow := RatFunc.inftyValuation.X_zpow
216172

217-
-- Dropped attribute `@[simp]` due to issue described here:
218-
-- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60synthInstance.2EmaxHeartbeats.60.20error.20but.20only.20in.20.60simpNF.60
219-
theorem inftyValuation.polynomial {p : F[X]} (hp : p ≠ 0) :
220-
inftyValuationDef F (algebraMap F[X] (RatFunc F) p) = exp (p.natDegree : ℤ) := by
221-
rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]
173+
@[deprecated RatFunc.inftyValuation.X_inv (since := "2026-04-14")]
174+
alias inftyValuation.X_inv := RatFunc.inftyValuation.X_inv
222175

223-
instance : Valuation.IsNontrivial (inftyValuation F) := ⟨RatFunc.X, by simp⟩
176+
@[deprecated RatFunc.inftyValuation.polynomial (since := "2026-04-14")]
177+
alias inftyValuation.polynomial := RatFunc.inftyValuation.polynomial
224178

225-
instance : Valuation.IsTrivialOn F (inftyValuation F) :=
226-
⟨fun _ hx ↦ by simp [inftyValuation.C _ hx]⟩
179+
@[deprecated RatFunc.inftyValued (since := "2026-04-14")]
180+
alias inftyValuedFt := RatFunc.inftyValued
227181

228-
/-- The valued field `F(t)` with the valuation at infinity. -/
229-
@[implicit_reducible]
230-
def inftyValuedFqt : Valued (RatFunc F) ℤᵐ⁰ :=
231-
Valued.mk' <| inftyValuation F
182+
@[deprecated RatFunc.inftyValued.def (since := "2026-04-14")]
183+
alias inftyValuedFt.def := RatFunc.inftyValued.def
232184

233-
theorem inftyValuedFqt.def {x : RatFunc F} :
234-
(inftyValuedFqt F).v x = inftyValuationDef F x :=
235-
rfl
185+
@[deprecated RatFunc.CompletionAtInfty (since := "2026-04-14")]
186+
alias FtInfty := RatFunc.CompletionAtInfty
236187

237-
namespace FqtInfty
188+
@[deprecated "Use the anonymous `Valued` instance on `RatFunc.CompletionAtInfty`"
189+
(since := "2026-04-14")]
190+
instance valuedFtInfty [DecidableEq (RatFunc F)] :
191+
Valued (RatFunc.CompletionAtInfty F) ℤᵐ⁰ :=
192+
inferInstance
238193

239-
/- We temporarily disable the existing valued instance coming from the ideal `X` to avoid diamonds
240-
with the uniform space structure coming from the valuation at infinity. -/
241-
attribute [-instance] RatFunc.valuedRatFunc
194+
@[deprecated RatFunc.valuedCompletionAtInfty.def (since := "2026-04-14")]
195+
alias valuedFtInfty.def := RatFunc.valuedCompletionAtInfty.def
242196

243-
/- Locally add the uniform space structure coming from the valuation at infinity. This instance
244-
is scoped in the `FqtInfty` namescape in case it is needed in the future. -/
245-
/-- The uniform space structure on `RatFunc F` coming from the valuation at infinity. -/
246-
scoped instance : UniformSpace (RatFunc F) := (inftyValuedFqt F).toUniformSpace
247-
248-
/-- The completion `F((t⁻¹))` of `F(t)` with respect to the valuation at infinity. -/
249-
def _root_.FunctionField.FqtInfty := UniformSpace.Completion (RatFunc F)
250-
deriving Field, Algebra (RatFunc F), Coe (RatFunc F), Inhabited
251-
252-
end FqtInfty
253-
254-
/-- The valuation at infinity on `k(t)` extends to a valuation on `FqtInfty`. -/
255-
instance valuedFqtInfty : Valued (FqtInfty F) ℤᵐ⁰ := (inftyValuedFqt F).valuedCompletion
256-
257-
theorem valuedFqtInfty.def {x : FqtInfty F} :
258-
Valued.v x = (inftyValuedFqt F).extensionValuation x := rfl
259-
260-
end InftyValuation
197+
end deprecated
261198

262199
end FunctionField

‎Mathlib/NumberTheory/RatFunc/Ostrowski.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -257,7 +257,7 @@ lemma valuation_isEquiv_adic_of_valuation_X_le_one (hle : v X ≤ 1) :
257257
A discrete valuation of rank 1 that is trivial on `K` is equivalent either to the valuation
258258
at infinity or to the `p`-adic valuation for a unique maximal ideal `p` of `K[X]`. -/
259259
theorem valuation_isEquiv_infty_or_adic [DecidableEq (RatFunc K)] :
260-
Xor' (v.IsEquiv (FunctionField.inftyValuation K))
260+
Xor' (v.IsEquiv (RatFunc.inftyValuation K))
261261
(∃! (u : HeightOneSpectrum K[X]), v.IsEquiv (u.valuation _)) := by
262262
rcases lt_or_ge 1 (v X) with hlt | hge
263263
/- Infinity case -/
@@ -272,7 +272,7 @@ theorem valuation_isEquiv_infty_or_adic [DecidableEq (RatFunc K)] :
272272
fun hv ↦ absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)⟩
273273

274274
lemma valuation_isEquiv_adic_of_not_isEquiv_infty [DecidableEq (RatFunc K)]
275-
(hni : ¬ v.IsEquiv (FunctionField.inftyValuation K)) :
275+
(hni : ¬ v.IsEquiv (RatFunc.inftyValuation K)) :
276276
∃! (u : HeightOneSpectrum K[X]), v.IsEquiv (u.valuation _) :=
277277
valuation_isEquiv_infty_or_adic.or.resolve_left hni
278278

0 commit comments

Comments
 (0)
⚡