feat: add properties of the X-adic valuation on PowerSeries K (#13064)

Add some properties of the $X$-adic valuation on the rings $K[X]$ and $K[[X]]$ when $K$ is a field. It is an intermediate step towards the proof that the $X$-adic completion of $K(X)$ is isomorphic to $K((X))$.

Co-authored-by: María Inés de Frutos-Fernández @mariainesdff

Mathlib/FieldTheory/RatFunc/AsPolynomial.lean

@@ -1,20 +1,25 @@
 /-
 Copyright (c) 2021 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Anne Baanen
+Authors: Anne Baanen, María Inés de Frutos-Fernández, Filippo A. E. Nuccio
 -/
 import Mathlib.FieldTheory.RatFunc.Basic
 import Mathlib.RingTheory.EuclideanDomain
+import Mathlib.RingTheory.DedekindDomain.AdicValuation
 import Mathlib.RingTheory.Localization.FractionRing
 import Mathlib.RingTheory.Polynomial.Content
 
 /-!
 # Generalities on the polynomial structure of rational functions
+* Main evaluation properties
+* Study of the X-adic valuation
 
 ## Main definitions
 - `RatFunc.C` is the constant polynomial
 - `RatFunc.X` is the indeterminate
 - `RatFunc.eval` evaluates a rational function given a value for the indeterminate
+- `IdealX` is the principal ideal generated by `X` in the ring of polynomials over a field K,
+  regarded as an element of the height-one-spectrum.
 -/
 
 noncomputable section
@@ -207,3 +212,48 @@ theorem eval_mul {x y : RatFunc K} (hx : Polynomial.eval₂ f a (denom x) ≠ 0)
 end Field
 
 end Eval
+
+end RatFunc
+
+section AdicValuation
+
+variable (K : Type*) [Field K]
+
+namespace Polynomial
+
+open IsDedekindDomain.HeightOneSpectrum
+
+/-- This is the principal ideal generated by `X` in the ring of polynomials over a field K,
+  regarded as an element of the height-one-spectrum. -/
+def idealX : IsDedekindDomain.HeightOneSpectrum K[X] where
+  asIdeal := Ideal.span {X}
+  isPrime := by rw [Ideal.span_singleton_prime]; exacts [Polynomial.prime_X, Polynomial.X_ne_zero]
+  ne_bot  := by rw [ne_eq, Ideal.span_singleton_eq_bot]; exact Polynomial.X_ne_zero
+
+@[simp]
+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
+  rw [← RatFunc.algebraMap_X, valuation_of_algebraMap, intValuation_singleton]
+  · exact Polynomial.X_ne_zero
+  · exact idealX_span K
+
+end Polynomial
+
+namespace RatFunc
+
+open scoped DiscreteValuation
+
+open Polynomial
+
+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
+
+end RatFunc
+
+end AdicValuation

Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

@@ -82,6 +82,7 @@ def intValuationDef (r : R) : ℤₘ₀ :=
       (-(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r} : Ideal R)).factors : ℤ))
 #align is_dedekind_domain.height_one_spectrum.int_valuation_def IsDedekindDomain.HeightOneSpectrum.intValuationDef
 
+
 theorem intValuationDef_if_pos {r : R} (hr : r = 0) : v.intValuationDef r = 0 :=
   if_pos hr
 #align is_dedekind_domain.height_one_spectrum.int_valuation_def_if_pos IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos
@@ -229,6 +230,10 @@ def intValuation : Valuation R ℤₘ₀ where
   map_add_le_max' := IntValuation.map_add_le_max' v
 #align is_dedekind_domain.height_one_spectrum.int_valuation IsDedekindDomain.HeightOneSpectrum.intValuation
 
+
+theorem intValuation_apply {r : R} (v : IsDedekindDomain.HeightOneSpectrum R) :
+    intValuation v r = intValuationDef v r := rfl
+
 /-- There exists `π ∈ R` with `v`-adic valuation `Multiplicative.ofAdd (-1)`. -/
 theorem int_valuation_exists_uniformizer :
     ∃ π : R, v.intValuationDef π = Multiplicative.ofAdd (-1 : ℤ) := by
