Module

LevelField.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.LevelField

9 declarations indexed from sourceView source ↗

Module documentation

The uniformizer norm identity: equal-characteristic Lubin--Tate level fields

The level-n+1 field is the simple extension generated by a primitive division point. Eisenstein irreducibility identifies its minimal polynomial with the primitive division polynomial and gives the exact degree (q - 1) q^n.

Imports3

Mathlib.SetTheory.Cardinal.Finite
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.PrimitiveIrreducible
Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.PrimitiveTorsion

Imported by9

theorem

equalCharacteristicSeparableBaseHom_eq_algebraMap

L38 ↗

LubinTate.EqualCharacteristic.equalCharacteristicSeparableBaseHom_eq_algebraMap

Documentation

The explicit base embedding used to choose division roots is the canonical algebra map of the separable closure.

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 equalCharacteristicSeparableBaseHom_eq_algebraMap
    (F : LocalField.{u, v} K) :
    equalCharacteristicSeparableBaseHom F =
      algebraMap F.residueField⸨X⸩
        (SeparableClosure F.residueField⸨X⸩)

def

equalCharacteristicLubinTateLevelField

L48 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField

Documentation

The simple extension generated by the chosen primitive level-n+1 division point.

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 equalCharacteristicLubinTateLevelField
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    IntermediateField F.residueField⸨X⸩
      (SeparableClosure F.residueField⸨X⸩)

def

equalCharacteristicLubinTateLevelFieldAlgebra

L61 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldAlgebra

Documentation

The canonical base algebra on a Lubin--Tate level field.

Naming this structure lets downstream files install the intended algebra locally without unfolding the separable-closure construction.

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 equalCharacteristicLubinTateLevelFieldAlgebra
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Algebra F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)

def

equalCharacteristicLubinTateLevelFieldSMul

L73 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldSMul

Documentation

Defines equalCharacteristicLubinTateLevelFieldSMul.

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 equalCharacteristicLubinTateLevelFieldSMul
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    SMul F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)

def

equalCharacteristicLubinTateLevelFieldModule

L85 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelFieldModule

Documentation

Defines equalCharacteristicLubinTateLevelFieldModule.

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 equalCharacteristicLubinTateLevelFieldModule
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Module F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)

theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_isIntegral

L97 ↗

LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_isIntegral

Documentation

The primitive division point is integral 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

theorem chosenEqualCharacteristicLubinTatePrimitiveRoot_isIntegral
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    IsIntegral F.residueField⸨X⸩
      (chosenEqualCharacteristicLubinTatePrimitiveRoot F n)

theorem

equalCharacteristicLubinTatePrimitivePolynomial_eq_minpoly

L111 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePolynomial_eq_minpoly

Documentation

The Eisenstein primitive polynomial is exactly the minimal polynomial of the chosen primitive division point.

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_eq_minpoly
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTatePrimitivePolynomial F n =
      minpoly F.residueField⸨X⸩
        (chosenEqualCharacteristicLubinTatePrimitiveRoot F n)

theorem

equalCharacteristicLubinTateLevelField_finiteDimensional

L129 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField_finiteDimensional

Documentation

Every equal-characteristic Lubin--Tate level field is finite over the Laurent-series base.

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 equalCharacteristicLubinTateLevelField_finiteDimensional
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)

theorem

equalCharacteristicLubinTateLevelField_finrank

L139 ↗

LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField_finrank

Documentation

The exact degree of the primitive level-n+1 extension.

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 equalCharacteristicLubinTateLevelField_finrank
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Module.finrank F.residueField⸨X⸩
        (equalCharacteristicLubinTateLevelField F n) =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n

Module documentation

The uniformizer norm identity: equal-characteristic Lubin--Tate level fields

Declarations