NYLL
Module

StandardLocalField.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.StandardLocalField
21 declarations indexed from sourceView source ↗

Module documentation

The canonical local-field package for Lubin--Tate applications

A topology-first nonarchimedean local field carries the canonical valuation used by finite local reciprocity. This file packages that valuation as a LocalField and identifies its valuation ring and principal-unit filtration with the pre-existing 𝒪[K], principalUnits, and LocalFieldTheory.fieldPrincipalUnits interfaces.

Imports6
Imported by5

Declarations

def

standardLocalField

L42 ↗
LubinTate.standardLocalField
Documentation

The canonical complete discrete valuation on K, together with its finite residue field, packaged for the standard Lubin--Tate construction.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · full declaration
def standardLocalField : LocalField K where
  toCompleteDVF := LocalFieldTheory.localCompleteDVF K
  residueFinite := by
    change Finite 𝓀[K]
    infer_instance
theorem

standardLocalField_toCompleteDVF

L51 ↗
LubinTate.standardLocalField_toCompleteDVF
Documentation

Forgetting residue-field finiteness recovers the canonical complete-DVF package used by finite local reciprocity.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalField_toCompleteDVF :
    (standardLocalField K).toCompleteDVF =
      LocalFieldTheory.localCompleteDVF K
theorem

standardLocalField_valuation_eq

L58 ↗
LubinTate.standardLocalField_valuation_eq
Documentation

The valuation in the canonical local-field package is the valuation attached to the given valuative relation.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalField_valuation_eq :
    (standardLocalField K).valuation =
      ValuativeRel.valuation K
theorem

standardLocalField_residueField_natCard

L69 ↗
LubinTate.standardLocalField_residueField_natCard
Documentation

The residue field in the canonical package has the same finite cardinality as the topology-first residue field.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalField_residueField_natCard :
    Nat.card (standardLocalField K).residueField =
      Nat.card 𝓀[K]
def

standardLocalFieldIntegerEquiv

L76 ↗
LubinTate.standardLocalFieldIntegerEquiv
Documentation

Identity on underlying field elements identifies the topology-first integer ring with the valuation ring of the canonical package.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · full declaration
def standardLocalFieldIntegerEquiv :
    𝒪[K] ≃+* (standardLocalField K).valuationSubring where
  toFun x := ⟨x, by
    change (standardLocalField K).valuation (x : K) ≤ 1
    rw [standardLocalField_valuation_eq]
    exact x.property⟩
  invFun x := ⟨x, by
    change ValuativeRel.valuation K (x : K) ≤ 1
    rw [← standardLocalField_valuation_eq]
    exact x.property⟩
  left_inv := fun _ => rfl
  right_inv := fun _ => rfl
  map_add' := fun _ _ => rfl
  map_mul' := fun _ _ => rfl
theorem

standardLocalFieldIntegerEquiv_apply_coe

L94 ↗
LubinTate.standardLocalFieldIntegerEquiv_apply_coe
Documentation

The canonical integer-ring equivalence preserves the underlying field element.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldIntegerEquiv_apply_coe (x : 𝒪[K]) :
    (((standardLocalFieldIntegerEquiv K x :
      (standardLocalField K).valuationSubring)) : K) =
      (x : K)
theorem

standardLocalFieldIntegerEquiv_symm_apply_coe

L103 ↗
LubinTate.standardLocalFieldIntegerEquiv_symm_apply_coe
Documentation

The inverse canonical integer-ring equivalence preserves the underlying field element.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldIntegerEquiv_symm_apply_coe
    (x : (standardLocalField K).valuationSubring) :
    ((((standardLocalFieldIntegerEquiv K).symm x : 𝒪[K])) : K) =
      (x : K)
theorem

standardLocalFieldIntegerEquiv_map_maximalIdeal

L111 ↗
LubinTate.standardLocalFieldIntegerEquiv_map_maximalIdeal
Documentation

The canonical integer-ring equivalence sends the maximal ideal to the maximal ideal of the packaged valuation ring.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldIntegerEquiv_map_maximalIdeal :
    Ideal.map (standardLocalFieldIntegerEquiv K).toRingHom
        (𝓂[K] : Ideal 𝒪[K]) =
      (standardLocalField K).maximalIdeal
theorem

standardLocalFieldIntegerEquiv_map_maximalIdeal_pow

L137 ↗
LubinTate.standardLocalFieldIntegerEquiv_map_maximalIdeal_pow
Documentation

The canonical integer-ring equivalence preserves every maximal-ideal power.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldIntegerEquiv_map_maximalIdeal_pow (n : ℕ) :
    Ideal.map (standardLocalFieldIntegerEquiv K).toRingHom
        ((𝓂[K] : Ideal 𝒪[K]) ^ n) =
      (standardLocalField K).maximalIdeal ^ n
theorem

standardLocalFieldIntegerEquiv_mem_maximalIdeal_pow_iff

L146 ↗
LubinTate.standardLocalFieldIntegerEquiv_mem_maximalIdeal_pow_iff
Documentation

Membership in a maximal-ideal power is reflected by the canonical integer-ring equivalence.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldIntegerEquiv_mem_maximalIdeal_pow_iff
    (n : ℕ) (x : 𝒪[K]) :
    standardLocalFieldIntegerEquiv K x ∈
        (standardLocalField K).maximalIdeal ^ n ↔
      x ∈ (𝓂[K] : Ideal 𝒪[K]) ^ n
def

standardLocalFieldIntegerUnitsEquiv

L166 ↗
LubinTate.standardLocalFieldIntegerUnitsEquiv
Documentation

The induced multiplicative equivalence between the two valuation-ring unit groups.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def standardLocalFieldIntegerUnitsEquiv :
    𝒪[K]ˣ ≃*
      (standardLocalField K).valuationSubringˣ
