NYLL
Module

StandardNormSubgroupExact.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.LubinTateApplication.StandardNormSubgroupExact
5 declarations indexed from sourceView source ↗

Module documentation

The norm subgroup of a standard Lubin--Tate level

The changed-uniformizer comparison shows that every (n + 1)-st principal unit is a norm from the standard level n. Together with the known norm of the chosen uniformizer, this contains the canonical standard open subgroup in the norm subgroup. Their independently computed, nonzero indices are equal, so the containment is an equality.

Imports3
Imported by3

Declarations

theorem

standardLocalFieldValuationUnitsToFieldUnits_eq_standardLubinTateUnitFactorFieldUnit

L41 ↗
LubinTate.standardLocalFieldValuationUnitsToFieldUnits_eq_standardLubinTateUnitFactorFieldUnit
Documentation

The topology-first inclusion of packaged valuation-ring units agrees with the inclusion used in the changed-uniformizer norm calculation.

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalClassFieldTheory
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_eq_standardLubinTateUnitFactorFieldUnit
    (u : (standardLocalField K).valuationSubringˣ) :
    standardLocalFieldValuationUnitsToFieldUnits K u =
      standardLubinTateUnitFactorFieldUnit (standardLocalField K) u
theorem

standardLubinTateFieldPrincipalUnits_le_normSubgroup

L53 ↗
LubinTate.standardLubinTateFieldPrincipalUnits_le_normSubgroup
Documentation

Every (n + 1)-st field principal unit is a norm from the standard Lubin--Tate level n.

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalClassFieldTheory
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 standardLubinTateFieldPrincipalUnits_le_normSubgroup
    {π : (standardLocalField K).valuationSubring}
    (hπ :
      (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
        (π : K))
    (n : ℕ) :
    LocalFieldTheory.fieldPrincipalUnits K (n + 1) ≤
      standardLubinTateNormSubgroup hπ n
theorem

standardLubinTateUniformizerPrincipalSubgroup_le_normSubgroup

L73 ↗
LubinTate.standardLubinTateUniformizerPrincipalSubgroup_le_normSubgroup
Documentation

The subgroup generated by the chosen uniformizer and U_K^(n+1) is contained in the norm subgroup of the standard level n.

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalClassFieldTheory
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 standardLubinTateUniformizerPrincipalSubgroup_le_normSubgroup
    {π : (standardLocalField K).valuationSubring}
    (hπ :
      (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
        (π : K))
    (n : ℕ) :
    LocalFieldTheory.uniformizerPrincipalSubgroup K
        (standardLubinTateBaseUniformizerUnit hπ) 1 (n + 1) ≤
      standardLubinTateNormSubgroup hπ n
theorem

standardLubinTateCanonicalUniformizerPrincipalSubgroup_eq_normSubgroup

L92 ↗
LubinTate.standardLubinTateCanonicalUniformizerPrincipalSubgroup_eq_normSubgroup
Documentation

For the canonical local-field package, the norm subgroup of standard level n is exactly the subgroup generated by the canonical uniformizer and U_K^(n+1).

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalClassFieldTheory
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
    standardLubinTateCanonicalUniformizerPrincipalSubgroup_eq_normSubgroup
    (n : ℕ) :
    LocalFieldTheory.uniformizerPrincipalSubgroup K
        (standardLubinTateBaseUniformizerUnit
          (standardLocalFieldUniformizer_isUniformizer K))
        1 (n + 1) =
      standardLubinTateNormSubgroup
        (standardLocalFieldUniformizer_isUniformizer K) n
theorem

standardLubinTateCanonicalNormSubgroup_eq_normalizedUniformizerPrincipalSubgroup

L119 ↗
LubinTate.standardLubinTateCanonicalNormSubgroup_eq_normalizedUniformizerPrincipalSubgroup
Documentation

With the normalized positive-valuation convention, the same norm subgroup is generated by the inverse canonical uniformizer and U_K^(n+1).

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalClassFieldTheory
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
    standardLubinTateCanonicalNormSubgroup_eq_normalizedUniformizerPrincipalSubgroup
    (n : ℕ) :
    standardLubinTateNormSubgroup
        (standardLocalFieldUniformizer_isUniformizer K) n =
      LocalFieldTheory.uniformizerPrincipalSubgroup K
        (inverseIntegerRingUniformizerFieldUnit K) 1 (n + 1)

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