[Merged by Bors] - chore: make arg in HeightOneSpectrum.valuation explicit

Mathlib/FieldTheory/RatFunc/AsPolynomial.lean

@@ -197,13 +197,13 @@ theorem idealX_span : (idealX K).asIdeal = Ideal.span {X} := rfl
 
 @[simp]
 theorem valuation_X_eq_neg_one :
-    (idealX K).valuation (RatFunc.X : RatFunc K) = Multiplicative.ofAdd (-1 : ℤ) := by
+    (idealX K).valuation (RatFunc K) RatFunc.X = Multiplicative.ofAdd (-1 : ℤ) := by
   rw [← RatFunc.algebraMap_X, valuation_of_algebraMap, intValuation_singleton]
   · exact Polynomial.X_ne_zero
   · exact idealX_span K
 
 theorem valuation_of_mk (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0) :
-    (Polynomial.idealX K).valuation (RatFunc.mk f g) =
+    (Polynomial.idealX K).valuation _ (RatFunc.mk f g) =
       (Polynomial.idealX K).intValuation f / (Polynomial.idealX K).intValuation g := by
   simp only [RatFunc.mk_eq_mk' _ hg, valuation_of_mk']
 
@@ -215,11 +215,11 @@ open scoped Multiplicative
 
 open Polynomial
 
-instance : Valued (RatFunc K) ℤₘ₀ := Valued.mk' (idealX K).valuation
+instance : Valued (RatFunc K) ℤₘ₀ := Valued.mk' ((idealX K).valuation _)
 
 @[simp]
 theorem WithZero.valued_def {x : RatFunc K} :
-    @Valued.v (RatFunc K) _ _ _ _ x = (idealX K).valuation x := rfl
+    @Valued.v (RatFunc K) _ _ _ _ x = (idealX K).valuation _ x := rfl
 
 end RatFunc
 

Mathlib/NumberTheory/NumberField/FinitePlaces.lean

@@ -54,19 +54,20 @@ lemma norm_ne_zero : (absNorm v.asIdeal : NNReal) ≠ 0 :=
 /-- The `v`-adic absolute value on `K` defined as the norm of `v` raised to negative `v`-adic
 valuation -/
 noncomputable def vadicAbv : AbsoluteValue K ℝ where
-  toFun x := toNNReal (norm_ne_zero v) (v.valuation x)
+  toFun x := toNNReal (norm_ne_zero v) (v.valuation K x)
   map_mul' _ _ := by simp only [_root_.map_mul, NNReal.coe_mul]
   nonneg' _ := NNReal.zero_le_coe
   eq_zero' _ := by simp only [NNReal.coe_eq_zero, map_eq_zero]
   add_le' x y := by
     -- the triangle inequality is implied by the ultrametric one
-    apply le_trans _ <| max_le_add_of_nonneg (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation x)))
-      (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation y)))
+    apply le_trans _ <| max_le_add_of_nonneg
+      (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation _ x)))
+      (zero_le ((toNNReal (norm_ne_zero v)) (v.valuation K y)))
     have h_mono := (toNNReal_strictMono (one_lt_norm_nnreal v)).monotone
     rw [← h_mono.map_max] --max goes inside withZeroMultIntToNNReal
-    exact h_mono (v.valuation.map_add x y)
+    exact h_mono ((v.valuation _).map_add x y)
 
-theorem vadicAbv_def {x : K} : vadicAbv v x = toNNReal (norm_ne_zero v) (v.valuation x) := rfl
+theorem vadicAbv_def {x : K} : vadicAbv v x = toNNReal (norm_ne_zero v) (v.valuation K x) := rfl
 
 end absoluteValue
 
@@ -125,7 +126,7 @@ theorem FinitePlace.norm_def (x : K) : ‖embedding v x‖ = vadicAbv v x := by
 /-- The norm of the image after the embedding associated to `v` is equal to the norm of `v` raised
 to the power of the `v`-adic valuation. -/
 theorem FinitePlace.norm_def' (x : K) : ‖embedding v x‖ = toNNReal (norm_ne_zero v)
-    (v.valuation x) := by
+    (v.valuation K x) := by
   rw [norm_def, vadicAbv_def]
 
 /-- The norm of the image after the embedding associated to `v` is equal to the norm of `v` raised
