NYLL
Module

PrimitiveTorsion.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.PrimitiveTorsion
7 declarations indexed from sourceView source ↗

Module documentation

The uniformizer norm identity: primitive equal-characteristic division points

The primitive factor Q_(n+1) constructed in the preceding file has roots which are killed by the (n+1)-st Lubin--Tate iterate but not by the n-th iterate. This file chooses one such root in the fixed separable closure and records that exact-level property. No irreducibility or Galois assertion is used here.

Imports2
Imported by5

Declarations

def

chosenEqualCharacteristicLubinTatePrimitiveRoot

L37 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot
Documentation

A chosen root of the primitive level-n+1 division polynomial in the fixed separable closure of κ((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 chosenEqualCharacteristicLubinTatePrimitiveRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) : SeparableClosure F.residueField⸨X⸩
theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_isRoot

L45 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_isRoot
Documentation

The chosen primitive division point is a root of Q_(n+1).

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_isRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    ((equalCharacteristicLubinTatePrimitivePolynomial F n).map
      (equalCharacteristicSeparableBaseHom F)).IsRoot
        (chosenEqualCharacteristicLubinTatePrimitiveRoot F n)
theorem

equalCharacteristicLubinTatePrimitivePolynomial_eval₂

L56 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePolynomial_eval₂
Documentation

Evaluation of Q_(n+1) is the defining primitive-division equation.

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_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (φ : F.residueField⸨X⸩ →+* A) (n : ℕ) (x : A) :
    Polynomial.eval₂ φ x
        (equalCharacteristicLubinTatePrimitivePolynomial F n) =
      equalCharacteristicLubinTateAmbientPiIterate F
          (φ (equalCharacteristicLaurentUniformizer F)) n x ^
          (Nat.card F.residueField - 1) +
        φ (equalCharacteristicLaurentUniformizer F)
theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_equation

L73 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_equation
Documentation

The chosen root satisfies the primitive-division equation.

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_equation
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicSeparableUniformizer F) n
        (chosenEqualCharacteristicLubinTatePrimitiveRoot F n) ^
          (Nat.card F.residueField - 1) +
      equalCharacteristicSeparableUniformizer F = 0
theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_torsion

L93 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_torsion
Documentation

A primitive level-n+1 point is killed by the next division 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 chosenEqualCharacteristicLubinTatePrimitiveRoot_torsion
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicSeparableUniformizer F) (n + 1)
      (chosenEqualCharacteristicLubinTatePrimitiveRoot F n)
theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_not_torsion_pred

L118 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_not_torsion_pred
Documentation

The chosen root is not already a level-n 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 chosenEqualCharacteristicLubinTatePrimitiveRoot_not_torsion_pred
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    ¬ IsEqualCharacteristicLubinTateAmbientTorsion F
      (equalCharacteristicSeparableUniformizer F) n
      (chosenEqualCharacteristicLubinTatePrimitiveRoot F n)
theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_ne_zero

L135 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_ne_zero
Documentation

In particular, a primitive division point is nonzero.

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_ne_zero
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    chosenEqualCharacteristicLubinTatePrimitiveRoot F n ≠ 0

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