NYLL
Module

PrimitiveIrreducible.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.PrimitiveIrreducible
23 declarations indexed from sourceView source ↗

Module documentation

The uniformizer norm identity: irreducibility of the equal-characteristic primitive polynomial

The primitive level-n+1 polynomial is lifted from κ((T)) to κ[[T]]. Modulo T this lift is the single monomial Y ^ ((q - 1) * q ^ n), while its constant coefficient is exactly T. It is therefore Eisenstein at (T), and Gauss's lemma gives irreducibility over κ((T)).

Imports4
Imported by5

Declarations

def

equalCharacteristicLubinTateIntegralPiPolynomial

L38 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomial
Documentation

The integral lift Y ^ q + T * Y of the equal-characteristic Lubin--Tate polynomial.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTateIntegralPiPolynomial
    (F : LocalField.{u, v} K) :
    Polynomial F.residueField⟦X⟧
theorem

equalCharacteristicLubinTateIntegralPiPolynomial_monic

L45 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomial_monic
Documentation

The integral Lubin–Tate π-polynomial is monic.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomial_monic
    (F : LocalField.{u, v} K) :
    (equalCharacteristicLubinTateIntegralPiPolynomial F).Monic
theorem

equalCharacteristicLubinTateIntegralPiPolynomial_natDegree

L55 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomial_natDegree
Documentation

The integral Lubin–Tate π-polynomial has degree equal to the residue-field cardinality.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomial_natDegree
    (F : LocalField.{u, v} K) :
    (equalCharacteristicLubinTateIntegralPiPolynomial F).natDegree =
      Nat.card F.residueField
def

equalCharacteristicLubinTateIntegralPiPolynomialIterate

L67 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomialIterate
Documentation

The compositional division polynomial over κ[[T]].

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTateIntegralPiPolynomialIterate
    (F : LocalField.{u, v} K) (n : ℕ) :
    Polynomial F.residueField⟦X⟧
theorem

equalCharacteristicLubinTateIntegralPiPolynomialIterate_natDegree

L73 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomialIterate_natDegree
Documentation

The n-fold integral π-iterate has degree q ^ n.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomialIterate_natDegree
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPiPolynomialIterate F n).natDegree =
      Nat.card F.residueField ^ n
theorem

equalCharacteristicLubinTateIntegralPiPolynomialIterate_succ

L83 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomialIterate_succ
Documentation

A successor integral π-iterate is obtained by one further composition.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomialIterate_succ
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicLubinTateIntegralPiPolynomialIterate F (n + 1) =
      (equalCharacteristicLubinTateIntegralPiPolynomial F).comp
        (equalCharacteristicLubinTateIntegralPiPolynomialIterate F n)
theorem

equalCharacteristicLubinTateIntegralPiPolynomialIterate_monic

L93 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomialIterate_monic
Documentation

Every iterate of the integral Lubin–Tate π-polynomial is monic.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomialIterate_monic
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPiPolynomialIterate F n).Monic
theorem

equalCharacteristicLubinTateIntegralPiPolynomial_map

L108 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomial_map
Documentation

Base change carries the integral π-polynomial to the Laurent-field π-polynomial.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomial_map
    (F : LocalField.{u, v} K) :
    (equalCharacteristicLubinTateIntegralPiPolynomial F).map
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩) =
      equalCharacteristicLubinTatePiPolynomial F
theorem

equalCharacteristicLubinTateIntegralPiPolynomialIterate_map

L118 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomialIterate_map
Documentation

Base change commutes with iteration of the integral π-polynomial.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomialIterate_map
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPiPolynomialIterate F n).map
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩) =
      equalCharacteristicLubinTatePiPolynomialIterate F n
theorem

equalCharacteristicLubinTateIntegralPiPolynomial_map_constantCoeff

L134 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomial_map_constantCoeff
Documentation

Reducing coefficients sends the integral π-polynomial to X ^ q.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomial_map_constantCoeff
    (F : LocalField.{u, v} K) :
    (equalCharacteristicLubinTateIntegralPiPolynomial F).map
        (PowerSeries.constantCoeff (R := F.residueField)) =
      Polynomial.X ^ Nat.card F.residueField
theorem

equalCharacteristicLubinTateIntegralPiPolynomialIterate_map_constantCoeff

L142 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomialIterate_map_constantCoeff
Documentation

Reducing coefficients sends the n-fold integral π-iterate to X ^ (q ^ n).

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomialIterate_map_constantCoeff
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPiPolynomialIterate F n).map
        (PowerSeries.constantCoeff (R := F.residueField)) =
      Polynomial.X ^ (Nat.card F.residueField ^ n)
