[Merged by Bors] - chore(FunctionField): move inftyValuation and FqtInfty to RatFunc namespace

Mathlib.lean

@@ -4398,6 +4398,7 @@ public import Mathlib.FieldTheory.RatFunc.Defs
 public import Mathlib.FieldTheory.RatFunc.Degree
 public import Mathlib.FieldTheory.RatFunc.IntermediateField
 public import Mathlib.FieldTheory.RatFunc.Luroth
+public import Mathlib.FieldTheory.RatFunc.Valuation
 public import Mathlib.FieldTheory.Relrank
 public import Mathlib.FieldTheory.Separable
 public import Mathlib.FieldTheory.SeparableClosure

Mathlib/FieldTheory/RatFunc/Valuation.lean

@@ -0,0 +1,160 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen, Ashvni Narayanan
+-/
+module
+
+public import Mathlib.FieldTheory.RatFunc.Degree
+
+/-!
+# Valuations on F(t)
+
+This file defines the valuation at infinity on the field of rational functions `F(t)`.
+
+## Main definitions
+
+- `RatFunc.inftyValuation` : The place at infinity on `F(t)` is the nonarchimedean
+  valuation on `F(t)` with uniformizer `1/t`.
+- `RatFunc.FtInfty` : The completion `F((t⁻¹))` of `F(t)` with respect to the
+  valuation at infinity.
+
+## References
+* [D. Marcus, *Number Fields*][marcus1977number]
+* [J.W.S. Cassels, A. Fröhlich, *Algebraic Number Theory*][cassels1967algebraic]
+* [P. Samuel, *Algebraic Theory of Numbers*][samuel1967]
+
+## Tags
+function field, ring of integers
+-/
+
+@[expose] public section
+
+
+public noncomputable section
+
+namespace RatFunc
+
+variable (F K : Type*) [Field F] [Field K]
+
+/-! ### The place at infinity on F(t) -/
+
+section InftyValuation
+
+open Multiplicative WithZero Polynomial
+
+variable [DecidableEq (RatFunc F)]
+
+/-- The valuation at infinity is the nonarchimedean valuation on `F(t)` with uniformizer `1/t`.
+Explicitly, if `f/g ∈ F(t)` is a nonzero quotient of polynomials, its valuation at infinity is
+`exp (degree(f) - degree(g))`. -/
+def inftyValuationDef (r : RatFunc F) : ℤᵐ⁰ :=
+  if r = 0 then 0 else exp r.intDegree
+
+theorem InftyValuation.map_zero' : inftyValuationDef F 0 = 0 :=
+  if_pos rfl
+
+theorem InftyValuation.map_one' : inftyValuationDef F 1 = 1 :=
+  (if_neg one_ne_zero).trans <| by simp
+
+theorem InftyValuation.map_mul' (x y : RatFunc F) :
+    inftyValuationDef F (x * y) = inftyValuationDef F x * inftyValuationDef F y := by
+  rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
+  by_cases hx : x = 0
+  · rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
+  · by_cases hy : y = 0
+    · rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
+    · simp_all [RatFunc.intDegree_mul]
+
+theorem InftyValuation.map_add_le_max' (x y : RatFunc F) :
+    inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y) := by
+  by_cases hx : x = 0
+  · rw [hx, zero_add]
+    conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]
+    rw [max_eq_right (WithZero.zero_le (inftyValuationDef F y))]
+  · by_cases hy : y = 0
+    · rw [hy, add_zero]
+      conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
+      rw [max_eq_right (WithZero.zero_le (inftyValuationDef F x))]
+    · by_cases hxy : x + y = 0
+      · rw [inftyValuationDef, if_pos hxy]; exact zero_le'
+      · rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy,
+          if_neg hxy]
+        simpa using RatFunc.intDegree_add_le hy hxy
+
+@[simp]
+theorem inftyValuation_of_nonzero {x : RatFunc F} (hx : x ≠ 0) :
+    inftyValuationDef F x = exp x.intDegree := by
+  rw [inftyValuationDef, if_neg hx]
+
+/-- The valuation at infinity on `F(t)`. -/
+def inftyValuation : Valuation (RatFunc F) ℤᵐ⁰ where
+  toFun := inftyValuationDef F
+  map_zero' := InftyValuation.map_zero' F
+  map_one' := InftyValuation.map_one' F
+  map_mul' := InftyValuation.map_mul' F
+  map_add_le_max' := InftyValuation.map_add_le_max' F
+
+theorem inftyValuation_apply {x : RatFunc F} : inftyValuation F x = inftyValuationDef F x :=
+  rfl
+
+@[simp]
+theorem inftyValuation.C {k : F} (hk : k ≠ 0) :
+    inftyValuation F (RatFunc.C k) = 1 := by
+  simp [inftyValuation_apply, hk]
+
+@[simp]
+theorem inftyValuation.X : inftyValuation F RatFunc.X = exp 1 := by
+  simp [inftyValuation_apply, inftyValuationDef, if_neg RatFunc.X_ne_zero, RatFunc.intDegree_X]
+
+lemma inftyValuation.X_zpow (m : ℤ) : inftyValuation F (RatFunc.X ^ m) = exp m := by simp
+
+theorem inftyValuation.X_inv : inftyValuation F (1 / RatFunc.X) = exp (-1) := by
+  rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]
+
+-- Dropped attribute `@[simp]` due to issue described here:
+-- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60synthInstance.2EmaxHeartbeats.60.20error.20but.20only.20in.20.60simpNF.60
+theorem inftyValuation.polynomial {p : F[X]} (hp : p ≠ 0) :
+    inftyValuationDef F (algebraMap F[X] (RatFunc F) p) = exp (p.natDegree : ℤ) := by
+  rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]
+
+instance : Valuation.IsNontrivial (inftyValuation F) := ⟨RatFunc.X, by simp⟩
+
+instance : Valuation.IsTrivialOn F (inftyValuation F) :=
+  ⟨fun _ hx ↦ by simp [inftyValuation.C _ hx]⟩
+
+/-- The valued field `F(t)` with the valuation at infinity. -/
+@[implicit_reducible]
+def inftyValuedFt : Valued (RatFunc F) ℤᵐ⁰ :=
+  Valued.mk' <| inftyValuation F
+
+theorem inftyValuedFt.def {x : RatFunc F} :
+    (inftyValuedFt F).v x = inftyValuationDef F x :=
+  rfl
+
+namespace FtInfty
+
+/- We temporarily disable the existing valued instance coming from the ideal `X` to avoid diamonds
+with the uniform space structure coming from the valuation at infinity. -/
+attribute [-instance] RatFunc.valuedRatFunc
+
+/- Locally add the uniform space structure coming from the valuation at infinity. This instance
+is scoped in the `FtInfty` namescape in case it is needed in the future. -/
+/-- The uniform space structure on `RatFunc F` coming from the valuation at infinity. -/
+scoped instance : UniformSpace (RatFunc F) := (inftyValuedFt F).toUniformSpace
+
+/-- The completion `F((t⁻¹))` of `F(t)` with respect to the valuation at infinity. -/
+def _root_.RatFunc.FtInfty := UniformSpace.Completion (RatFunc F)
+deriving Field, Algebra (RatFunc F), Coe (RatFunc F), Inhabited
+
+end FtInfty
+
+/-- The valuation at infinity on `k(t)` extends to a valuation on `FtInfty`. -/
+instance valuedFtInfty : Valued (FtInfty F) ℤᵐ⁰ := (inftyValuedFt F).valuedCompletion
+
+theorem valuedFtInfty.def {x : FtInfty F} :
+  Valued.v x = (inftyValuedFt F).extensionValuation x := rfl
+
+end InftyValuation
+
+end RatFunc

