Documentation

Mathlib.RingTheory.Valuation.Discrete.RankOne

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} [Ring R] (v : Valuation R Γ) [hv : v.IsRankOneDiscrete] :

(↑v).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ)

An order-preserving isomorphism between the ValueGroup₀ of a discrete valuation and ℤᵐ⁰. TODO: rename this into lowerCamelCase.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[simp]

theorem Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_apply {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [Ring R] (v : Valuation R Γ) [hv : v.IsRankOneDiscrete] (a : WithZero ↥(↑v).valueGroup) :

(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} [Ring 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} [Ring 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} [Ring 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} [Ring R] (v : Valuation R Γ) [hv : v.IsRankOneDiscrete] :

StrictMono ⇑(valueGroup₀_equiv_withZeroMulInt v)

@[instance_reducible]

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

A discrete valuation has rank one.

Equations

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

Instances For

theorem Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective {R : Type u_2} [Ring R] {v : Valuation R (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete] (hsurj : Function.Surjective ⇑v) (x : R) :

(valueGroup₀_equiv_withZeroMulInt v) (v.restrict x) = v x