Discrete valuations have rank one #
Main Definitions and Results #
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt: the order-preserving isomorphism between theValueGroup₀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]
:
An order-preserving isomorphism between the ValueGroup₀ of a discrete valuation and ℤᵐ⁰.
Instances For
@[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]
:
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)
:
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.