NYLL
Module

FiniteParameters.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.FiniteParameters
12 declarations indexed from sourceView source ↗

Module documentation

Finite unit parameters for standard Lubin--Tate levels

For a local field F, the unit parameters visible at primitive level n + 1 are the valuation-ring units modulo the higher principal-unit subgroup U^(n + 1). This file records that quotient, chooses representatives, and computes its cardinality as

(q - 1) * q ^ n,

where q is the residue-field cardinality. The final declarations descend the standard Lubin--Tate action on the chosen primitive point to this finite parameter quotient.

Imports3
Imported by4

Declarations

def

standardLubinTateUnitParameter

L43 ↗
LubinTate.standardLubinTateUnitParameter
Documentation

The finite unit parameters visible on the primitive level-n + 1 standard Lubin--Tate torsion point.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTateUnitParameter
    (F : LocalField.{u, v} K) (n : ℕ) : Type u
instance

standardLubinTateUnitParameter_commGroup

L50 ↗
LubinTate.standardLubinTateUnitParameter_commGroup
Documentation

The finite unit parameter quotient carries its canonical commutative group structure.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
instance standardLubinTateUnitParameter_commGroup
    (F : LocalField.{u, v} K) (n : ℕ) :
    CommGroup (standardLubinTateUnitParameter F n)
def

standardLubinTateUnitParameterClass

L60 ↗
LubinTate.standardLubinTateUnitParameterClass
Documentation

The canonical class of a valuation-ring unit at primitive level n + 1.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTateUnitParameterClass
    (F : LocalField.{u, v} K) (n : ℕ) :
    F.valuationSubringˣ →* standardLubinTateUnitParameter F n
instance

standardLubinTateUnitParameter_finite

L67 ↗
LubinTate.standardLubinTateUnitParameter_finite
Documentation

The finite-level unit parameter space is finite.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
instance standardLubinTateUnitParameter_finite
    (F : LocalField.{u, v} K) (n : ℕ) :
    Finite (standardLubinTateUnitParameter F n)
def

standardLubinTateUnitParameterChosenRepresentative

L78 ↗
LubinTate.standardLubinTateUnitParameterChosenRepresentative
Documentation

A chosen valuation-ring unit representing a finite unit parameter.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTateUnitParameterChosenRepresentative
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : standardLubinTateUnitParameter F n) :
    F.valuationSubringˣ
theorem

standardLubinTateUnitParameterChosenRepresentative_spec

L88 ↗
LubinTate.standardLubinTateUnitParameterChosenRepresentative_spec
Documentation

The chosen representative has the prescribed quotient class.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateUnitParameterChosenRepresentative_spec
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : standardLubinTateUnitParameter F n) :
    standardLubinTateUnitParameterClass F n
        (standardLubinTateUnitParameterChosenRepresentative F n a) = a
theorem

standardLubinTateUnitParameterClass_eq_iff_div_mem

L99 ↗
LubinTate.standardLubinTateUnitParameterClass_eq_iff_div_mem
Documentation

Two valuation-ring units determine the same finite parameter exactly when their quotient belongs to U^(n + 1).

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateUnitParameterClass_eq_iff_div_mem
    (F : LocalField.{u, v} K) (n : ℕ)
    (a b : F.valuationSubringˣ) :
    standardLubinTateUnitParameterClass F n a =
        standardLubinTateUnitParameterClass F n b ↔
      a / b ∈
        CompleteDVF.higherPrincipalUnitGroup F.toCompleteDVF (n + 1)
theorem

standardLubinTateUnitParameter_natCard

L116 ↗
LubinTate.standardLubinTateUnitParameter_natCard
Documentation

The finite standard unit parameter set has cardinality (q - 1) * q ^ n.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateUnitParameter_natCard
    (F : LocalField.{u, v} K) (n : ℕ) :
    Nat.card (standardLubinTateUnitParameter F n) =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n
def

standardLubinTateUnitParameterRoot

L172 ↗
LubinTate.standardLubinTateUnitParameterRoot
Documentation

The primitive root attached to a finite unit parameter. A representative is chosen only to evaluate the primitive action; the theorem below shows that the value depends only on its quotient class.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
def standardLubinTateUnitParameterRoot
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) :
    SeparableClosure K
theorem

standardLubinTateUnitParameterRoot_eq_action_of_class_eq

L182 ↗
LubinTate.standardLubinTateUnitParameterRoot_eq_action_of_class_eq
Documentation

The parameter root can be evaluated using any representative of its quotient class.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateUnitParameterRoot_eq_action_of_class_eq
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n)
    (u : F.valuationSubringˣ)
    (hu : standardLubinTateUnitParameterClass F n u = a) :
    standardLubinTateUnitParameterRoot F hπ n a =
      standardLubinTatePrimitiveRootAction hπ n u
theorem

standardLubinTateUnitParameterRoot_class

L202 ↗
LubinTate.standardLubinTateUnitParameterRoot_class
Documentation

Evaluating at a canonical quotient class recovers the primitive action of the original valuation-ring unit.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateUnitParameterRoot_class
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (u : F.valuationSubringˣ) :
    standardLubinTateUnitParameterRoot F hπ n
        (standardLubinTateUnitParameterClass F n u) =
      standardLubinTatePrimitiveRootAction hπ n u
theorem

standardLubinTateUnitParameterRoot_isRoot

L214 ↗
LubinTate.standardLubinTateUnitParameterRoot_isRoot
Documentation

Every finite unit parameter gives a root of the primitive level polynomial.

Source context 7 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateUnitParameterRoot_isRoot
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) :
    ((standardLubinTatePrimitivePolynomialOverField F π n).map
      (algebraMap K (SeparableClosure K))).IsRoot
        (standardLubinTateUnitParameterRoot F hπ n a)

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