Module

StandardNormIndex.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.LubinTateApplication.StandardNormIndex

2 declarations indexed from sourceView source ↗

Module documentation

Norm indices for standard finite Lubin--Tate levels

Finite local reciprocity identifies the cardinality of the norm quotient of a finite abelian Galois extension with its field degree. Applied to a standard Lubin--Tate level over the canonical local-field package, this gives index (q - 1) * q ^ n.

Imports4

Imported by2

theorem

standardLubinTateNormSubgroup_index

L38 ↗

LubinTate.standardLubinTateNormSubgroup_index

Documentation

The norm subgroup of a standard level over the canonical local-field package has index equal to the standard Lubin--Tate degree.

Source context 7 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
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem standardLubinTateNormSubgroup_index
    {π : (standardLocalField K).valuationSubring}
    (hπ :
      (standardLocalField K).toCompleteDVF.valuation.IsUniformizer
        (π : K))
    (n : ℕ) :
    (standardLubinTateNormSubgroup hπ n).index =
      (Nat.card 𝓀[K] - 1) * Nat.card 𝓀[K] ^ n

theorem

standardLubinTateCanonicalNormSubgroup_index

L65 ↗

LubinTate.standardLubinTateCanonicalNormSubgroup_index