Normalizing a ℤᵐ⁰-valued valuation of a field

The orders ord_v f attained by a ℤᵐ⁰-valued valuation v of a field form a subgroup of ℤ, so they are the multiples of a single natural number, the index Valuation.ordIndex v; it is zero exactly when v is trivial. Dividing the order by the index produces the normalization Valuation.normalization v: the valuation equivalent to v whose value group is all of ℤᵐ⁰ (the trivial valuation, when v is trivial).

This is the operation that turns the restriction of a discrete valuation along a field extension back into a normalized one, and the index it divides by is the ramification index of that extension.

Main definitions

• Valuation.ordIndex: the least positive order attained by v, and 0 if there is none.
• Valuation.normalization: the normalization of v.

Main results

• Valuation.ordIndex_dvd_ord: every order attained by v is a multiple of the index.
• Valuation.ordIndex_eq_mul_of_forall_ord_eq: indices multiply when one order function is a natural-number multiple of another.
• Valuation.ord_normalization_mul_ordIndex: the order function of v is the index times the order function of its normalization — the defining relation between the two.
• Valuation.isEquiv_normalization: a valuation is equivalent to its normalization; in particular the two have the same valuation subring.
• Valuation.normalization_surjective: the normalization of a nontrivial valuation is surjective.
• Valuation.IsTrivialOn.normalization: normalization preserves triviality on a base semiring.

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

The index of a ℤᵐ⁰-valued valuation of a field: the least positive order it attains, and 0 when the valuation is trivial. The orders attained by v are exactly the multiples of the index (Valuation.ordIndex_dvd_ord and Valuation.exists_ord_eq_ordIndex).

Equations

• v.ordIndex = sInf {n : ℕ | 0 < n ∧ ∃ (f : F), v.ord f = ↑n}

theorem Valuation.ordIndex_le {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {n : ℕ} (hn : 0 < n) {f : F} (hf : v.ord f = ↑n) : v.ordIndex ≤ n

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

A valuation attaining a nonzero order has positive index.

theorem Valuation.exists_ord_eq_ordIndex {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) : ∃ (f : F), v.ord f = ↑v.ordIndex

Every valuation attains its index as an order, including the trivial valuation.

theorem Valuation.ordIndex_eq_zero_iff {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) : v.ordIndex = 0 ↔ ∀ (f : F), v.ord f = 0

The index vanishes exactly for the trivial valuations.

theorem Valuation.ordIndex_dvd_ord {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : F) : ↑v.ordIndex ∣ v.ord f

Every order attained by a valuation is a multiple of its index.

theorem Valuation.ordIndex_eq_mul_of_forall_ord_eq {F : Type u_1} [Field F] (v w : Valuation F (WithZero (Multiplicative ℤ))) {e : ℕ} (hord : ∀ (f : F), v.ord f = ↑e * w.ord f) : v.ordIndex = e * w.ordIndex

If one order function is a natural-number multiple of another, their indices differ by the same factor. This includes a zero factor and trivial valuations.

theorem Valuation.ordIndex_ne_zero_of_isNontrivial {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) [v.IsNontrivial] : v.ordIndex ≠ 0

A nontrivial valuation has nonzero order index. This is the hypothesis Valuation.normalization_surjective asks for, so it is what lets a nontrivial valuation be normalized.

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

The normalization of a ℤᵐ⁰-valued valuation of a field: the valuation whose order function is the order function of v divided by the index Valuation.ordIndex v. It is equivalent to v and, as soon as v is nontrivial, surjective.

Equations

• v.normalization = { toFun := fun (f : F) => if f = 0 then 0 else WithZero.exp (-(v.ord f / ↑v.ordIndex)), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

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

@[simp]

theorem Valuation.ord_normalization {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : F) : v.normalization.ord f = v.ord f / ↑v.ordIndex

theorem Valuation.ord_normalization_mul_ordIndex {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (f : F) : v.normalization.ord f * ↑v.ordIndex = v.ord f

The defining relation between a valuation and its normalization: the order function of v is the index times the order function of normalization v.

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

theorem Valuation.isEquiv_normalization {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) : v.normalization.IsEquiv v

A valuation is equivalent to its normalization.

@[simp]

theorem Valuation.valuationSubring_normalization {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) : v.normalization.valuationSubring = v.valuationSubring

@[simp]

theorem Valuation.ordIndex_eq_one_of_surjective {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (hv : Function.Surjective ⇑v) : v.ordIndex = 1

A surjective valuation has index 1: it already attains the order 1, and the index divides every order attained.

@[simp]

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

A surjective valuation is its own normalization: normalizing divides every order by the index, which is 1.

theorem Valuation.normalization_surjective {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) (hv : v.ordIndex ≠ 0) : Function.Surjective ⇑v.normalization

The normalization of a nontrivial valuation is surjective: its value group is all of ℤᵐ⁰.

theorem Valuation.IsTrivialOn.normalization {F : Type u_1} [Field F] (v : Valuation F (WithZero (Multiplicative ℤ))) {A : Type u_2} [CommSemiring A] [Algebra A F] [IsTrivialOn A v] : IsTrivialOn A v.normalization

Normalization preserves triviality on a base semiring.