Mathlib/NumberTheory/FunctionField.lean

@@ -10,6 +10,7 @@ public import Mathlib.RingTheory.DedekindDomain.IntegralClosure
 public import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
 public import Mathlib.Topology.Algebra.Valued.ValuedField
 public import Mathlib.Topology.Algebra.InfiniteSum.Defs
+public import Mathlib.FieldTheory.RatFunc.Valuation -- for deprecation to `RatFunc.inftyValuation` and `RatFunc.FtInfty`
 
 /-!
 # Function fields
@@ -22,10 +23,6 @@ This file defines a function field and the ring of integers corresponding to it.
   i.e. it is a finite extension of the field of rational functions in one variable over `F`.
 - `FunctionField.ringOfIntegers` defines the ring of integers corresponding to a function field
   as the integral closure of `F[X]` in the function field.
-- `FunctionField.inftyValuation` : The place at infinity on `F(t)` is the nonarchimedean
-  valuation on `F(t)` with uniformizer `1/t`.
-- `FunctionField.FqtInfty` : The completion `F((t⁻¹))` of `F(t)` with respect to the
-  valuation at infinity.
 
 ## Implementation notes
 The definitions that involve a field of fractions choose a canonical field of fractions,
@@ -138,125 +135,62 @@ instance [Algebra.IsSeparable (RatFunc F) K] : IsDedekindDomain (ringOfIntegers
 
 end ringOfIntegers
 
-/-! ### The place at infinity on F(t) -/
+section deprecated
 
+@[deprecated RatFunc.inftyValuationDef (since := "2026-04-14")]
+alias inftyValuationDef := RatFunc.inftyValuationDef
 
-section InftyValuation
-
-open Multiplicative WithZero
-
-variable [DecidableEq (RatFunc F)]
-
-/-- The valuation at infinity is the nonarchimedean valuation on `F(t)` with uniformizer `1/t`.
-Explicitly, if `f/g ∈ F(t)` is a nonzero quotient of polynomials, its valuation at infinity is
-`exp (degree(f) - degree(g))`. -/
-def inftyValuationDef (r : RatFunc F) : ℤᵐ⁰ :=
-  if r = 0 then 0 else exp r.intDegree
-
-theorem InftyValuation.map_zero' : inftyValuationDef F 0 = 0 :=
-  if_pos rfl
-
-theorem InftyValuation.map_one' : inftyValuationDef F 1 = 1 :=
-  (if_neg one_ne_zero).trans <| by simp
+@[deprecated RatFunc.InftyValuation.map_zero' (since := "2026-04-14")]
+alias InftyValuation.map_zero' := RatFunc.InftyValuation.map_zero'
 
-theorem InftyValuation.map_mul' (x y : RatFunc F) :
-    inftyValuationDef F (x * y) = inftyValuationDef F x * inftyValuationDef F y := by
-  rw [inftyValuationDef, inftyValuationDef, inftyValuationDef]
-  by_cases hx : x = 0
-  · rw [hx, zero_mul, if_pos (Eq.refl _), zero_mul]
-  · by_cases hy : y = 0
-    · rw [hy, mul_zero, if_pos (Eq.refl _), mul_zero]
-    · simp_all [RatFunc.intDegree_mul]
+@[deprecated RatFunc.InftyValuation.map_one' (since := "2026-04-14")]
+alias InftyValuation.map_one' := RatFunc.InftyValuation.map_one'
 
-theorem InftyValuation.map_add_le_max' (x y : RatFunc F) :
-    inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y) := by
-  by_cases hx : x = 0
-  · rw [hx, zero_add]
-    conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]
-    rw [max_eq_right (WithZero.zero_le (inftyValuationDef F y))]
-  · by_cases hy : y = 0
-    · rw [hy, add_zero]
-      conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
-      rw [max_eq_right (WithZero.zero_le (inftyValuationDef F x))]
-    · by_cases hxy : x + y = 0
-      · rw [inftyValuationDef, if_pos hxy]; exact zero_le'
-      · rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy,
-          if_neg hxy]
-        simpa using RatFunc.intDegree_add_le hy hxy
+@[deprecated RatFunc.InftyValuation.map_mul' (since := "2026-04-14")]
+alias InftyValuation.map_mul' := RatFunc.InftyValuation.map_mul'
 
-@[simp]
-theorem inftyValuation_of_nonzero {x : RatFunc F} (hx : x ≠ 0) :
-    inftyValuationDef F x = exp x.intDegree := by
-  rw [inftyValuationDef, if_neg hx]
+@[deprecated RatFunc.InftyValuation.map_add_le_max' (since := "2026-04-14")]
+alias InftyValuation.map_add_le_max' := RatFunc.InftyValuation.map_add_le_max'
 
-/-- The valuation at infinity on `F(t)`. -/
-def inftyValuation : Valuation (RatFunc F) ℤᵐ⁰ where
-  toFun := inftyValuationDef F
-  map_zero' := InftyValuation.map_zero' F
-  map_one' := InftyValuation.map_one' F
-  map_mul' := InftyValuation.map_mul' F
-  map_add_le_max' := InftyValuation.map_add_le_max' F
+@[deprecated RatFunc.inftyValuation_of_nonzero (since := "2026-04-14")]
+alias inftyValuation_of_nonzero := RatFunc.inftyValuation_of_nonzero
 
-theorem inftyValuation_apply {x : RatFunc F} : inftyValuation F x = inftyValuationDef F x :=
-  rfl
+@[deprecated RatFunc.inftyValuation (since := "2026-04-14")]
+alias inftyValuation := RatFunc.inftyValuation
 
-@[simp]
-theorem inftyValuation.C {k : F} (hk : k ≠ 0) :
-    inftyValuation F (RatFunc.C k) = 1 := by
-  simp [inftyValuation_apply, hk]
+@[deprecated RatFunc.inftyValuation_apply (since := "2026-04-14")]
+alias inftyValuation_apply := RatFunc.inftyValuation_apply
 
-@[simp]
-theorem inftyValuation.X : inftyValuation F RatFunc.X = exp 1 := by
-  simp [inftyValuation_apply, inftyValuationDef, if_neg RatFunc.X_ne_zero, RatFunc.intDegree_X]
+@[deprecated RatFunc.inftyValuation.C (since := "2026-04-14")]
+alias inftyValuation.C := RatFunc.inftyValuation.C
 
-lemma inftyValuation.X_zpow (m : ℤ) : inftyValuation F (RatFunc.X ^ m) = exp m := by simp
+@[deprecated RatFunc.inftyValuation.X (since := "2026-04-14")]
+alias inftyValuation.X := RatFunc.inftyValuation.X
 
-theorem inftyValuation.X_inv : inftyValuation F (1 / RatFunc.X) = exp (-1) := by
-  rw [one_div, ← zpow_neg_one, inftyValuation.X_zpow]
+@[deprecated RatFunc.inftyValuation.X_zpow (since := "2026-04-14")]
+alias inftyValuation.X_zpow := RatFunc.inftyValuation.X_zpow
 
--- Dropped attribute `@[simp]` due to issue described here:
--- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60synthInstance.2EmaxHeartbeats.60.20error.20but.20only.20in.20.60simpNF.60
-theorem inftyValuation.polynomial {p : F[X]} (hp : p ≠ 0) :
-    inftyValuationDef F (algebraMap F[X] (RatFunc F) p) = exp (p.natDegree : ℤ) := by
-  rw [inftyValuationDef, if_neg (by simpa), RatFunc.intDegree_polynomial]
+@[deprecated RatFunc.inftyValuation.X_inv (since := "2026-04-14")]
+alias inftyValuation.X_inv := RatFunc.inftyValuation.X_inv
 
-instance : Valuation.IsNontrivial (inftyValuation F) := ⟨RatFunc.X, by simp⟩
+@[deprecated RatFunc.inftyValuation.polynomial (since := "2026-04-14")]
+alias inftyValuation.polynomial := RatFunc.inftyValuation.polynomial
 
-instance : Valuation.IsTrivialOn F (inftyValuation F) :=
-  ⟨fun _ hx ↦ by simp [inftyValuation.C _ hx]⟩
+@[deprecated RatFunc.inftyValuedFt (since := "2026-04-14")]
+alias inftyValuedFt := RatFunc.inftyValuedFt
 
-/-- The valued field `F(t)` with the valuation at infinity. -/
-@[implicit_reducible]
-def inftyValuedFqt : Valued (RatFunc F) ℤᵐ⁰ :=
-  Valued.mk' <| inftyValuation F
+@[deprecated RatFunc.inftyValuedFt.def (since := "2026-04-14")]
+alias inftyValuedFt.def := RatFunc.inftyValuedFt.def
 
-theorem inftyValuedFqt.def {x : RatFunc F} :
-    (inftyValuedFqt F).v x = inftyValuationDef F x :=
-  rfl
+@[deprecated RatFunc.FtInfty (since := "2026-04-14")]
+alias FtInfty := RatFunc.FtInfty
 
-namespace FqtInfty
+@[deprecated RatFunc.valuedFtInfty (since := "2026-04-14")]
+alias valuedFtInfty := RatFunc.valuedFtInfty
 
-/- We temporarily disable the existing valued instance coming from the ideal `X` to avoid diamonds
-with the uniform space structure coming from the valuation at infinity. -/
-attribute [-instance] RatFunc.valuedRatFunc
+@[deprecated RatFunc.valuedFtInfty.def (since := "2026-04-14")]
+alias valuedFtInfty.def := RatFunc.valuedFtInfty.def
 
-/- Locally add the uniform space structure coming from the valuation at infinity. This instance
-is scoped in the `FqtInfty` namescape in case it is needed in the future. -/
-/-- The uniform space structure on `RatFunc F` coming from the valuation at infinity. -/
-scoped instance : UniformSpace (RatFunc F) := (inftyValuedFqt F).toUniformSpace
-
-/-- The completion `F((t⁻¹))` of `F(t)` with respect to the valuation at infinity. -/
-def _root_.FunctionField.FqtInfty := UniformSpace.Completion (RatFunc F)
-deriving Field, Algebra (RatFunc F), Coe (RatFunc F), Inhabited
-
-end FqtInfty
-
-/-- The valuation at infinity on `k(t)` extends to a valuation on `FqtInfty`. -/
-instance valuedFqtInfty : Valued (FqtInfty F) ℤᵐ⁰ := (inftyValuedFqt F).valuedCompletion
-
-theorem valuedFqtInfty.def {x : FqtInfty F} :
-  Valued.v x = (inftyValuedFqt F).extensionValuation x := rfl
-
-end InftyValuation
+end deprecated
 
 end FunctionField

Mathlib/NumberTheory/RatFunc/Ostrowski.lean

@@ -257,7 +257,7 @@ lemma valuation_isEquiv_adic_of_valuation_X_le_one (hle : v X ≤ 1) :
 A discrete valuation of rank 1 that is trivial on `K` is equivalent either to the valuation
 at infinity or to the `p`-adic valuation for a unique maximal ideal `p` of `K[X]`. -/
 theorem valuation_isEquiv_infty_or_adic [DecidableEq (RatFunc K)] :
-    Xor' (v.IsEquiv (FunctionField.inftyValuation K))
+    Xor' (v.IsEquiv (RatFunc.inftyValuation K))
       (∃! (u : HeightOneSpectrum K[X]), v.IsEquiv (u.valuation _)) := by
   rcases lt_or_ge 1 (v X) with hlt | hge
   /- Infinity case -/
@@ -272,7 +272,7 @@ theorem valuation_isEquiv_infty_or_adic [DecidableEq (RatFunc K)] :
       fun hv ↦ absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)⟩
 
 lemma valuation_isEquiv_adic_of_not_isEquiv_infty [DecidableEq (RatFunc K)]
-    (hni : ¬ v.IsEquiv (FunctionField.inftyValuation K)) :
+    (hni : ¬ v.IsEquiv (RatFunc.inftyValuation K)) :
     ∃! (u : HeightOneSpectrum K[X]), v.IsEquiv (u.valuation _) :=
   valuation_isEquiv_infty_or_adic.or.resolve_left hni