Ostrowski's theorem for K(X)

This file proves Ostrowski's theorem for the field of rational functions K(X), where K is any field: if v is a valuation on K(X) which is trivial on elements of K, then v is equivalent to either the I-adic valuation for some I : HeightOneSpectrum K[X], or to the valuation at infinity FunctionField.inftyValuation K.

Main results

• RatFunc.valuation_isEquiv_infty_or_adic: Ostrowski's theorem for K(X).

TODO

• Show that a nontrivial valuation v, trivial on K, is a rank one discrete valuation. (*)

theorem RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} {f : RatFunc K} [Valuation.IsTrivialOn K v] (hlt : 1 < v X) (hf : f ≠ 0) : v f = v X ^ f.intDegree

theorem RatFunc.valuation_isEquiv_inftyValuation_of_one_lt_valuation_X {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [DecidableEq (RatFunc K)] [Valuation.IsTrivialOn K v] (hlt : 1 < v X) : v.IsEquiv (inftyValuation K)

theorem RatFunc.setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) : {p : Polynomial K | v ↑p < 1 ∧ p ≠ 0}.Nonempty

@[deprecated RatFunc.setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty (since := "2026-07-09")]

theorem RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) : {p : Polynomial K | v ↑p < 1 ∧ p ≠ 0}.Nonempty

Alias of RatFunc.setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty.

theorem RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [Valuation.IsTrivialOn K v] (hne : {p : Polynomial K | v ↑p < 1 ∧ p ≠ 0}.Nonempty) : Irreducible (⋯.min {p : Polynomial K | v ↑p < 1 ∧ p ≠ 0} hne)

@[reducible, inline]

noncomputable abbrev RatFunc.uniformizingPolynomial {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) : Polynomial K

A uniformizing element for the valuation v, as a polynomial in K[X].

Equations

• RatFunc.uniformizingPolynomial hle = ⋯.min {p : Polynomial K | v ↑p < 1 ∧ p ≠ 0} ⋯

theorem RatFunc.uniformizingPolynomial_ne_zero {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) : uniformizingPolynomial hle ≠ 0

theorem RatFunc.valuation_uniformizingPolynomial_lt_one {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) : v ↑(uniformizingPolynomial hle) < 1

noncomputable def RatFunc.valuationIdeal {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) : IsDedekindDomain.HeightOneSpectrum (Polynomial K)

The maximal ideal of K[X] generated by the uniformizingPolynomial for v.

Equations

• RatFunc.valuationIdeal hle = { asIdeal := Polynomial K ∙ RatFunc.uniformizingPolynomial hle, isPrime := ⋯, ne_bot := ⋯ }

theorem RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) {p : Polynomial K} (hp : p ≠ 0) : v ((algebraMap (Polynomial K) (RatFunc K)) p) = v (↑(uniformizingPolynomial hle) ^ (Associates.mk (valuationIdeal hle).asIdeal).count (Associates.mk (Ideal.span {p})).factors)

theorem RatFunc.exists_zpow_uniformizingPolynomial {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) {f : RatFunc K} (hf : f ≠ 0) : ∃ (z : ℤ), v f = v ↑(uniformizingPolynomial hle) ^ z

theorem RatFunc.uniformizingPolynomial_isUniformizer {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) [hv : v.IsRankOneDiscrete] : v.IsUniformizer ↑(uniformizingPolynomial hle)

theorem RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [v.IsNontrivial] [Valuation.IsTrivialOn K v] (hle : v X ≤ 1) : v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (valuationIdeal hle))

theorem RatFunc.adicValuation_not_isEquiv_infty_valuation {K : Type u_1} [Field K] [DecidableEq (RatFunc K)] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : ¬(IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) p).IsEquiv (inftyValuation K)

theorem RatFunc.adicValuation_ne_inftyValuation {K : Type u_1} [Field K] [DecidableEq (RatFunc K)] (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)) : IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) p ≠ inftyValuation K

theorem RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [Valuation.IsTrivialOn K v] [v.IsNontrivial] (hle : v X ≤ 1) : ∃ (u : IsDedekindDomain.HeightOneSpectrum (Polynomial K)), v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) u)

theorem RatFunc.valuation_isEquiv_infty_or_adic {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [Valuation.IsTrivialOn K v] [v.IsNontrivial] [DecidableEq (RatFunc K)] : Xor (v.IsEquiv (inftyValuation K)) (∃! u : IsDedekindDomain.HeightOneSpectrum (Polynomial K), v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) u))

Ostrowski's Theorem for K(X) with K any field: A valuation 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 RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty {K : Type u_1} {Γ : Type u_2} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} [Valuation.IsTrivialOn K v] [v.IsNontrivial] [DecidableEq (RatFunc K)] (hni : ¬v.IsEquiv (inftyValuation K)) : ∃! u : IsDedekindDomain.HeightOneSpectrum (Polynomial K), v.IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) u)