@@ -254,6 +259,13 @@ theorem int_valuation_exists_uniformizer :
   exact Nat.eq_of_le_of_lt_succ mem nmem
 #align is_dedekind_domain.height_one_spectrum.int_valuation_exists_uniformizer IsDedekindDomain.HeightOneSpectrum.int_valuation_exists_uniformizer
 
+/-- The `I`-adic valuation of a generator of `I` equals `(-1 : ℤₘ₀)` -/
+theorem intValuation_singleton {r : R} (hr : r ≠ 0) (hv : v.asIdeal = Ideal.span {r}) :
+    v.intValuation r = Multiplicative.ofAdd (-1 : ℤ) := by
+  rw [intValuation_apply, v.intValuationDef_if_neg hr, ← hv, Associates.count_self, Int.ofNat_one,
+    ofAdd_neg, WithZero.coe_inv]
+  apply v.associates_irreducible
+
 /-! ### Adic valuations on the field of fractions `K` -/
 
 

Mathlib/RingTheory/LaurentSeries.lean

@@ -1,12 +1,14 @@
 /-
 Copyright (c) 2021 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Aaron Anderson
+Authors: Aaron Anderson, María Inés de Frutos-Fernández, Filippo A. E. Nuccio
 -/
 import Mathlib.Data.Int.Interval
 import Mathlib.RingTheory.Binomial
+import Mathlib.RingTheory.DedekindDomain.Basic
 import Mathlib.RingTheory.HahnSeries.PowerSeries
 import Mathlib.RingTheory.HahnSeries.Summable
+import Mathlib.RingTheory.PowerSeries.Inverse
 import Mathlib.FieldTheory.RatFunc.AsPolynomial
 import Mathlib.RingTheory.Localization.FractionRing
 
@@ -25,6 +27,7 @@ import Mathlib.RingTheory.Localization.FractionRing
   `HahnSeries.ofPowerSeries`.
 * Embedding of rational functions into Laurent series, provided as a coercion, utilizing
 the underlying `RatFunc.coeAlgHom`.
+* Study of the X-Adic valuation on the ring of Laurent series over a field
 
 ## Main Results
 * Basic properties of Hasse derivatives
@@ -429,3 +432,55 @@ instance : IsScalarTower F[X] (RatFunc F) (LaurentSeries F) :=
 end RatFunc
 
 end RatFunc
