Centres of valuations on subrings

A valuation of a field K that is bounded by 1 on a commutative ring R determines a prime ideal of R: the elements whose images have value strictly below 1. When K is the fraction field of R and the valuation is nontrivial, this centre is nonzero. The value group may be any linearly ordered commutative group with zero.

Main definitions and results

• Valuation.centerIdeal: the prime centre of a valuation bounded by 1 on R.
• Valuation.mem_centerIdeal: membership is equivalent to valuation strictly below 1.
• Valuation.centerIdeal_ne_bot: a nontrivial valuation of the fraction field has nonzero centre.
• Valuation.heightOneSpectrum: the nonzero prime centre bundled as HeightOneSpectrum R. This structure records a nonzero prime ideal; it is a height one prime when R is Dedekind.
• Valuation.asIdeal_heightOneSpectrum: the underlying ideal is the centre ideal.

def Valuation.centerIdeal (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] (w : Valuation K Γ₀) (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) : Ideal R

The centre on R of a valuation w of K whose valuation ring contains R: the ideal of elements of R of positive valuation. It is prime (Valuation.isPrime_centerIdeal), and it is nonzero as soon as w is nontrivial and K is the fraction field of R (Valuation.centerIdeal_ne_bot).

Equations

• Valuation.centerIdeal R w hR = Ideal.comap ((algebraMap R K).codRestrict w.valuationSubring ⋯) (IsLocalRing.maximalIdeal ↥w.valuationSubring)

@[simp]

theorem Valuation.mem_centerIdeal {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] {w : Valuation K Γ₀} {r : R} {hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1} : r ∈ centerIdeal R w hR ↔ w ((algebraMap R K) r) < 1

An element belongs to the centre ideal exactly when its valuation is strictly below 1.

theorem Valuation.eq_one_of_notMem_centerIdeal {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] {w : Valuation K Γ₀} {r : R} (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) (hr : r ∉ centerIdeal R w hR) : w ((algebraMap R K) r) = 1

Off its centre, a valuation bounded by 1 on R takes the value 1.

theorem Valuation.isPrime_centerIdeal {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] {w : Valuation K Γ₀} (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) : (centerIdeal R w hR).IsPrime

The centre of a valuation bounded by 1 on R is a prime ideal of R.

theorem Valuation.centerIdeal_ne_bot {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] {w : Valuation K Γ₀} [IsFractionRing R K] [w.IsNontrivial] (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) : centerIdeal R w hR ≠ ⊥

The centre of a nontrivial valuation of the fraction field K of R is a nonzero ideal of R: an element of K of value below 1 is a fraction a / b whose numerator a is a nonzero element of the centre.

def Valuation.heightOneSpectrum (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [IsFractionRing R K] (w : Valuation K Γ₀) [w.IsNontrivial] (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) : IsDedekindDomain.HeightOneSpectrum R

The nonzero prime centre of a nontrivial valuation of K bounded by 1 on R, bundled as a HeightOneSpectrum R. This is a height one prime when R is a Dedekind domain.

Equations

• Valuation.heightOneSpectrum R w hR = { asIdeal := Valuation.centerIdeal R w hR, isPrime := ⋯, ne_bot := ⋯ }

@[simp]

theorem Valuation.asIdeal_heightOneSpectrum {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] {w : Valuation K Γ₀} [IsFractionRing R K] [w.IsNontrivial] (hR : ∀ (r : R), w ((algebraMap R K) r) ≤ 1) : (heightOneSpectrum R w hR).asIdeal = centerIdeal R w hR

The underlying ideal of heightOneSpectrum is the centre ideal.