NYLL
Module

RangeRestriction.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValuationSubringUnits.RangeRestriction
8 declarations indexed from sourceView source ↗

Module documentation

Restricting a valuation to its multiplicative range

The restricted valuation has the same valuation ring, maximal ideal, and residue field as the original valuation.

Imports1
Imported by7

Declarations

def

mrangeRestrict

L42 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.mrangeRestrict
Documentation

Restrict a valuation's codomain to its actual multiplicative range.

This removes irrelevant ambient value-group elements. It is the value-group normalization needed before finite-dimensional closedness can be used for an abstract chosen local-field valuation.

Source context 11 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]
section Field
variable [Field R]
Lean source · full declaration
def mrangeRestrict (v : _root_.Valuation R Gamma) :
    _root_.Valuation R (MonoidHom.mrange v.toMonoidWithZeroHom) where
  toFun r := ⟨v r, ⟨r, rfl⟩⟩
  map_one' := by
    ext
    exact map_one v
  map_zero' := by
    ext
    exact map_zero v
  map_mul' x y := by
    ext
    exact map_mul v x y
  map_add_le_max' x y := by
    rw [← Subtype.coe_le_coe]
    exact map_add_le_max v x y
theorem

mrangeRestrict_apply

L60 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.mrangeRestrict_apply
Documentation

The defining evaluation formula for mrangeRestrict is (mrangeRestrict v x : Gamma) = v x.

Source context 11 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]
section Field
variable [Field R]
Lean source · statement
theorem mrangeRestrict_apply (v : _root_.Valuation R Gamma) (x : R) :
    (mrangeRestrict v x : Gamma) = v x
theorem

mem_mrangeRestrict_valuationSubring_iff

L66 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.mem_mrangeRestrict_valuationSubring_iff
Documentation

Passing to the actual multiplicative range does not change the valuation subring predicate.

Source context 11 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]
section Field
variable [Field R]
Lean source · statement
theorem mem_mrangeRestrict_valuationSubring_iff
    (v : _root_.Valuation R Gamma) (x : R) :
    x ∈ (mrangeRestrict v).valuationSubring ↔ x ∈ v.valuationSubring
def

valuationSubringEquivMrangeRestrict

L76 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.valuationSubringEquivMrangeRestrict
Documentation

The valuation subring is unchanged after restricting the value group to the actual multiplicative range.

Source context 11 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]
section Field
variable [Field R]
Lean source · full declaration
def valuationSubringEquivMrangeRestrict
    (v : _root_.Valuation R Gamma) :
    v.valuationSubring ≃+* (mrangeRestrict v).valuationSubring where
  toFun x :=
    ⟨x, (mem_mrangeRestrict_valuationSubring_iff v x).2 x.2⟩
  invFun x :=
    ⟨x, (mem_mrangeRestrict_valuationSubring_iff v x).1 x.2⟩
  left_inv x := by ext; rfl
  right_inv x := by ext; rfl
  map_mul' x y := by ext; rfl
  map_add' x y := by ext; rfl
theorem

valuationSubringEquivMrangeRestrict_apply_coe

L93 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.valuationSubringEquivMrangeRestrict_apply_coe
Documentation

Establishes the identity ((valuationSubringEquivMrangeRestrict v x : (mrangeRestrict v).valuationSubring) : R) = x.

Source context 11 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]
section Field
variable [Field R]
Lean source · statement
theorem valuationSubringEquivMrangeRestrict_apply_coe
    (v : _root_.Valuation R Gamma) (x : v.valuationSubring) :
    ((valuationSubringEquivMrangeRestrict v x :
      (mrangeRestrict v).valuationSubring) : R) = x
theorem

valuationSubringEquivMrangeRestrict_mem_maximalIdeal_iff

L103 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.valuationSubringEquivMrangeRestrict_mem_maximalIdeal_iff
Documentation

The valuation-subring equivalence induced by range restriction preserves the maximal ideal.

Source context 12 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]
section Field
variable [Field R]
variable {K : Type u} [Field K]
Lean source · statement
theorem valuationSubringEquivMrangeRestrict_mem_maximalIdeal_iff
    (v : _root_.Valuation K Gamma) (x : v.valuationSubring) :
    valuationSubringEquivMrangeRestrict v x ∈
        IsLocalRing.maximalIdeal (mrangeRestrict v).valuationSubring ↔
      x ∈ IsLocalRing.maximalIdeal v.valuationSubring
theorem

valuationSubringEquivMrangeRestrict_map_maximalIdeal

L119 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.valuationSubringEquivMrangeRestrict_map_maximalIdeal
Documentation

Establishes the identity (IsLocalRing.maximalIdeal v.valuationSubring).map (valuationSubringEquivMrangeRestrict v : v.valuationSubring →+* (mrangeRestrict v).valuationSubring) = IsLocalRing.maximalIdeal (mrangeRestrict v).valuationSubring.

Source context 12 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]
section Field
variable [Field R]
variable {K : Type u} [Field K]
Lean source · statement
theorem valuationSubringEquivMrangeRestrict_map_maximalIdeal
    (v : _root_.Valuation K Gamma) :
    (IsLocalRing.maximalIdeal v.valuationSubring).map
        (valuationSubringEquivMrangeRestrict v :
          v.valuationSubring →+* (mrangeRestrict v).valuationSubring) =
      IsLocalRing.maximalIdeal (mrangeRestrict v).valuationSubring
def

residueFieldEquivMrangeRestrict

L141 ↗
LocalFieldTheory.DiscreteValuationField.WithZeroValuation.residueFieldEquivMrangeRestrict
Documentation

Restricting a valuation to its actual multiplicative range induces the same residue field.

Source context 12 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]
section Field
variable [Field R]
variable {K : Type u} [Field K]
Lean source · statement
def residueFieldEquivMrangeRestrict
    (v : _root_.Valuation K Gamma) :
    IsLocalRing.ResidueField v.valuationSubring ≃+*
      IsLocalRing.ResidueField (mrangeRestrict v).valuationSubring

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