NYLL
Module

LevelFieldTower.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.LevelFieldTower
3 declarations indexed from sourceView source ↗

Module documentation

The tower of standard Lubin--Tate level fields

The primitive roots defining the standard finite levels are chosen independently in one separable closure. Exact torsion and normality show that the resulting simple fields nevertheless form an increasing tower.

Imports2
Imported by2

Declarations

def

standardLubinTatePrimitivePredecessorInLevelField

L34 ↗
LubinTate.standardLubinTatePrimitivePredecessorInLevelField
Documentation

The polynomial predecessor of the primitive level-n + 1 generator, regarded as an element of the level-n + 1 field itself.

Source context 6 commands

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

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

standardLubinTatePrimitivePredecessorInLevelField_coe

L47 ↗
LubinTate.standardLubinTatePrimitivePredecessorInLevelField_coe
Documentation

Coercing the internal predecessor to the separable closure gives the ambient polynomial predecessor used by the exact-torsion theorem.

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePrimitivePredecessorInLevelField_coe
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    {m n : ℕ} (hmn : m ≤ n) :
    (standardLubinTatePrimitivePredecessorInLevelField hπ hmn :
        SeparableClosure K) =
      (standardLubinTatePolynomialIterateOverSeparableClosure
        F π (n - m)).eval
          (chosenStandardLubinTatePrimitiveRoot hπ n)
theorem

standardLubinTateLevelField_mono

L81 ↗
LubinTate.standardLubinTateLevelField_mono
Documentation

The independently chosen standard Lubin--Tate level fields form an increasing tower inside the fixed separable closure.

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateLevelField_mono
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    {m n : ℕ} (hmn : m ≤ n) :
    standardLubinTateLevelField hπ m ≤
      standardLubinTateLevelField hπ n

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