Module

CompleteRangeRestriction.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValuationSubringUnits.CompleteRangeRestriction

8 declarations indexed from sourceView source ↗

Module documentation

Range restriction for complete discretely valued fields

This file specializes multiplicative-range restriction to CompleteDVF and transports residue finiteness, adic completeness, cyclicity, and discreteness.

Imports4

Imported by8

def

mrangeRestrict

L39 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict

Documentation

Restrict the chosen valuation of a complete DVF to its actual multiplicative range. This keeps the valuation ring, maximal ideal, and residue field unchanged while eliminating irrelevant ambient value-group elements.

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 mrangeRestrict (F : CompleteDVF.{u, v} K) :
    _root_.Valuation K (MonoidHom.mrange F.valuation.toMonoidWithZeroHom)

theorem

mrangeRestrict_apply

L48 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_apply

Documentation

The defining evaluation formula for mrangeRestrict is ((CompleteDVF.mrangeRestrict F) x : F.ValueGroup) = F.valuation 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 mrangeRestrict_apply (F : CompleteDVF.{u, v} K) (x : K) :
    ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F) x : F.ValueGroup) =
      F.valuation x

theorem

mrangeRestrict_residueField_finite

L55 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_residueField_finite

Documentation

The residue field remains finite after restricting the value group to the actual multiplicative range.

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 mrangeRestrict_residueField_finite
    (F : CompleteDVF.{u, v} K) [Finite F.residueField] :
    Finite (IsLocalRing.ResidueField
      (LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F).valuationSubring)

theorem

mrangeRestrict_isAdicComplete

L66 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_isAdicComplete

Documentation

The range-restricted valuation ring is adically complete because it is identified with the original complete-DVF valuation ring and the maximal ideal is preserved by that identification.

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 mrangeRestrict_isAdicComplete
    (F : CompleteDVF.{u, v} K) :
    IsAdicComplete
      (IsLocalRing.maximalIdeal
        (LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F).valuationSubring)
      (LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F).valuationSubring

theorem

mrangeRestrict_units_isCyclic

L135 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_units_isCyclic

Documentation

The actual multiplicative range of a complete-DVF valuation is generated by the image of a discrete valuation generator.

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 mrangeRestrict_units_isCyclic
    (F : CompleteDVF.{u, v} K) :
    IsCyclic (MonoidHom.mrange F.valuation.toMonoidWithZeroHom)ˣ

theorem

mrangeRestrict_isNontrivial

L214 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_isNontrivial

Documentation

The range-restricted valuation is nontrivial whenever the original complete-DVF valuation is nontrivial.

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 mrangeRestrict_isNontrivial
    (F : CompleteDVF.{u, v} K) :
    (LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F).IsNontrivial

theorem

mrangeRestrict_isRankOneDiscrete

L237 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_isRankOneDiscrete

Documentation

Restricting a complete-DVF valuation to its actual multiplicative range preserves rank-one discreteness.

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 mrangeRestrict_isRankOneDiscrete
    (F : CompleteDVF.{u, v} K) :
    (LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F).IsRankOneDiscrete

def

mrangeRestrict_rankOne

L260 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict_rankOne

Documentation

The range-restricted valuation is rank one as a valuation into its actual 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 mrangeRestrict_rankOne
    (F : CompleteDVF.{u, v} K) :
    (LocalFieldTheory.DiscreteValuationField.CompleteDVF.mrangeRestrict F).RankOne

Module documentation

Range restriction for complete discretely valued fields

Declarations