@@ -279,7 +280,7 @@ lemma embedding_mul_absNorm (v : HeightOneSpectrum (𝓞 K)) {x : 𝓞 K} (h_x_n
     ‖(embedding v) x‖ * absNorm (v.maxPowDividing (span {x})) = 1 := by
   rw [maxPowDividing, map_pow, Nat.cast_pow, norm_def, vadicAbv_def,
     WithZeroMulInt.toNNReal_neg_apply _
-      (v.valuation.ne_zero_iff.mpr (RingOfIntegers.coe_ne_zero_iff.mpr h_x_nezero))]
+      ((v.valuation K).ne_zero_iff.mpr (RingOfIntegers.coe_ne_zero_iff.mpr h_x_nezero))]
   push_cast
   rw [← zpow_natCast, ← zpow_add₀ <| mod_cast (zero_lt_one.trans (one_lt_norm_nnreal v)).ne']
   norm_cast

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

@@ -78,7 +78,6 @@ def intValuationDef (r : R) : ℤₘ₀ :=
     ↑(Multiplicative.ofAdd
       (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r} : Ideal R)).factors : ℤ))
 
-
 theorem intValuationDef_if_pos {r : R} (hr : r = 0) : v.intValuationDef r = 0 :=
   if_pos hr
 
@@ -222,7 +221,6 @@ def intValuation : Valuation R ℤₘ₀ where
   map_mul' := intValuation.map_mul' v
   map_add_le_max' := intValuation.map_add_le_max' v
 
-
 theorem intValuation_apply {r : R} (v : IsDedekindDomain.HeightOneSpectrum R) :
     intValuation v r = intValuationDef v r := rfl
 