theorem

standardLocalFieldIntegerUnitsEquiv_apply_coe

L174 ↗
LubinTate.standardLocalFieldIntegerUnitsEquiv_apply_coe
Documentation

The induced unit equivalence preserves the underlying field element.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldIntegerUnitsEquiv_apply_coe (u : 𝒪[K]ˣ) :
    ((((standardLocalFieldIntegerUnitsEquiv K u :
      (standardLocalField K).valuationSubringˣ) :
        (standardLocalField K).valuationSubring)) : K) =
      (((u : 𝒪[K]ˣ) : 𝒪[K]) : K)
theorem

standardLocalFieldIntegerUnitsEquiv_mem_higherPrincipalUnitGroup_iff

L183 ↗
LubinTate.standardLocalFieldIntegerUnitsEquiv_mem_higherPrincipalUnitGroup_iff
Documentation

Under the canonical unit equivalence, packaged higher principal units are exactly the topology-first principal units.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem
    standardLocalFieldIntegerUnitsEquiv_mem_higherPrincipalUnitGroup_iff
    (n : ℕ) (u : 𝒪[K]ˣ) :
    standardLocalFieldIntegerUnitsEquiv K u ∈
        higherPrincipalUnitGroup
          (standardLocalField K).toCompleteDVF n ↔
      u ∈ principalUnits K n
theorem

standardLocalFieldHigherPrincipalUnitGroup_map_eq_principalUnits

L204 ↗
LubinTate.standardLocalFieldHigherPrincipalUnitGroup_map_eq_principalUnits
Documentation

Mapping packaged higher principal units back through the canonical integer-unit equivalence gives the topology-first principal-unit subgroup.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldHigherPrincipalUnitGroup_map_eq_principalUnits
    (n : ℕ) :
    (higherPrincipalUnitGroup
        (standardLocalField K).toCompleteDVF n).map
        (standardLocalFieldIntegerUnitsEquiv K).symm.toMonoidHom =
      principalUnits K n
def

standardLocalFieldValuationUnitsToFieldUnits

L231 ↗
LubinTate.standardLocalFieldValuationUnitsToFieldUnits
Documentation

Inclusion of packaged valuation-ring units into field units, expressed through the canonical integer-ring identification.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def standardLocalFieldValuationUnitsToFieldUnits :
    (standardLocalField K).valuationSubringˣ →* Kˣ
theorem

standardLocalFieldValuationUnitsToFieldUnits_apply_coe

L239 ↗
LubinTate.standardLocalFieldValuationUnitsToFieldUnits_apply_coe
Documentation

The packaged valuation-unit inclusion preserves the underlying field element.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldValuationUnitsToFieldUnits_apply_coe
    (u : (standardLocalField K).valuationSubringˣ) :
    ((standardLocalFieldValuationUnitsToFieldUnits K u : Kˣ) : K) =
      (((u : (standardLocalField K).valuationSubringˣ) :
        (standardLocalField K).valuationSubring) : K)
theorem

standardLocalFieldHigherPrincipalUnitGroup_map_eq_fieldPrincipalUnits

L248 ↗
LubinTate.standardLocalFieldHigherPrincipalUnitGroup_map_eq_fieldPrincipalUnits
Documentation

The packaged higher principal-unit subgroup maps exactly to the topology-first field principal-unit subgroup.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldHigherPrincipalUnitGroup_map_eq_fieldPrincipalUnits
    (n : ℕ) :
    (higherPrincipalUnitGroup
        (standardLocalField K).toCompleteDVF n).map
        (standardLocalFieldValuationUnitsToFieldUnits K) =
      LocalFieldTheory.fieldPrincipalUnits K n
theorem

standardLocalFieldValuationUnit_mem_fieldPrincipalUnits_iff_mem_higher

L265 ↗
LubinTate.standardLocalFieldValuationUnit_mem_fieldPrincipalUnits_iff_mem_higher
Documentation

A packaged valuation-ring unit lies in U^n exactly when its field-unit image lies in LocalFieldTheory.fieldPrincipalUnits K n.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem
    standardLocalFieldValuationUnit_mem_fieldPrincipalUnits_iff_mem_higher
    (n : ℕ) (u : (standardLocalField K).valuationSubringˣ) :
    standardLocalFieldValuationUnitsToFieldUnits K u ∈
        LocalFieldTheory.fieldPrincipalUnits K n ↔
      u ∈ higherPrincipalUnitGroup
        (standardLocalField K).toCompleteDVF n
def

standardLocalFieldUniformizer

L286 ↗
LubinTate.standardLocalFieldUniformizer
Documentation

The canonical chosen uniformizer of 𝒪[K], transported to the valuation ring of the standard local-field package.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def standardLocalFieldUniformizer :
    (standardLocalField K).valuationSubring
theorem

standardLocalFieldUniformizer_coe

L294 ↗
LubinTate.standardLocalFieldUniformizer_coe
Documentation

The transported canonical uniformizer has the expected underlying field element.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldUniformizer_coe :
    ((standardLocalFieldUniformizer K :
      (standardLocalField K).valuationSubring) : K) =
      ((chosenIntegerRingUniformizer K : 𝒪[K]) : K)
theorem

standardLocalFieldUniformizer_isUniformizer

L302 ↗
LubinTate.standardLocalFieldUniformizer_isUniformizer
Documentation

The transported canonical prime element is a uniformizer for the valuation in the standard local-field package.

Source context 8 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLocalFieldUniformizer_isUniformizer :
    (standardLocalField K).valuation.IsUniformizer
      (standardLocalFieldUniformizer K : K)

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