Additive orders of discrete valuations

This file packages the additive order attached to a ℤᵐ⁰-valued valuation and develops the facts that do not depend on a choice of constant field. The convention is ord_v f = -log (v f), so a uniformizer has order one. As WithZero.log 0 = 0, the order has the junk value ord_v 0 = 0; hypotheses excluding zero are included where necessary.

noncomputable def Valuation.ord {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : F) : ℤ

The additive order attached to a ℤᵐ⁰-valued valuation, with the convention that a uniformizer has order one. It has the junk value ord_v 0 = 0.

Equations

• v.ord f = -(v f).log

theorem Valuation.ord_def {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : F) : v.ord f = -(v f).log

@[simp]

theorem Valuation.ord_comap {F : Type u_1} [Field F] {K : Type u_2} [Field K] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : K →+* F) (x : K) : (comap f v).ord x = v.ord (f x)

The order function commutes with restriction along a ring homomorphism.

theorem Valuation.valuation_eq_exp_neg_ord {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f : F} (hf : f ≠ 0) : v f = WithZero.exp (-v.ord f)

Translation between the multiplicative valuation and its additive order.

theorem Valuation.ord_eq_iff_valuation_eq_exp_neg {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f : F} (hf : f ≠ 0) {n : ℤ} : v.ord f = n ↔ v f = WithZero.exp (-n)

@[simp]

theorem Valuation.ord_zero {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) : v.ord 0 = 0

@[simp]

theorem Valuation.ord_one {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) : v.ord 1 = 0

theorem Valuation.ord_mul {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) : v.ord (f * g) = v.ord f + v.ord g