@@ -261,49 +259,53 @@ theorem intValuation_singleton {r : R} (hr : r ≠ 0) (hv : v.asIdeal = Ideal.sp
 
 /-! ### Adic valuations on the field of fractions `K` -/
 
-
+variable (K) in
 /-- The `v`-adic valuation of `x ∈ K` is the valuation of `r` divided by the valuation of `s`,
 where `r` and `s` are chosen so that `x = r/s`. -/
 def valuation (v : HeightOneSpectrum R) : Valuation K ℤₘ₀ :=
   v.intValuation.extendToLocalization
     (fun r hr => Set.mem_compl <| v.intValuation_ne_zero' ⟨r, hr⟩) K
 
 theorem valuation_def (x : K) :
-    v.valuation x =
+    v.valuation K x =
       v.intValuation.extendToLocalization
         (fun r hr => Set.mem_compl (v.intValuation_ne_zero' ⟨r, hr⟩)) K x :=
   rfl
 
 /-- The `v`-adic valuation of `r/s ∈ K` is the valuation of `r` divided by the valuation of `s`. -/
 theorem valuation_of_mk' {r : R} {s : nonZeroDivisors R} :
-    v.valuation (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation s := by
+    v.valuation K (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation s := by
   erw [valuation_def, (IsLocalization.toLocalizationMap (nonZeroDivisors R) K).lift_mk',
     div_eq_mul_inv, mul_eq_mul_left_iff]
   left
   rw [Units.val_inv_eq_inv_val, inv_inj]
   rfl
 
+open scoped algebraMap in
 /-- The `v`-adic valuation on `K` extends the `v`-adic valuation on `R`. -/
-theorem valuation_of_algebraMap (r : R) : v.valuation (algebraMap R K r) = v.intValuation r := by
+theorem valuation_of_algebraMap (r : R) : v.valuation K r = v.intValuation r := by
   rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]
 
 open scoped algebraMap in
-lemma valuation_eq_intValuationDef (r : R) : v.valuation (r : K) = v.intValuationDef r :=
+lemma valuation_eq_intValuationDef (r : R) : v.valuation K r = v.intValuationDef r :=
   Valuation.extendToLocalization_apply_map_apply ..
 
+open scoped algebraMap in
 /-- The `v`-adic valuation on `R` is bounded above by 1. -/
-theorem valuation_le_one (r : R) : v.valuation (algebraMap R K r) ≤ 1 := by
+theorem valuation_le_one (r : R) : v.valuation K r ≤ 1 := by
   rw [valuation_of_algebraMap]; exact v.intValuation_le_one r
 
+open scoped algebraMap in
 /-- The `v`-adic valuation of `r ∈ R` is less than 1 if and only if `v` divides the ideal `(r)`. -/
 theorem valuation_lt_one_iff_dvd (r : R) :
-    v.valuation (algebraMap R K r) < 1 ↔ v.asIdeal ∣ Ideal.span {r} := by
+    v.valuation K r < 1 ↔ v.asIdeal ∣ Ideal.span {r} := by
   rw [valuation_of_algebraMap]; exact v.intValuation_lt_one_iff_dvd r
 
 variable (K)
 
 /-- There exists `π ∈ K` with `v`-adic valuation `Multiplicative.ofAdd (-1)`. -/
-theorem valuation_exists_uniformizer : ∃ π : K, v.valuation π = Multiplicative.ofAdd (-1 : ℤ) := by
+theorem valuation_exists_uniformizer : ∃ π : K,
+    v.valuation K π = Multiplicative.ofAdd (-1 : ℤ) := by
   obtain ⟨r, hr⟩ := v.intValuation_exists_uniformizer
   use algebraMap R K r
   rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]
@@ -315,7 +317,7 @@ theorem valuation_uniformizer_ne_zero : Classical.choose (v.valuation_exists_uni
   (Valuation.ne_zero_iff _).mp (ne_of_eq_of_ne hu WithZero.coe_ne_zero)
 
 theorem mem_integers_of_valuation_le_one (x : K)
-    (h : ∀ v : HeightOneSpectrum R, v.valuation x ≤ 1) : x ∈ (algebraMap R K).range := by
+    (h : ∀ v : HeightOneSpectrum R, v.valuation K x ≤ 1) : x ∈ (algebraMap R K).range := by
   obtain ⟨⟨n, d, hd⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors R) x
   obtain rfl : x = IsLocalization.mk' K n ⟨d, hd⟩ := IsLocalization.eq_mk'_iff_mul_eq.mpr hx
   obtain rfl | hn0 := eq_or_ne n 0
@@ -352,9 +354,9 @@ variable {K}
 
 /-- `K` as a valued field with the `v`-adic valuation. -/
 def adicValued : Valued K ℤₘ₀ :=
-  Valued.mk' v.valuation
+  Valued.mk' (v.valuation K)
 
-theorem adicValued_apply {x : K} : v.adicValued.v x = v.valuation x :=
+theorem adicValued_apply {x : K} : v.adicValued.v x = v.valuation K x :=
   rfl
 
 variable (K)
@@ -501,13 +503,13 @@ open scoped algebraMap in -- to make the coercions from `R` fire
 /-- The valuation on the completion agrees with the global valuation on elements of the
 integer ring. -/
 theorem valuedAdicCompletion_eq_valuation (r : R) :
-    Valued.v (r : v.adicCompletion K) = v.valuation (r : K) := by
+    Valued.v (r : v.adicCompletion K) = v.valuation K r := by
   convert Valued.valuedCompletion_apply (r : K)
 
 variable {R K} in
 /-- The valuation on the completion agrees with the global valuation on elements of the field. -/
 theorem valuedAdicCompletion_eq_valuation' (k : K) :
-    Valued.v (k : v.adicCompletion K) = v.valuation k := by
+    Valued.v (k : v.adicCompletion K) = v.valuation K k := by
   convert Valued.valuedCompletion_apply k
 
 variable {R K} in

Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

@@ -269,20 +269,21 @@ theorem one : (1 : K_hat R K).IsFiniteAdele := by
 
 open scoped Multiplicative
 
-theorem algebraMap' (k : K) : (_root_.algebraMap K (K_hat R K) k).IsFiniteAdele := by
+open scoped algebraMap in
+theorem algebraMap' (k : K) : (algebraMap K (K_hat R K) k).IsFiniteAdele := by
   rw [IsFiniteAdele, Filter.eventually_cofinite]
   simp_rw [mem_adicCompletionIntegers, ProdAdicCompletions.algebraMap_apply',
     adicCompletion, Valued.valuedCompletion_apply, not_le]
-  change {v : HeightOneSpectrum R | 1 < v.valuation k}.Finite
+  change {v : HeightOneSpectrum R | 1 < v.valuation K k}.Finite
   -- The goal currently: if k ∈ K = field of fractions of a Dedekind domain R,
   -- then v(k)>1 for only finitely many v.
   -- We now write k=n/d and go via R to solve this goal. Do we need to do this?
   obtain ⟨⟨n, ⟨d, hd⟩⟩, hk⟩ := IsLocalization.surj (nonZeroDivisors R) k
   have hd' : d ≠ 0 := nonZeroDivisors.ne_zero hd
-  suffices {v : HeightOneSpectrum R | v.valuation (_root_.algebraMap R K d : K) < 1}.Finite by
+  suffices {v : HeightOneSpectrum R | v.valuation K d < 1}.Finite by
     apply Finite.subset this
     intro v hv
-    apply_fun v.valuation at hk
+    apply_fun v.valuation K at hk
     simp only [Valuation.map_mul, valuation_of_algebraMap] at hk
     rw [mem_setOf_eq, valuation_of_algebraMap]
     have := intValuation_le_one v n

Mathlib/RingTheory/DedekindDomain/SInteger.lean

@@ -61,18 +61,18 @@ variable {R : Type u} [CommRing R] [IsDedekindDomain R]
 @[simps!]
 def integer : Subalgebra R K :=
   {
-    (⨅ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuation.valuationSubring.toSubring).copy
-        {x : K | ∀ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuation x ≤ 1} <|
+    (⨅ (v) (_ : v ∉ S), (v.valuation K).valuationSubring.toSubring).copy
+        {x : K | ∀ (v) (_ : v ∉ S), v.valuation K x ≤ 1} <|
       Set.ext fun _ => by simp [SetLike.mem_coe, Subring.mem_iInf] with
     algebraMap_mem' := fun x v _ => v.valuation_le_one x }
 
 theorem integer_eq :
     (S.integer K).toSubring =
-      ⨅ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuation.valuationSubring.toSubring :=
+      ⨅ (v) (_ : v ∉ S), (v.valuation K).valuationSubring.toSubring :=
   SetLike.ext' <| by ext; simp
 
 theorem integer_valuation_le_one (x : S.integer K) {v : HeightOneSpectrum R} (hv : v ∉ S) :
-    v.valuation (x : K) ≤ 1 :=
+    v.valuation K x ≤ 1 :=
   x.property v hv
 
 /-! ## `S`-units -/
@@ -81,19 +81,19 @@ theorem integer_valuation_le_one (x : S.integer K) {v : HeightOneSpectrum R} (hv
 /-- The subgroup of `S`-units of `Kˣ`. -/
 @[simps!]
 def unit : Subgroup Kˣ :=
-  (⨅ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuation.valuationSubring.unitGroup).copy
-      {x : Kˣ | ∀ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuation (x : K) = 1} <|
+  (⨅ (v) (_ : v ∉ S), (v.valuation K).valuationSubring.unitGroup).copy
+      {x : Kˣ | ∀ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuation K x = 1} <|
     Set.ext fun _ => by
       -- Porting note: was
       -- simpa only [SetLike.mem_coe, Subgroup.mem_iInf, Valuation.mem_unitGroup_iff]
       simp only [mem_setOf, SetLike.mem_coe, Subgroup.mem_iInf, Valuation.mem_unitGroup_iff]
 
 theorem unit_eq :
-    S.unit K = ⨅ (v) (_ : v ∉ S), (v : HeightOneSpectrum R).valuation.valuationSubring.unitGroup :=
+    S.unit K = ⨅ (v) (_ : v ∉ S), (v.valuation K).valuationSubring.unitGroup :=
   Subgroup.copy_eq _ _ _
 
 theorem unit_valuation_eq_one (x : S.unit K) {v : HeightOneSpectrum R} (hv : v ∉ S) :
-    v.valuation ((x : Kˣ) : K) = 1 :=
+    v.valuation K (x : Kˣ) = 1 :=
   x.property v hv
 
 /-- The group of `S`-units is the group of units of the ring of `S`-integers. -/
@@ -110,7 +110,7 @@ def unitEquivUnitsInteger : S.unit K ≃* (S.integer K)ˣ where
         Eq.ge <| by
           -- Porting note: was
           -- rw [← map_mul]; convert v.valuation.map_one; exact subtype.mk_eq_mk.mp x.val_inv⟩
-          rw [Units.val_mk0, ← map_mul, Subtype.mk_eq_mk.mp x.val_inv, v.valuation.map_one]⟩
+          rw [Units.val_mk0, ← map_mul, Subtype.mk_eq_mk.mp x.val_inv, map_one]⟩
   left_inv _ := by ext; rfl
   right_inv _ := by ext; rfl
   map_mul' _ _ := by ext; rfl

Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean

@@ -90,9 +90,9 @@ def valuationOfNeZeroToFun (x : Kˣ) : Multiplicative ℤ :=
 
 @[simp]
 theorem valuationOfNeZeroToFun_eq (x : Kˣ) :
-    (v.valuationOfNeZeroToFun x : ℤₘ₀) = v.valuation (x : K) := by
+    (v.valuationOfNeZeroToFun x : ℤₘ₀) = v.valuation K x := by
   classical
-  rw [show v.valuation (x : K) = _ * _ by rfl]
+  rw [show v.valuation K x = _ * _ by rfl]
   rw [Units.val_inv_eq_inv_val]
   change _ = ite _ _ _ * (ite _ _ _)⁻¹
   simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
@@ -110,7 +110,7 @@ def valuationOfNeZero : Kˣ →* Multiplicative ℤ where
     simp only [valuationOfNeZeroToFun_eq]; exact map_mul _ _ _
 
 @[simp]
-theorem valuationOfNeZero_eq (x : Kˣ) : (v.valuationOfNeZero x : ℤₘ₀) = v.valuation (x : K) :=
+theorem valuationOfNeZero_eq (x : Kˣ) : (v.valuationOfNeZero x : ℤₘ₀) = v.valuation K x :=
   valuationOfNeZeroToFun_eq v x
 
 @[simp]
@@ -120,10 +120,10 @@ theorem valuation_of_unit_eq (x : Rˣ) :
   constructor
   · exact v.valuation_le_one x
   · obtain ⟨x, _, hx, _⟩ := x
-    change ¬v.valuation (algebraMap R K x) < 1
+    change ¬v.valuation K (algebraMap R K x) < 1
     apply_fun v.intValuation at hx
     rw [map_one, map_mul] at hx
-    rw [not_lt, ← hx, ← mul_one <| v.valuation _, valuation_of_algebraMap,
+    rw [not_lt, ← hx, ← mul_one <| v.valuation _ _, valuation_of_algebraMap,
       mul_le_mul_left <| zero_lt_iff.2 <| left_ne_zero_of_mul_eq_one hx]
     exact v.intValuation_le_one _
 

Mathlib/RingTheory/LaurentSeries.lean

@@ -555,7 +555,7 @@ open IsDedekindDomain.HeightOneSpectrum PowerSeries
 open scoped LaurentSeries
 
 theorem valuation_eq_LaurentSeries_valuation (P : RatFunc K) :
-    (Polynomial.idealX K).valuation P = (PowerSeries.idealX K).valuation (P : K⸨X⸩) := by
+    (Polynomial.idealX K).valuation _ P = (PowerSeries.idealX K).valuation K⸨X⸩ P := by
   refine RatFunc.induction_on' P ?_
   intro f g h
   rw [Polynomial.valuation_of_mk K f h, RatFunc.mk_eq_mk' f h, Eq.comm]
@@ -572,7 +572,7 @@ namespace LaurentSeries
 
 open IsDedekindDomain.HeightOneSpectrum PowerSeries RatFunc
 
-instance : Valued K⸨X⸩ ℤₘ₀ := Valued.mk' (PowerSeries.idealX K).valuation
+instance : Valued K⸨X⸩ ℤₘ₀ := Valued.mk' ((PowerSeries.idealX K).valuation _)
 
 theorem valuation_X_pow (s : ℕ) :
     Valued.v (((X : K⟦X⟧) : K⸨X⸩) ^ s) = Multiplicative.ofAdd (-(s : ℤ)) := by