From c655316477b6e16ddb51557c5aa6406bb38096b6 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Fri, 5 Jul 2024 11:29:00 +0000 Subject: [PATCH] feat: add properties of the X-adic valuation on `PowerSeries K` (#13064) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 52 ++++++++++++++++- .../DedekindDomain/AdicValuation.lean | 12 ++++ Mathlib/RingTheory/LaurentSeries.lean | 57 ++++++++++++++++++- Mathlib/RingTheory/PowerSeries/Inverse.lean | 32 +++++++---- 4 files changed, 141 insertions(+), 12 deletions(-) diff --git a/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean b/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean index 2e9bbd22095b6..7d20887628092 100644 --- a/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean +++ b/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 diff --git a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean b/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean index aef163c676be0..ffa66ef641ea1 100644 --- a/Mathlib/RingTheory/DedekindDomain/AdicValuation.lean +++ b/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` -/ diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean index f3203730b2351..e7cfb7947f648 100644 --- a/Mathlib/RingTheory/LaurentSeries.lean +++ b/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 diff --git a/Mathlib/RingTheory/PowerSeries/Inverse.lean b/Mathlib/RingTheory/PowerSeries/Inverse.lean index 95331cd6b797d..e5c38e19b4dd4 100644 --- a/Mathlib/RingTheory/PowerSeries/Inverse.lean +++ b/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