Discrete valuations have rank one #
Main Definitions and Results #
Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range: the generator of a discrete valuation inℤᵐ⁰that containsexp (-1)in its range is equal toexp (-1).Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_surjective: the generator of a surjective discrete valuation inℤᵐ⁰is equal toexp (-1).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}
[Ring R]
(v : Valuation R Γ)
[hv : v.IsRankOneDiscrete]
:
An order-preserving isomorphism between the ValueGroup₀ of a discrete valuation and ℤᵐ⁰.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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
@[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 ↥(MonoidWithZeroHom.valueGroup v))
:
(valueGroup₀_equiv_withZeroMulInt v) a = (WithZero.map' ↑(intEquivOfZPowersEqTop (generator' v)⁻¹ ⋯).symm) 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]
:
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 : ℤ)
:
theorem
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono
{Γ : Type u_1}
[LinearOrderedCommGroupWithZero Γ]
{R : Type u_2}
[Ring R]
(v : Valuation R Γ)
[hv : v.IsRankOneDiscrete]
:
@[implicit_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)
:
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 := ⋯ }
Instances For
theorem
Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range
{R : Type u_2}
[Ring R]
{v : Valuation R (WithZero (Multiplicative ℤ))}
[hv : v.IsRankOneDiscrete]
(hπ : WithZero.exp (-1) ∈ Set.range ⇑v)
:
The generator of a discrete valuation in ℤᵐ⁰ that contains exp (-1) in its range
is equal to exp (-1).
theorem
Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_surjective
{R : Type u_2}
[Ring R]
{v : Valuation R (WithZero (Multiplicative ℤ))}
[hv : v.IsRankOneDiscrete]
(hsurj : Function.Surjective ⇑v)
:
The generator of a surjective discrete valuation in ℤᵐ⁰ is equal to exp (-1).
@[deprecated Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_surjective (since := "2026-04-01")]
theorem
Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjective
{R : Type u_2}
[Ring R]
{v : Valuation R (WithZero (Multiplicative ℤ))}
[hv : v.IsRankOneDiscrete]
(hsurj : Function.Surjective ⇑v)
:
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)
: