NYLL
Module

UniformizerIntegerValuation.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValuationSubringUnits.UniformizerIntegerValuation
12 declarations indexed from sourceView source ↗

Module documentation

Integer valuations from complete-DVF uniformizers

A chosen uniformizer determines the exponent of every nonzero field value and therefore an integer-valued multiplicative valuation on field units.

Imports2
Imported by6

Declarations

def

fieldUnitValueUnit

L35 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.fieldUnitValueUnit
Documentation

The nonzero value of a field unit, regarded as a unit of the ambient value group.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
def fieldUnitValueUnit
    (F : CompleteDVF.{u, v} K) (x : Kˣ) : F.ValueGroupˣ
theorem

fieldUnitValueUnit_one

L42 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.fieldUnitValueUnit_one
Documentation

Establishes the identity (CompleteDVF.fieldUnitValueUnit F) (1 : Kˣ) = 1.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem fieldUnitValueUnit_one (F : CompleteDVF.{u, v} K) :
    (fieldUnitValueUnit F) (1 : Kˣ) = 1
theorem

fieldUnitValueUnit_mul

L52 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.fieldUnitValueUnit_mul
Documentation

fieldUnitValueUnit satisfies the multiplication formula (CompleteDVF.fieldUnitValueUnit F) (x * y) = (CompleteDVF.fieldUnitValueUnit F) x * (CompleteDVF.fieldUnitValueUnit F) y.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem fieldUnitValueUnit_mul
    (F : CompleteDVF.{u, v} K) (x y : Kˣ) :
    (fieldUnitValueUnit F) (x * y) =
      (fieldUnitValueUnit F) x * (fieldUnitValueUnit F) y
def

uniformizerValueUnit

L61 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.uniformizerValueUnit
Documentation

The value of a chosen uniformizer, regarded as a unit of the ambient value group.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
def uniformizerValueUnit
    (F : CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    F.ValueGroupˣ
theorem

exists_uniformizerValueUnit_zpow_eq_fieldUnitValueUnit

L69 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.exists_uniformizerValueUnit_zpow_eq_fieldUnitValueUnit
Documentation

The value of every field unit is an integral power of the value of a chosen uniformizer.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem exists_uniformizerValueUnit_zpow_eq_fieldUnitValueUnit
    (F : CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    ∃ n : ℤ,
      (uniformizerValueUnit F) hπ ^ n = (fieldUnitValueUnit F) x
theorem

uniformizerValueUnit_zpow_inj

L89 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.uniformizerValueUnit_zpow_inj
Documentation

Integral powers of the value of a uniformizer are indexed uniquely.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem uniformizerValueUnit_zpow_inj
    (F : CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {m n : ℤ} :
    (uniformizerValueUnit F) hπ ^ m =
        (uniformizerValueUnit F) hπ ^ n ↔
      m = n
def

uniformizerValueExponent

L110 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.uniformizerValueExponent
Documentation

The integer exponent of the value of a field unit with respect to a chosen uniformizer.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
def uniformizerValueExponent
    (F : CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) : ℤ
theorem

uniformizerValueUnit_zpow_uniformizerValueExponent_eq_fieldUnitValueUnit

L118 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.uniformizerValueUnit_zpow_uniformizerValueExponent_eq_fieldUnitValueUnit
Documentation

The chosen exponent really recovers the value of the field unit.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem uniformizerValueUnit_zpow_uniformizerValueExponent_eq_fieldUnitValueUnit
    (F : CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    (uniformizerValueUnit F) hπ ^
        (uniformizerValueExponent F) hπ x =
      (fieldUnitValueUnit F) x
def

multiplicativeIntegerValuationOfUniformizer

L131 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.multiplicativeIntegerValuationOfUniformizer
Documentation

The integer-valued multiplicative valuation on Kˣ attached to a chosen uniformizer of an arbitrary complete DVF. Its value is the exponent of the field-unit value as a power of the uniformizer value.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · full declaration
def multiplicativeIntegerValuationOfUniformizer
    (F : CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    MultiplicativeIntegerValuation Kˣ where
  val x := (uniformizerValueExponent F) hπ x
  map_one := by
    apply ((uniformizerValueUnit_zpow_inj F) hπ).1
    rw [(uniformizerValueUnit_zpow_uniformizerValueExponent_eq_fieldUnitValueUnit F)]
    simp
  map_mul x y := by
    apply ((uniformizerValueUnit_zpow_inj F) hπ).1
    calc
      (uniformizerValueUnit F) hπ ^
          (uniformizerValueExponent F) hπ (x * y) =
          (fieldUnitValueUnit F) (x * y) := by
        rw [(uniformizerValueUnit_zpow_uniformizerValueExponent_eq_fieldUnitValueUnit F)]
      _ = (fieldUnitValueUnit F) x * (fieldUnitValueUnit F) y := by
        rw [(fieldUnitValueUnit_mul F)]
      _ =
          (uniformizerValueUnit F) hπ ^ (uniformizerValueExponent F) hπ x *
            (uniformizerValueUnit F) hπ ^ (uniformizerValueExponent F) hπ y := by
        rw [(uniformizerValueUnit_zpow_uniformizerValueExponent_eq_fieldUnitValueUnit F),
          (uniformizerValueUnit_zpow_uniformizerValueExponent_eq_fieldUnitValueUnit F)]
      _ =
          (uniformizerValueUnit F) hπ ^
            ((uniformizerValueExponent F) hπ x +
              (uniformizerValueExponent F) hπ y) := by
        rw [← zpow_add]
theorem

multiplicativeIntegerValuationOfUniformizer_val

L165 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.multiplicativeIntegerValuationOfUniformizer_val
Documentation

Establishes the identity ((CompleteDVF.multiplicativeIntegerValuationOfUniformizer F) hπ).val x = (CompleteDVF.uniformizerValueExponent F) hπ x.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem multiplicativeIntegerValuationOfUniformizer_val
    (F : CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    (x : Kˣ) :
    ((multiplicativeIntegerValuationOfUniformizer F) hπ).val x =
      (uniformizerValueExponent F) hπ x
theorem

multiplicativeIntegerValuationOfUniformizer_isUniformizer

L174 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.multiplicativeIntegerValuationOfUniformizer_isUniformizer
Documentation

The chosen uniformizer has integer value one for the attached valuation.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem multiplicativeIntegerValuationOfUniformizer_isUniformizer
    (F : CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    ((multiplicativeIntegerValuationOfUniformizer F) hπ).IsUniformizer
      (Units.mk0 (π : K) hπ.ne_zero)
theorem

multiplicativeIntegerValuationOfUniformizer_zeroSubgroup_eq_unitGroup

L187 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.multiplicativeIntegerValuationOfUniformizer_zeroSubgroup_eq_unitGroup
Documentation

The zero subgroup of the attached integer-valued valuation is exactly the valuation-subring unit group.

Source context 8 commands

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

noncomputable section
universe u v
open WithZero
open scoped NNReal Valued WithZero
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem multiplicativeIntegerValuationOfUniformizer_zeroSubgroup_eq_unitGroup
    (F : CompleteDVF.{u, v} K)
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K)) :
    ((multiplicativeIntegerValuationOfUniformizer F) hπ).zeroSubgroup =
      F.valuation.valuationSubring.unitGroup

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