NYLL
Module

NormSubgroup.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.NormSubgroup
7 declarations indexed from sourceView source ↗

Module documentation

The norm subgroup of a standard Lubin--Tate level

This file introduces the local norm subgroup attached to a standard finite Lubin--Tate level. The norm identity for the negative primitive generator shows that the chosen base uniformizer is an actual norm. Consequently its entire cyclic subgroup of integral powers lies in the norm subgroup.

The higher-principal-unit contribution is intentionally left to the later norm calculation.

Imports2
Imported by4

Declarations

def

standardLubinTateNormSubgroup

L36 ↗
LubinTate.standardLubinTateNormSubgroup
Documentation

The local norm subgroup attached to a standard finite Lubin--Tate level.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTateNormSubgroup
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) : Subgroup Kˣ
def

standardLubinTateBaseUniformizerUnit

L44 ↗
LubinTate.standardLubinTateBaseUniformizerUnit
Documentation

The chosen base uniformizer, regarded as a nonzero field unit.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTateBaseUniformizerUnit
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    Kˣ
theorem

standardLubinTateBaseUniformizerUnit_coe

L53 ↗
LubinTate.standardLubinTateBaseUniformizerUnit_coe
Documentation

The chosen uniformizer unit has the expected underlying field element.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateBaseUniformizerUnit_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    (standardLubinTateBaseUniformizerUnit hπ : K) = (π : K)
theorem

standardLubinTateBaseUniformizerUnit_mem_normSubgroup

L61 ↗
LubinTate.standardLubinTateBaseUniformizerUnit_mem_normSubgroup
Documentation

The chosen base uniformizer is an actual norm from every standard finite level.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateBaseUniformizerUnit_mem_normSubgroup
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    standardLubinTateBaseUniformizerUnit hπ ∈
      standardLubinTateNormSubgroup hπ n
theorem

standardLubinTateBaseUniformizerUnit_inv_mem_normSubgroup

L92 ↗
LubinTate.standardLubinTateBaseUniformizerUnit_inv_mem_normSubgroup
Documentation

The inverse uniformizer is also a norm, for conventions that choose the inverse generator of the valuation factor.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateBaseUniformizerUnit_inv_mem_normSubgroup
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    (standardLubinTateBaseUniformizerUnit hπ)⁻¹ ∈
      standardLubinTateNormSubgroup hπ n
theorem

standardLubinTateBaseUniformizerUnit_zpowers_le_normSubgroup

L102 ↗
LubinTate.standardLubinTateBaseUniformizerUnit_zpowers_le_normSubgroup
Documentation

Every integral power of the chosen base uniformizer is a norm.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateBaseUniformizerUnit_zpowers_le_normSubgroup
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    Subgroup.zpowers (standardLubinTateBaseUniformizerUnit hπ) ≤
      standardLubinTateNormSubgroup hπ n
theorem

standardLubinTateBaseUniformizerUnit_inv_zpowers_le_normSubgroup

L113 ↗
LubinTate.standardLubinTateBaseUniformizerUnit_inv_zpowers_le_normSubgroup
Documentation

The same cyclic norm-subgroup inclusion using the inverse-uniformizer convention.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateBaseUniformizerUnit_inv_zpowers_le_normSubgroup
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    Subgroup.zpowers ((standardLubinTateBaseUniformizerUnit hπ)⁻¹) ≤
      standardLubinTateNormSubgroup hπ n

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