Module

CompletedPrimitiveIrreducible.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedPrimitiveIrreducible

11 declarations indexed from sourceView source ↗

Module documentation

The completed theta-intertwining theorem: irreducibility after completed unramified base change

The primitive Lubin--Tate polynomial remains Eisenstein after replacing the finite residue field κ by its algebraic closure. Consequently it remains irreducible over (AlgebraicClosure κ)((T)). This is the algebraic input needed to prescribe the image of a primitive point when arithmetic Frobenius is extended to the completed level field.

Imports4

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.CompletedLevel.CompletedLevel
Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Mathlib.RingTheory.PowerSeries.Ideal

Imported by5

instance

equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra

L38 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField)

def

equalCharacteristicCompletedIntegralPrimitivePolynomial

L46 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegralPrimitivePolynomial

Documentation

Coefficientwise extension of the integral primitive polynomial from κ[[T]] to (AlgebraicClosure κ)[[T]].

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

def equalCharacteristicCompletedIntegralPrimitivePolynomial
    (F : LocalField.{u, v} K) (n : ℕ) :
    Polynomial (AlgebraicClosure F.residueField)⟦X⟧

theorem

equalCharacteristicCompletedIntegralPrimitivePolynomial_monic

L54 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegralPrimitivePolynomial_monic

Documentation

States the theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_monic.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_monic
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedIntegralPrimitivePolynomial F n).Monic

theorem

equalCharacteristicCompletedIntegralPrimitivePolynomial_natDegree

L60 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegralPrimitivePolynomial_natDegree

Documentation

States the theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_natDegree.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_natDegree
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedIntegralPrimitivePolynomial F n).natDegree =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n

theorem

equalCharacteristicPowerSeriesLaurent_baseChange_commutes

L70 ↗

LubinTate.EqualCharacteristic.equalCharacteristicPowerSeriesLaurent_baseChange_commutes

Documentation

The power-series coefficient map commutes with passage to Laurent series.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicPowerSeriesLaurent_baseChange_commutes
    (F : LocalField.{u, v} K) :
    (algebraMap (AlgebraicClosure F.residueField)⟦X⟧
        (equalCharacteristicCompletedUnramifiedField F.residueField)).comp
        (PowerSeries.map
          (algebraMap F.residueField (AlgebraicClosure F.residueField))) =
      (algebraMap F.residueField⸨X⸩
          (equalCharacteristicCompletedUnramifiedField F.residueField)).comp
        (algebraMap F.residueField⟦X⟧ F.residueField⸨X⸩)

theorem

equalCharacteristicCompletedIntegralPrimitivePolynomial_map

L96 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegralPrimitivePolynomial_map

Documentation

Passing the integral polynomial to the Laurent fraction field gives exactly the completed primitive polynomial.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_map
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedIntegralPrimitivePolynomial F n).map
        (algebraMap (AlgebraicClosure F.residueField)⟦X⟧
          (equalCharacteristicCompletedUnramifiedField F.residueField)) =
      equalCharacteristicCompletedPrimitivePolynomial F n

theorem

equalCharacteristicCompletedIntegralPrimitivePolynomial_map_constantCoeff

L110 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegralPrimitivePolynomial_map_constantCoeff

Documentation

Reduction modulo T is the single leading monomial.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_map_constantCoeff
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedIntegralPrimitivePolynomial F n).map
        (PowerSeries.constantCoeff
          (R := AlgebraicClosure F.residueField)) =
      Polynomial.X ^
        ((Nat.card F.residueField - 1) * Nat.card F.residueField ^ n)

theorem

equalCharacteristicCompletedIntegralPrimitivePolynomial_coeff_zero

L135 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegralPrimitivePolynomial_coeff_zero

Documentation

States the theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_coeff_zero.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_coeff_zero
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedIntegralPrimitivePolynomial F n).coeff 0 =
      (PowerSeries.X : (AlgebraicClosure F.residueField)⟦X⟧)

theorem

equalCharacteristicCompletedIntegralPrimitivePolynomial_isEisensteinAt

L145 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegralPrimitivePolynomial_isEisensteinAt

Documentation

The completed integral primitive polynomial is Eisenstein at (T).

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_isEisensteinAt
    (F : LocalField.{u, v} K) (n : ℕ) :
    (equalCharacteristicCompletedIntegralPrimitivePolynomial F n).IsEisensteinAt
      (Ideal.span
        ({PowerSeries.X} :
          Set (AlgebraicClosure F.residueField)⟦X⟧))

theorem

equalCharacteristicCompletedIntegralPrimitivePolynomial_irreducible

L178 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedIntegralPrimitivePolynomial_irreducible

Documentation

States the theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_irreducible.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicCompletedIntegralPrimitivePolynomial_irreducible
    (F : LocalField.{u, v} K) (n : ℕ) :
    Irreducible (equalCharacteristicCompletedIntegralPrimitivePolynomial F n)

theorem

equalCharacteristicCompletedPrimitivePolynomial_irreducible

L193 ↗

LubinTate.EqualCharacteristic.equalCharacteristicCompletedPrimitivePolynomial_irreducible

Documentation

The primitive polynomial remains irreducible over the completed maximal unramified Laurent field.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries Polynomial PowerSeries
universe u v
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
noncomputable local instance equalCharacteristicCompletedPrimitiveIrreducibleBaseAlgebra
    (F : LocalField.{u, v} K) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicCompletedUnramifiedField F.residueField) :=
  laurentSeriesCoefficientAlgebra

Lean source · statement

theorem equalCharacteristicCompletedPrimitivePolynomial_irreducible
    (F : LocalField.{u, v} K) (n : ℕ) :
    Irreducible (equalCharacteristicCompletedPrimitivePolynomial F n)

Module documentation

The completed theta-intertwining theorem: irreducibility after completed unramified base change

Declarations