Module

PrimitiveEisenstein.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.PrimitiveEisenstein

6 declarations indexed from sourceView source ↗

Module documentation

Eisenstein property of the standard primitive division polynomials

Let F be a local field, let π be a uniformizer, and put

f(X) = X ^ q + π * X,

where q is the cardinality of the residue field. Reduction modulo the maximal ideal sends the n-fold compositional iterate of f to X ^ (q ^ n). Consequently, the primitive quotient polynomial

Qₙ(X) = (f^[n](X)) ^ (q - 1) + π

reduces to its leading monomial. Its constant coefficient is the uniformizer itself, so Qₙ is Eisenstein at the maximal ideal and hence irreducible over the valuation ring.

The argument is independent of the characteristic of F.

Imports2

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.DivisionPolynomial
Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Imported by2

theorem

standardLubinTatePolynomial_map_residue

L46 ↗

LubinTate.standardLubinTatePolynomial_map_residue

Documentation

Reduction modulo the maximal ideal sends the standard Lubin--Tate polynomial to X ^ q.

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_map_residue
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) :
    (standardLubinTatePolynomial F π).map F.residueMap =
      Polynomial.X ^ Nat.card F.residueField

theorem

standardLubinTatePolynomialIterate_map_residue

L56 ↗

LubinTate.standardLubinTatePolynomialIterate_map_residue

Documentation

Reduction modulo the maximal ideal sends the n-fold standard iterate to X ^ (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 standardLubinTatePolynomialIterate_map_residue
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTatePolynomialIterate F π n).map F.residueMap =
      Polynomial.X ^ (Nat.card F.residueField ^ n)

theorem

standardLubinTatePrimitivePolynomial_map_residue

L73 ↗

LubinTate.standardLubinTatePrimitivePolynomial_map_residue

Documentation

Reduction modulo the maximal ideal sends the primitive quotient polynomial to its leading monomial.

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 standardLubinTatePrimitivePolynomial_map_residue
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTatePrimitivePolynomial F π n).map F.residueMap =
      Polynomial.X ^
        ((Nat.card F.residueField - 1) *
          Nat.card F.residueField ^ n)

theorem

standardLubinTatePrimitivePolynomial_isEisensteinAt

L87 ↗

LubinTate.standardLubinTatePrimitivePolynomial_isEisensteinAt

Documentation

The standard primitive quotient polynomial is Eisenstein at the maximal ideal of the valuation ring.

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

theorem

standardLubinTatePrimitivePolynomial_isPrimitive

L119 ↗

LubinTate.standardLubinTatePrimitivePolynomial_isPrimitive

Documentation

Every standard primitive quotient polynomial is primitive.

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

theorem

standardLubinTatePrimitivePolynomial_irreducible

L126 ↗

LubinTate.standardLubinTatePrimitivePolynomial_irreducible

Documentation

The standard primitive quotient polynomial is irreducible by Eisenstein's criterion.

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

Module documentation

Eisenstein property of the standard primitive division polynomials

Declarations

standardLubinTatePolynomial_map_residue

standardLubinTatePolynomialIterate_map_residue

standardLubinTatePrimitivePolynomial_map_residue

standardLubinTatePrimitivePolynomial_isEisensteinAt

standardLubinTatePrimitivePolynomial_isPrimitive

standardLubinTatePrimitivePolynomial_irreducible