NYLL
Module

CyclicValueGroup.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValuationSubringUnits.CyclicValueGroup
6 declarations indexed from sourceView source ↗

Module documentation

Cyclic value groups and normalized uniformizers

This file supplies the ordered-group and rank-one facts used for actual multiplicative valuation ranges, together with normalized uniformizer results for ℤᵐ⁰-valued valuations.

Imports6
Imported by7

Declarations

def

rankOne

L44 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.rankOne
Documentation

A nontrivial ℤᵐ⁰-valued valuation is rank one via the standard strictly monotone embedding ℤᵐ⁰ -> ℝ≥0. This is kept as an explicit definition, not a global instance, so later finite-dimensional closedness arguments can opt in without changing typeclass search everywhere.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u x
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace WithZeroValuation
variable {R : Type u}
variable {Gamma : Type x} [LinearOrderedCommGroupWithZero Gamma]
Lean source · full declaration
def rankOne
    [Ring R]
    (v : _root_.Valuation R ℤᵐ⁰) [v.IsNontrivial] : v.RankOne where
  hom' :=
    (WithZeroMulInt.toNNReal (by norm_num : (2 : ℝ≥0) ≠ 0)).comp
      MonoidWithZeroHom.ValueGroup₀.embedding
  strictMono' :=
    (WithZeroMulInt.toNNReal_strictMono
      (by norm_num : (1 : ℝ≥0) < 2)).comp
        MonoidWithZeroHom.ValueGroup₀.embedding_strictMono
  exists_val_nontrivial :=
    _root_.Valuation.IsNontrivial.exists_val_nontrivial (v := v)
theorem

isCyclic_mulArchimedean

L62 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.isCyclic_mulArchimedean
Documentation

A cyclic linearly ordered commutative group is multiplicatively Archimedean. Mathlib supplies the valuation-theoretic equivalence RankOne <-> MulArchimedean; this lemma supplies the missing ordered-group input for actual valuation ranges whose unit group has already been proved cyclic.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u x
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace WithZeroValuation
variable {R : Type u}
variable {Gamma : Type x} [LinearOrderedCommGroupWithZero Gamma]
Lean source · statement
theorem isCyclic_mulArchimedean
    (G : Type*) [CommGroup G] [LinearOrder G] [IsOrderedMonoid G]
    [IsCyclic G] :
    MulArchimedean G
theorem

units_isCyclic_mulArchimedean

L108 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.units_isCyclic_mulArchimedean
Documentation

If the nonzero part of a value group is cyclic, the value group is multiplicatively Archimedean.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u x
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace WithZeroValuation
variable {R : Type u}
variable {Gamma : Type x} [LinearOrderedCommGroupWithZero Gamma]
Lean source · statement
theorem units_isCyclic_mulArchimedean
    (Gamma : Type x) [LinearOrderedCommGroupWithZero Gamma]
    [IsCyclic Gammaˣ] :
    MulArchimedean Gamma
def

rankOneOfUnitsIsCyclic

L120 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.rankOneOfUnitsIsCyclic
Documentation

A nontrivial valuation whose ambient value group has cyclic unit group is rank one. This is used only after restricting an abstract complete-DVF valuation to its actual range.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u x
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace WithZeroValuation
variable {R : Type u}
variable {Gamma : Type x} [LinearOrderedCommGroupWithZero Gamma]
Lean source · statement
def rankOneOfUnitsIsCyclic
    [Ring R]
    (v : _root_.Valuation R Gamma) [v.IsNontrivial] [IsCyclic Gammaˣ] :
    v.RankOne
theorem

isUniformizer_of_valuation_eq_exp_neg_one

L143 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.isUniformizer_of_valuation_eq_exp_neg_one
Documentation

For a valuation with values in the standard group ℤᵐ⁰, an element of value exp (-1) is a uniformizer.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u x
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace WithZeroValuation
variable {R : Type u}
variable {Gamma : Type x} [LinearOrderedCommGroupWithZero Gamma]
open LinearOrderedCommGroup
Lean source · statement
theorem isUniformizer_of_valuation_eq_exp_neg_one
    {K : Type u} [Field K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [v.IsRankOneDiscrete] (π : K)
    (hπ : v π = WithZero.exp (-1 : ℤ)) :
    v.IsUniformizer π
theorem

exists_valuationSubring_valuation_eq_exp_neg_one_of_surjective

L157 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.exists_valuationSubring_valuation_eq_exp_neg_one_of_surjective
Documentation

A surjective standard ℤᵐ⁰-valued valuation has a normalized uniformizer in its valuation subring.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u x
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace WithZeroValuation
variable {R : Type u}
variable {Gamma : Type x} [LinearOrderedCommGroupWithZero Gamma]
open LinearOrderedCommGroup
Lean source · statement
theorem exists_valuationSubring_valuation_eq_exp_neg_one_of_surjective
    {K : Type u} [Field K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (hv : Function.Surjective v) :
    ∃ π : v.valuationSubring,
      v (π : K) = WithZero.exp (-1 : ℤ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.