+
+section AdicValuation
+
+namespace PowerSeries
+
+variable (K : Type*) [Field K]
+
+/-- The prime ideal `(X)` of `PowerSeries K`, when `K` is a field, as a term of the
+`HeightOneSpectrum`. -/
+def idealX : IsDedekindDomain.HeightOneSpectrum K⟦X⟧ where
+  asIdeal := Ideal.span {X}
+  isPrime := PowerSeries.span_X_isPrime
+  ne_bot  := by rw [ne_eq, Ideal.span_singleton_eq_bot]; exact X_ne_zero
+
+open RatFunc IsDedekindDomain.HeightOneSpectrum
+
+variable {K}
+
+/- The `X`-adic valuation of a polynomial equals the `X`-adic valuation of its coercion to `K⟦X⟧`-/
+theorem intValuation_eq_of_coe (P : K[X]) :
+    (Polynomial.idealX K).intValuation P = (idealX K).intValuation (P : K⟦X⟧) := by
+  by_cases hP : P = 0
+  · rw [hP, Valuation.map_zero, Polynomial.coe_zero, Valuation.map_zero]
+  simp only [intValuation_apply]
+  rw [intValuationDef_if_neg _ hP, intValuationDef_if_neg _ <| coe_ne_zero hP]
+  simp only [idealX_span, ofAdd_neg, inv_inj, WithZero.coe_inj, EmbeddingLike.apply_eq_iff_eq,
+    Nat.cast_inj]
+  have span_ne_zero :
+    (Ideal.span {P} : Ideal K[X]) ≠ 0 ∧ (Ideal.span {Polynomial.X} : Ideal K[X]) ≠ 0 := by
+    simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, hP, Polynomial.X_ne_zero,
+      not_false_iff, and_self_iff]
+  have span_ne_zero' :
+    (Ideal.span {↑P} : Ideal K⟦X⟧) ≠ 0 ∧ ((idealX K).asIdeal : Ideal K⟦X⟧) ≠ 0 := by
+    simp only [Ideal.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot, coe_eq_zero_iff, hP,
+      not_false_eq_true, true_and, (idealX K).3]
+  rw [count_associates_factors_eq (Ideal.span {P}) (Ideal.span {Polynomial.X}) (span_ne_zero).1
+    (Ideal.span_singleton_prime Polynomial.X_ne_zero|>.mpr prime_X) (span_ne_zero).2,
+    count_associates_factors_eq (Ideal.span {↑(P : K⟦X⟧)}) (idealX K).asIdeal]
+  convert (normalized_count_X_eq_of_coe hP).symm
+  exacts [count_span_normalizedFactors_eq_of_normUnit hP Polynomial.normUnit_X prime_X,
+    count_span_normalizedFactors_eq_of_normUnit (coe_ne_zero hP) normUnit_X X_prime,
+    span_ne_zero'.1, (idealX K).isPrime, span_ne_zero'.2]
+
+/-- The integral valuation of the power series `X : K⟦X⟧` equals `(ofAdd -1) : ℤₘ₀`-/
+@[simp]
+theorem intValuation_X : (idealX K).intValuationDef X = ↑(Multiplicative.ofAdd (-1 : ℤ)) := by
+  rw [← Polynomial.coe_X, ← intValuation_apply, ← intValuation_eq_of_coe]
+  apply intValuation_singleton _ Polynomial.X_ne_zero (by rfl)
+
+end PowerSeries
+
+end AdicValuation

Mathlib/RingTheory/PowerSeries/Inverse.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Kenny Lau
+Authors: Johan Commelin, Kenny Lau, María Inés de Frutos-Fernández, Filippo A. E. Nuccio
 -/
 
 import Mathlib.RingTheory.DiscreteValuationRing.Basic
@@ -10,7 +10,6 @@ import Mathlib.RingTheory.PowerSeries.Basic
 import Mathlib.RingTheory.PowerSeries.Order
 
 
-
 #align_import ring_theory.power_series.basic from "leanprover-community/mathlib"@"2d5739b61641ee4e7e53eca5688a08f66f2e6a60"
 
 /-! # Formal power series - Inverses
@@ -109,13 +108,13 @@ theorem mul_invOfUnit (φ : R⟦X⟧) (u : Rˣ) (h : constantCoeff R φ = u) :
 
 /-- Two ways of removing the constant coefficient of a power series are the same. -/
 theorem sub_const_eq_shift_mul_X (φ : R⟦X⟧) :
-    φ - C R (constantCoeff R φ) = (PowerSeries.mk fun p => coeff R (p + 1) φ) * X :=
+    φ - C R (constantCoeff R φ) = (mk fun p ↦ coeff R (p + 1) φ) * X :=
   sub_eq_iff_eq_add.mpr (eq_shift_mul_X_add_const φ)
 set_option linter.uppercaseLean3 false in
 #align power_series.sub_const_eq_shift_mul_X PowerSeries.sub_const_eq_shift_mul_X
 
 theorem sub_const_eq_X_mul_shift (φ : R⟦X⟧) :
-    φ - C R (constantCoeff R φ) = X * PowerSeries.mk fun p => coeff R (p + 1) φ :=
+    φ - C R (constantCoeff R φ) = X * mk fun p ↦ coeff R (p + 1) φ :=
   sub_eq_iff_eq_add.mpr (eq_X_mul_shift_add_const φ)
 set_option linter.uppercaseLean3 false in
 #align power_series.sub_const_eq_X_mul_shift PowerSeries.sub_const_eq_X_mul_shift