theorem

equalCharacteristicLubinTateIntegralPiPolynomialIterate_eval_zero

L158 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPiPolynomialIterate_eval_zero
Documentation

Every integral π-iterate vanishes at zero.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPiPolynomialIterate_eval_zero
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPiPolynomialIterate F n).eval 0 = 0
def

equalCharacteristicLubinTateIntegralPrimitivePolynomial

L172 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPrimitivePolynomial
Documentation

The integral lift of the primitive level-n+1 polynomial.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTateIntegralPrimitivePolynomial
    (F : LocalField.{u, v} K) (n : ℕ) :
    Polynomial F.residueField⟦X⟧
theorem

equalCharacteristicLubinTateIntegralPrimitivePolynomial_natDegree

L180 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPrimitivePolynomial_natDegree
Documentation

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

Source context 7 commands

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

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

equalCharacteristicLubinTateIntegralPrimitivePolynomial_monic

L200 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPrimitivePolynomial_monic
Documentation

The integral primitive polynomial is monic.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPrimitivePolynomial_monic
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPrimitivePolynomial F n).Monic
theorem

equalCharacteristicLubinTateIntegralPrimitivePolynomial_map

L220 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPrimitivePolynomial_map
Documentation

Base change carries the integral primitive polynomial to its Laurent-field counterpart.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPrimitivePolynomial_map
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPrimitivePolynomial F n).map
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩) =
      equalCharacteristicLubinTatePrimitivePolynomial F n
theorem

equalCharacteristicLubinTateIntegralPrimitivePolynomial_map_constantCoeff

L231 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPrimitivePolynomial_map_constantCoeff
Documentation

Reducing the integral primitive polynomial yields its leading monomial.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPrimitivePolynomial_map_constantCoeff
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPrimitivePolynomial F n).map
        (PowerSeries.constantCoeff (R := F.residueField)) =
      Polynomial.X ^
        ((Nat.card F.residueField - 1) * Nat.card F.residueField ^ n)
theorem

equalCharacteristicLubinTateIntegralPrimitivePolynomial_coeff_zero

L242 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPrimitivePolynomial_coeff_zero
Documentation

The integral primitive polynomial has constant coefficient X.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPrimitivePolynomial_coeff_zero
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPrimitivePolynomial F n).coeff 0 =
      (PowerSeries.X : F.residueField⟦X⟧)
theorem

powerSeries_X_notMem_span_X_sq

L253 ↗
LubinTate.EqualCharacteristic.powerSeries_X_notMem_span_X_sq
Documentation

The power-series parameter X does not lie in the square of its principal ideal.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem powerSeries_X_notMem_span_X_sq
    (k : Type*) [Field k] :
    (PowerSeries.X : k⟦X⟧) ∉
      (Ideal.span ({PowerSeries.X} : Set k⟦X⟧)) ^ 2
theorem

equalCharacteristicLubinTateIntegralPrimitivePolynomial_isEisensteinAt

L268 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPrimitivePolynomial_isEisensteinAt
Documentation

The integral primitive polynomial is Eisenstein at (T).

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPrimitivePolynomial_isEisensteinAt
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTateIntegralPrimitivePolynomial F n).IsEisensteinAt
      (Ideal.span ({PowerSeries.X} : Set F.residueField⟦X⟧))
theorem

equalCharacteristicLubinTateIntegralPrimitivePolynomial_irreducible

L295 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateIntegralPrimitivePolynomial_irreducible
Documentation

The integral primitive polynomial is irreducible by Eisenstein's criterion.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateIntegralPrimitivePolynomial_irreducible
    (F : LocalField.{u, v} K) (n : ℕ) :
    Irreducible (equalCharacteristicLubinTateIntegralPrimitivePolynomial F n)
theorem

equalCharacteristicLubinTatePrimitivePolynomial_monic

L308 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePolynomial_monic
Documentation

The primitive polynomial over κ((T)) is monic.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePolynomial_monic
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicLubinTatePrimitivePolynomial F n).Monic
theorem

equalCharacteristicLubinTatePrimitivePolynomial_irreducible

L315 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePolynomial_irreducible
Documentation

The primitive level-n+1 polynomial over κ((T)) is irreducible.

Source context 7 commands

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

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTatePrimitivePolynomial_irreducible
    (F : LocalField.{u, v} K) (n : ℕ) :
    Irreducible (equalCharacteristicLubinTatePrimitivePolynomial F n)

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