theorem Valuation.ord_prod {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {ι : Type u_2} (s : Finset ι) {f : ι → F} (hf : ∀ i ∈ s, f i ≠ 0) : v.ord (∏ i ∈ s, f i) = ∑ i ∈ s, v.ord (f i)

@[simp]

theorem Valuation.ord_inv {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : F) : v.ord f⁻¹ = -v.ord f

@[simp]

theorem Valuation.ord_zpow {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : F) (n : ℤ) : v.ord (f ^ n) = n * v.ord f

@[simp]

theorem Valuation.ord_pow {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : F) (n : ℕ) : v.ord (f ^ n) = ↑n * v.ord f

theorem Valuation.ord_div {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) : v.ord (f / g) = v.ord f - v.ord g

@[simp]

theorem Valuation.ord_neg {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : F) : v.ord (-f) = v.ord f

theorem Valuation.ord_div_zpow {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f t : F} (hf : f ≠ 0) (ht : t ≠ 0) (n : ℤ) : v.ord (f / t ^ n) = v.ord f - n * v.ord t

The order of a quotient by an integral power.

theorem Valuation.isNontrivial_of_surjective {R : Type u_2} [Ring R] {v : Valuation R (WithZero (Multiplicative ℤ))} (hv : Function.Surjective ⇑v) : v.IsNontrivial

A surjective valuation onto ℤᵐ⁰ is nontrivial. Surjectivity is the form the hypothesis usually arrives in — a Place carries it by definition — while the results about order and normalization are stated for a nontrivial valuation, and this converts one to the other.

theorem Valuation.ord_surjective {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (hv : Function.Surjective ⇑v) : Function.Surjective v.ord

theorem Valuation.mem_valuationSubring_iff_ord_nonneg {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f : F} : f ∈ v.valuationSubring ↔ 0 ≤ v.ord f

theorem Valuation.min_ord_le_ord_add {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f g : F} (h : f + g ≠ 0) : min (v.ord f) (v.ord g) ≤ v.ord (f + g)

The ultrametric inequality in additive form. The hypothesis excludes the junk value at zero.

theorem Valuation.ord_add_eq_min_of_ord_ne {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) (h : v.ord f ≠ v.ord g) : v.ord (f + g) = min (v.ord f) (v.ord g)

The strict triangle inequality for an additive order.

theorem Valuation.ord_lt_ord_iff_valuation_gt {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f g : F} (hf : f ≠ 0) (hg : g ≠ 0) : v.ord f < v.ord g ↔ v g < v f

The order reverses the valuation: an element of larger order has smaller valuation. The hypotheses exclude the junk value ord_v 0 = 0.

theorem Valuation.sum_ne_zero_of_forall_ord_lt {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {ι : Type u_2} {s : Finset ι} {f : ι → F} {j : ι} (hj : j ∈ s) (hfj : f j ≠ 0) (hlt : ∀ i ∈ s, i ≠ j → v.ord (f j) < v.ord (f i)) : ∑ i ∈ s, f i ≠ 0

A finite sum one of whose summands has strictly least order does not vanish. A vanishing summand is no obstacle: it carries the junk order 0, so the hypothesis already forces the distinguished summand to have negative order there.

theorem Valuation.ord_sum_eq_of_forall_lt {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {ι : Type u_2} {s : Finset ι} {f : ι → F} {j : ι} (hj : j ∈ s) (hfj : f j ≠ 0) (hlt : ∀ i ∈ s, i ≠ j → v.ord (f j) < v.ord (f i)) : v.ord (∑ i ∈ s, f i) = v.ord (f j)

The order of a finite sum with a strict minimum: if one summand has strictly smaller order than each of the others, the sum has that order. This is the Finset.sum form of TauCeti.Valuation.ord_add_eq_min_of_ord_ne; only the distinguished summand is asked to be nonzero, which keeps the junk value ord_v 0 = 0 out of the conclusion.

theorem Valuation.valueGroup_eq_top_of_surjective {F : Type u_2} [Ring F] (v : Valuation F (WithZero (Multiplicative ℤ))) (hv : Function.Surjective ⇑v) : (↑v).valueGroup = ⊤

Surjectivity of v makes its value group the whole of ℤᵐ⁰.

theorem Valuation.nontrivial_valueGroup_of_surjective {F : Type u_2} [Ring F] (v : Valuation F (WithZero (Multiplicative ℤ))) (hv : Function.Surjective ⇑v) : Nontrivial ↥(↑v).valueGroup

A surjective ℤᵐ⁰-valued valuation has nontrivial value group.

theorem Valuation.valuationSubring_isDiscreteValuationRing_of_surjective {F : Type u_2} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (hv : Function.Surjective ⇑v) : IsDiscreteValuationRing ↥v.valuationSubring

The valuation ring of a surjective ℤᵐ⁰-valued valuation is a DVR.

theorem Valuation.isUniformizer_iff_ord_eq_one_of_surjective {F : Type u_2} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) [Nontrivial ↥(↑v).valueGroup] (hv : Function.Surjective ⇑v) {t : F} : v.IsUniformizer t ↔ v.ord t = 1

Uniformizers of a surjective ℤᵐ⁰-valuation are exactly the elements of order one.

theorem Valuation.exists_isUniformizer_of_surjective {F : Type u_2} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) [Nontrivial ↥(↑v).valueGroup] (hv : Function.Surjective ⇑v) : ∃ (t : F), v.IsUniformizer t

theorem Valuation.isUnit_iff_ord_eq_zero {F : Type u_2} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {x : ↥v.valuationSubring} (hx : ↑x ≠ 0) : IsUnit x ↔ v.ord ↑x = 0

theorem Valuation.exists_eq_zpow_mul_unit_of_surjective {F : Type u_2} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) [Nontrivial ↥(↑v).valueGroup] (hv : Function.Surjective ⇑v) {t : F} (ht : v.IsUniformizer t) {f : F} (hf : f ≠ 0) : ∃ (u : (↥v.valuationSubring)ˣ), f = t ^ v.ord f * ↑↑u

Existence half of the uniformizer expansion for a surjective valuation.

theorem Valuation.mem_maximalIdeal_iff_ord_pos {F : Type u_2} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {f : ↥v.valuationSubring} (hf : ↑f ≠ 0) : f ∈ IsLocalRing.maximalIdeal ↥v.valuationSubring ↔ 0 < v.ord ↑f

theorem Valuation.valuationSubring_ne_top_of_surjective {F : Type u_2} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (hv : Function.Surjective ⇑v) : v.valuationSubring ≠ ⊤

theorem Valuation.IsEquiv.ord_nonneg_iff {F : Type u_2} [Field F] {v w : Valuation F (WithZero (Multiplicative ℤ))} (h : v.IsEquiv w) (f : F) : 0 ≤ v.ord f ↔ 0 ≤ w.ord f

Equivalent valuations agree on which elements have nonnegative order. Equivalence identifies the valuation subrings, and membership of the subring is exactly nonnegativity of the additive order.

Only equivalence is needed; neither valuation has to be surjective.

theorem Valuation.IsEquiv.ord_eq_zero_iff {F : Type u_2} [Field F] {v w : Valuation F (WithZero (Multiplicative ℤ))} (h : v.IsEquiv w) (f : F) : v.ord f = 0 ↔ w.ord f = 0

Equivalent valuations agree on which elements have order zero. This is the additive-order analogue of Valuation.IsEquiv.eq_one_iff_eq_one: away from 0, order zero says the valuation is 1, so the two valuations have the same units. The junk value ord v 0 = 0 is absorbed on both sides.

Only equivalence is needed; neither valuation has to be surjective.

theorem Valuation.eq_of_isEquiv_of_surjective {F : Type u_2} [Field F] {v w : Valuation F (WithZero (Multiplicative ℤ))} (hv : Function.Surjective ⇑v) (hw : Function.Surjective ⇑w) (h : v.IsEquiv w) : v = w

Two equivalent normalized ℤᵐ⁰-valuations are equal.