@@ -282,7 +281,7 @@ theorem Unit_of_divided_by_X_pow_order_zero : Unit_of_divided_by_X_pow_order (0
 
 theorem eq_divided_by_X_pow_order_Iff_Unit {f : k⟦X⟧} (hf : f ≠ 0) :
     f = divided_by_X_pow_order hf ↔ IsUnit f :=
-  ⟨fun h => by rw [h]; exact isUnit_divided_by_X_pow_order hf, fun h => by
+  ⟨fun h ↦ by rw [h]; exact isUnit_divided_by_X_pow_order hf, fun h ↦ by
     have : f.order.get (order_finite_iff_ne_zero.mpr hf) = 0 := by
       simp only [order_zero_of_unit h, PartENat.get_zero]
     convert (self_eq_X_pow_order_mul_divided_by_X_pow_order hf).symm
@@ -355,7 +354,7 @@ theorem maximalIdeal_eq_span_X : LocalRing.maximalIdeal (k⟦X⟧) = Ideal.span
 instance : NormalizationMonoid k⟦X⟧ where
   normUnit f := (Unit_of_divided_by_X_pow_order f)⁻¹
   normUnit_zero := by simp only [Unit_of_divided_by_X_pow_order_zero, inv_one]
-  normUnit_mul  := fun hf hg => by
+  normUnit_mul  := fun hf hg ↦ by
     simp only [← mul_inv, inv_inj]
     simp only [Unit_of_divided_by_X_pow_order_nonzero (mul_ne_zero hf hg),
       Unit_of_divided_by_X_pow_order_nonzero hf, Unit_of_divided_by_X_pow_order_nonzero hg,
@@ -367,23 +366,36 @@ instance : NormalizationMonoid k⟦X⟧ where
     rw [inv_inj, Units.ext_iff, ← hu, Unit_of_divided_by_X_pow_order_nonzero h₀.ne_zero]
     exact ((eq_divided_by_X_pow_order_Iff_Unit h₀.ne_zero).mpr h₀).symm
 
-theorem normUnit_X : normUnit (X : PowerSeries k) = 1 := by
+theorem normUnit_X : normUnit (X : k⟦X⟧) = 1 := by
   simp [normUnit, ← Units.val_eq_one, Unit_of_divided_by_X_pow_order_nonzero]
 
-theorem X_eq_normalizeX : (X : PowerSeries k) = normalize X := by
+theorem X_eq_normalizeX : (X : k⟦X⟧) = normalize X := by
   simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]
 
+open UniqueFactorizationMonoid Classical
+
+theorem normalized_count_X_eq_of_coe {P : k[X]} (hP : P ≠ 0) :
+    Multiset.count PowerSeries.X (normalizedFactors (P : k⟦X⟧)) =
+      Multiset.count Polynomial.X (normalizedFactors P) := by
+  apply eq_of_forall_le_iff
+  simp only [← PartENat.coe_le_coe]
+  rw [X_eq_normalize, PowerSeries.X_eq_normalizeX, ← multiplicity_eq_count_normalizedFactors
+    irreducible_X hP, ← multiplicity_eq_count_normalizedFactors X_irreducible] <;>
+  simp only [← multiplicity.pow_dvd_iff_le_multiplicity, Polynomial.X_pow_dvd_iff,
+    PowerSeries.X_pow_dvd_iff, Polynomial.coeff_coe P, implies_true, ne_eq, coe_eq_zero_iff, hP,
+    not_false_eq_true]
+
 open LocalRing
 
 theorem ker_coeff_eq_max_ideal : RingHom.ker (constantCoeff k) = maximalIdeal _ :=
-  Ideal.ext fun _ => by
+  Ideal.ext fun _ ↦ by
     rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]
 
 /-- The ring isomorphism between the residue field of the ring of power series valued in a field `K`
 and `K` itself. -/
 def residueFieldOfPowerSeries : ResidueField k⟦X⟧ ≃+* k :=
   (Ideal.quotEquivOfEq (ker_coeff_eq_max_ideal).symm).trans
-    (RingHom.quotientKerEquivOfSurjective PowerSeries.constantCoeff_surj)
+    (RingHom.quotientKerEquivOfSurjective constantCoeff_surj)
 
 end DiscreteValuationRing