Module

PrimitiveRoot.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.PrimitiveRoot

18 declarations indexed from sourceView source ↗

Module documentation

Primitive roots and standard Lubin--Tate level fields

For a local field F with uniformizer π, this file maps the primitive division polynomial from the valuation ring to the fraction field. Gauss's lemma transfers its Eisenstein irreducibility to the field. We also prove separability directly, choose a root in SeparableClosure K, and identify the degree of the simple extension generated by that root.

The separability argument works in both mixed and equal characteristic. It uses the identity

(f^[n])'(0) = π ^ n

for f(X) = X ^ q + π * X, together with the fact that q - 1 is nonzero in the base field.

Imports4

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.PrimitiveEisenstein
Mathlib.FieldTheory.IsSepClosed
Mathlib.RingTheory.Polynomial.GaussLemma
Mathlib.SetTheory.Cardinal.Finite

Imported by2

theorem

standardLubinTatePolynomial_derivative_eval_zero

L47 ↗

LubinTate.standardLubinTatePolynomial_derivative_eval_zero

Documentation

The derivative of the standard polynomial at zero is its linear coefficient.

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 standardLubinTatePolynomial_derivative_eval_zero
    (F : LocalField.{u, v} K) (π : F.valuationSubring) :
    (standardLubinTatePolynomial F π).derivative.eval 0 = π

theorem

standardLubinTatePolynomialIterate_derivative_eval_zero

L56 ↗

LubinTate.standardLubinTatePolynomialIterate_derivative_eval_zero

Documentation

The derivative at zero of the n-fold standard iterate is π ^ n.

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 standardLubinTatePolynomialIterate_derivative_eval_zero
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePolynomialIterate F π n).derivative.eval 0 =
      π ^ n

def

standardLubinTatePrimitivePolynomialOverField

L73 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField

Documentation

The primitive division polynomial after extending coefficients from the valuation ring to the base field.

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 standardLubinTatePrimitivePolynomialOverField
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    Polynomial K

theorem

standardLubinTatePrimitivePolynomialOverField_formula

L80 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField_formula

Documentation

The field-valued primitive polynomial has the expected formula.

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 standardLubinTatePrimitivePolynomialOverField_formula
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    standardLubinTatePrimitivePolynomialOverField F π n =
      (standardLubinTatePolynomialIterate F π n).map
          (algebraMap F.valuationSubring K) ^
        (Nat.card F.residueField - 1) +
      Polynomial.C (π : K)

theorem

standardLubinTatePrimitivePolynomialOverField_monic

L91 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField_monic

Documentation

The field-valued primitive polynomial is monic.

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 standardLubinTatePrimitivePolynomialOverField_monic
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePrimitivePolynomialOverField F π n).Monic

theorem

standardLubinTatePrimitivePolynomialOverField_natDegree

L98 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField_natDegree

Documentation

The field-valued primitive polynomial has degree (q - 1) * q ^ n.

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 standardLubinTatePrimitivePolynomialOverField_natDegree
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    (standardLubinTatePrimitivePolynomialOverField F π n).natDegree =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n

theorem

standardLubinTatePrimitivePolynomialOverField_irreducible

L109 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField_irreducible

Documentation

Gauss's lemma transfers Eisenstein irreducibility from the valuation ring to the base field.

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 standardLubinTatePrimitivePolynomialOverField_irreducible
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Irreducible (standardLubinTatePrimitivePolynomialOverField F π n)

theorem

residueFieldNatCard_sub_one_cast_ne_zero

L123 ↗

LubinTate.residueFieldNatCard_sub_one_cast_ne_zero

Documentation

The natural number q - 1 is nonzero in the local field.

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 residueFieldNatCard_sub_one_cast_ne_zero
    (F : LocalField.{u, v} K) :
    ((Nat.card F.residueField - 1 : ℕ) : K) ≠ 0

theorem

standardLubinTatePrimitivePolynomialOverField_derivative_ne_zero

L147 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField_derivative_ne_zero

Documentation

The field-valued primitive polynomial has nonzero derivative.

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 standardLubinTatePrimitivePolynomialOverField_derivative_ne_zero
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTatePrimitivePolynomialOverField F π n).derivative ≠ 0

theorem

standardLubinTatePrimitivePolynomialOverField_separable

L190 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField_separable

Documentation

The field-valued primitive polynomial is separable.

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 standardLubinTatePrimitivePolynomialOverField_separable
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTatePrimitivePolynomialOverField F π n).Separable

theorem

exists_standardLubinTatePrimitivePolynomialOverField_root

L199 ↗

LubinTate.exists_standardLubinTatePrimitivePolynomialOverField_root

Documentation

The primitive polynomial has a root in the chosen 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 exists_standardLubinTatePrimitivePolynomialOverField_root
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    ∃ x : SeparableClosure K,
      ((standardLubinTatePrimitivePolynomialOverField F π n).map
        (algebraMap K (SeparableClosure K))).IsRoot x

def

chosenStandardLubinTatePrimitiveRoot

L221 ↗

LubinTate.chosenStandardLubinTatePrimitiveRoot

Documentation

A chosen primitive level-n+1 root in SeparableClosure K.

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 chosenStandardLubinTatePrimitiveRoot
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    SeparableClosure K

theorem

chosenStandardLubinTatePrimitiveRoot_isRoot

L230 ↗

LubinTate.chosenStandardLubinTatePrimitiveRoot_isRoot

Documentation

The chosen primitive element is a root of the field-valued primitive polynomial.

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 chosenStandardLubinTatePrimitiveRoot_isRoot
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    ((standardLubinTatePrimitivePolynomialOverField F π n).map
      (algebraMap K (SeparableClosure K))).IsRoot
        (chosenStandardLubinTatePrimitiveRoot hπ n)

theorem

chosenStandardLubinTatePrimitiveRoot_isIntegral

L240 ↗

LubinTate.chosenStandardLubinTatePrimitiveRoot_isIntegral

Documentation

The chosen primitive root is integral over the base field.

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 chosenStandardLubinTatePrimitiveRoot_isIntegral
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsIntegral K (chosenStandardLubinTatePrimitiveRoot hπ n)

theorem

standardLubinTatePrimitivePolynomialOverField_eq_minpoly

L252 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField_eq_minpoly

Documentation

The field-valued primitive polynomial is the minimal polynomial of the chosen root.

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 standardLubinTatePrimitivePolynomialOverField_eq_minpoly
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    standardLubinTatePrimitivePolynomialOverField F π n =
      minpoly K (chosenStandardLubinTatePrimitiveRoot hπ n)

def

standardLubinTateLevelField

L267 ↗

LubinTate.standardLubinTateLevelField

Documentation

The simple extension generated by the chosen primitive root.

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 standardLubinTateLevelField
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IntermediateField K (SeparableClosure K)

theorem

standardLubinTateLevelField_finiteDimensional

L276 ↗

LubinTate.standardLubinTateLevelField_finiteDimensional

Documentation

Every standard Lubin--Tate level field is finite-dimensional over the base field.

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_finiteDimensional
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n)

theorem

standardLubinTateLevelField_finrank

L285 ↗

LubinTate.standardLubinTateLevelField_finrank

Documentation

The standard primitive level-n+1 extension has degree (q - 1) * q ^ n.

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_finrank
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    Module.finrank K (standardLubinTateLevelField hπ n) =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n

Module documentation

Primitive roots and standard Lubin--Tate level fields

Declarations