Module

LocalFieldRangeRestriction.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValuationSubringUnits.LocalFieldRangeRestriction

3 declarations indexed from sourceView source ↗

Module documentation

Multiplicative-range restriction for local fields

This file packages range restriction as a LocalField and exposes the properness and completeness of the resulting topology.

Imports1

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValuationSubringUnits.RangeRestrictedTopology

Imported by6

def

mrangeRestrict

L33 ↗

LocalFieldTheory.DiscreteValuationField.LocalField.mrangeRestrict

Documentation

A local-field package with its chosen valuation restricted to the actual multiplicative range.

Source context 7 commands

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

noncomputable section
universe u v
open scoped Valued
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]

Lean source · statement

def mrangeRestrict (F : LocalField.{u, v} K) :
    LocalField.{u, v} K

theorem

mrangeRestrict_properSpace

L45 ↗

LocalFieldTheory.DiscreteValuationField.LocalField.mrangeRestrict_properSpace

Documentation

The range-restricted topology attached to a local-field package is proper.

Source context 7 commands

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

noncomputable section
universe u v
open scoped Valued
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]

Lean source · full declaration

theorem mrangeRestrict_properSpace
    (F : LocalField.{u, v} K) :
    letI : Valued K
        (MonoidHom.mrange
          F.toCompleteDVF.valuation.toMonoidWithZeroHom) :=
      (CompleteDVF.mrangeRestrictValued F.toCompleteDVF)
    letI : NontriviallyNormedField K :=
      (CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF)
    ProperSpace K := by
  exact
    (CompleteDVF.mrangeRestrict_properSpace_of_residueField_finite F.toCompleteDVF)

theorem

mrangeRestrict_completeSpace

L58 ↗

LocalFieldTheory.DiscreteValuationField.LocalField.mrangeRestrict_completeSpace

Documentation

The range-restricted topology attached to a local-field package is complete.

Source context 7 commands

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

noncomputable section
universe u v
open scoped Valued
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]

Lean source · full declaration

theorem mrangeRestrict_completeSpace
    (F : LocalField.{u, v} K) :
    letI : Valued K
        (MonoidHom.mrange
          F.toCompleteDVF.valuation.toMonoidWithZeroHom) :=
      (CompleteDVF.mrangeRestrictValued F.toCompleteDVF)
    letI : NontriviallyNormedField K :=
      (CompleteDVF.mrangeRestrict_nontriviallyNormedField F.toCompleteDVF)
    CompleteSpace K := by
  exact
    (CompleteDVF.mrangeRestrict_completeSpace_of_residueField_finite F.toCompleteDVF)

Module documentation

Multiplicative-range restriction for local fields

Declarations

mrangeRestrict

mrangeRestrict_properSpace

mrangeRestrict_completeSpace