Values of a valuation whose maximal ideal is principal

Let v be a valuation on a field F whose valuation ring has maximal ideal generated by ϖ. Every value of v in (v ϖ ^ n, 1] is a power v ϖ ^ j with j < n, so when ϖ ≠ 0 there are exactly n such values. No discreteness of v is assumed: the value group may have higher rank.

Main results

• Valuation.map_lt_one_of_maximalIdeal_eq_span_of_dvd: a multiple of ϖ in the valuation ring has value less than 1.
• Valuation.map_lt_one_of_maximalIdeal_eq_span: the generator ϖ has v ϖ < 1.
• Valuation.exists_pow_eq_of_pow_lt_of_le_one: a value of v in (v ϖ ^ n, 1] is v ϖ ^ j for some j < n.
• Valuation.natCard_range_inter_Ioc_pow: if ϖ ≠ 0, there are exactly n values of v in (v ϖ ^ n, 1].

theorem Valuation.map_lt_one_of_maximalIdeal_eq_span_of_dvd {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {ϖ : ↥v.valuationSubring} (hϖ : IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {ϖ}) {z : ↥v.valuationSubring} (hz : ϖ ∣ z) : v ↑z < 1

An element of the valuation ring divisible by a generator ϖ of the maximal ideal has value less than 1.

theorem Valuation.map_lt_one_of_maximalIdeal_eq_span {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {ϖ : ↥v.valuationSubring} (hϖ : IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {ϖ}) : v ↑ϖ < 1

A generator of the maximal ideal of the valuation ring has value less than 1.

theorem Valuation.exists_pow_eq_of_pow_lt_of_le_one {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {ϖ : ↥v.valuationSubring} (hϖ : IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {ϖ}) (n : ℕ) {z : F} : v ↑ϖ ^ n < v z → v z ≤ 1 → ∃ j < n, v ↑ϖ ^ j = v z

When the maximal ideal of the valuation ring is generated by ϖ, the values of v in (v ϖ ^ n, 1] are the powers v ϖ ^ j with j < n.

theorem Valuation.natCard_range_inter_Ioc_pow {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {ϖ : ↥v.valuationSubring} (hϖ : IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {ϖ}) (hϖ0 : ↑ϖ ≠ 0) (n : ℕ) : Nat.card ↑(Set.range ⇑v ∩ Set.Ioc (v ↑ϖ ^ n) 1) = n

When the maximal ideal of the valuation ring is generated by ϖ ≠ 0, there are exactly n values of v in (v ϖ ^ n, 1].