Discrete valuations have rank one

Main Definitions and Results

• Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt : the order-preserving isomorphism between the ValueGroup₀ of a discrete valuation and ℤᵐ⁰.
• Valuation.IsRankOneDiscrete.rankOne : a discrete valuation has rank one.

Tags

valuation, discrete, rank one

noncomputable def Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [CommRing R] (v : Valuation R Γ) [hv : v.IsRankOneDiscrete] : MonoidWithZeroHom.ValueGroup₀ v ≃* WithZero (Multiplicative ℤ)

An order-preserving isomorphism between the ValueGroup₀ of a discrete valuation and ℤᵐ⁰.

Equations

• Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v = MulEquiv.withZero (intEquivOfZPowersEqTop (Valuation.IsRankOneDiscrete.generator' v)⁻¹ ⋯).symm

@[simp]

theorem Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [CommRing R] (v : Valuation R Γ) [hv : v.IsRankOneDiscrete] (a : WithZero ↥(MonoidWithZeroHom.valueGroup v)) : (valueGroup₀_equiv_withZeroMulInt v) a = (WithZero.map' ↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm) a

@[simp]

theorem Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_symm_apply {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [CommRing R] (v : Valuation R Γ) [hv : v.IsRankOneDiscrete] (a : WithZero (Multiplicative ℤ)) : (valueGroup₀_equiv_withZeroMulInt v).symm a = (WithZero.map' ↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯)) a

theorem Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zero {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [CommRing R] (v : Valuation R Γ) [hv : v.IsRankOneDiscrete] : (valueGroup₀_equiv_withZeroMulInt v) 0 = 0

theorem Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply_zpow {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [CommRing R] (v : Valuation R Γ) [hv : v.IsRankOneDiscrete] (k : ℤ) : (valueGroup₀_equiv_withZeroMulInt v) (↑(generator' v) ^ k) = WithZero.exp (-k)

theorem Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [CommRing R] (v : Valuation R Γ) [hv : v.IsRankOneDiscrete] : StrictMono ⇑(valueGroup₀_equiv_withZeroMulInt v)

theorem Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjective {K : Type u_2} [Field K] {v : Valuation K (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete] (hsurj : Function.Surjective ⇑v) : generator v = Units.mk0 (WithZero.exp (-1)) generator_eq_neg_exp_one_of_surjective._proof_1

theorem Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective {K : Type u_2} [Field K] {v : Valuation K (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete] (hsurj : Function.Surjective ⇑v) (x : K) : (valueGroup₀_equiv_withZeroMulInt v) (v.restrict x) = v x

@[implicit_reducible]

noncomputable def Valuation.IsRankOneDiscrete.rankOne {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] (v : Valuation K Γ) [hv : v.IsRankOneDiscrete] {e : NNReal} (he : 1 < e) : v.RankOne

A discrete valuation has rank one.

Equations

• Valuation.IsRankOneDiscrete.rankOne v he = { hom' := (WithZeroMulInt.toNNReal ⋯).comp ↑(Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v), strictMono' := ⋯, toIsNontrivial := ⋯ }