Module

PrimitiveTorsion.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.PrimitiveTorsion

13 declarations indexed from sourceView source ↗

Module documentation

Primitive Lubin--Tate torsion points

This file records the exact torsion level of the primitive roots chosen in PrimitiveRoot. The standard division-polynomial iterates are first mapped from the valuation ring to the base field and to its fixed separable closure. Their evaluations satisfy the expected additivity under composition.

For a root of the primitive level-n + 1 factor, the factorization of the next iterate shows that the level-n + 1 iterate vanishes. The primitive equation and nonvanishing of the uniformizer show that the level-n iterate does not vanish. All arguments are characteristic-independent.

Imports1

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.PrimitiveRoot

Imported by2

def

standardLubinTatePolynomialIterateOverField

L39 ↗

LubinTate.standardLubinTatePolynomialIterateOverField

Documentation

The n-fold standard iterate after extending coefficients from the valuation ring to the base field.

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

def standardLubinTatePolynomialIterateOverField
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    Polynomial K

def

standardLubinTatePolynomialIterateOverSeparableClosure

L47 ↗

LubinTate.standardLubinTatePolynomialIterateOverSeparableClosure

Documentation

The n-fold standard iterate after extending coefficients to the fixed separable closure of the base field.

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

def standardLubinTatePolynomialIterateOverSeparableClosure
    (F : LocalField.{u, v} K) (π : F.valuationSubring) (n : ℕ) :
    Polynomial (SeparableClosure K)

theorem

standardLubinTatePolynomialIterateOverField_eval

L57 ↗

LubinTate.standardLubinTatePolynomialIterateOverField_eval

Documentation

Evaluation of the field-valued iterate is evaluation over the valuation ring with the coefficient embedding.

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 standardLubinTatePolynomialIterateOverField_eval
    (F : LocalField.{u, v} K) (π : F.valuationSubring)
    (n : ℕ) (x : K) :
    (standardLubinTatePolynomialIterateOverField F π n).eval x =
      Polynomial.eval₂ (algebraMap F.valuationSubring K) x
        (standardLubinTatePolynomialIterate F π n)

theorem

standardLubinTatePolynomialIterateOverSeparableClosure_eval

L69 ↗

LubinTate.standardLubinTatePolynomialIterateOverSeparableClosure_eval

Documentation

Evaluation of the separable-closure-valued iterate is evaluation over the valuation ring with the composite coefficient embedding.

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 standardLubinTatePolynomialIterateOverSeparableClosure_eval
    (F : LocalField.{u, v} K) (π : F.valuationSubring)
    (n : ℕ) (x : SeparableClosure K) :
    (standardLubinTatePolynomialIterateOverSeparableClosure F π n).eval x =
      Polynomial.eval₂
        ((algebraMap K (SeparableClosure K)).comp
          (algebraMap F.valuationSubring K))
        x (standardLubinTatePolynomialIterate F π n)

theorem

standardLubinTatePolynomialIterate_eval₂_eq_iterate

L82 ↗

LubinTate.standardLubinTatePolynomialIterate_eval₂_eq_iterate

Documentation

Evaluating a compositional iterate is the corresponding iterate of the evaluation function.

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 · full declaration

theorem standardLubinTatePolynomialIterate_eval₂_eq_iterate
    (F : LocalField.{u, v} K) (π : F.valuationSubring)
    {A : Type*} [CommSemiring A]
    (φ : F.valuationSubring →+* A) (n : ℕ) (x : A) :
    Polynomial.eval₂ φ x
        (standardLubinTatePolynomialIterate F π n) =
      (fun y : A =>
        Polynomial.eval₂ φ y (standardLubinTatePolynomial F π))^[n] x := by
  simp [standardLubinTatePolynomialIterate]

theorem

standardLubinTatePolynomialIterate_eval₂_add

L93 ↗

LubinTate.standardLubinTatePolynomialIterate_eval₂_add

Documentation

Standard iterate indices add under evaluated composition.

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_eval₂_add
    (F : LocalField.{u, v} K) (π : F.valuationSubring)
    {A : Type*} [CommSemiring A]
    (φ : F.valuationSubring →+* A) (m n : ℕ) (x : A) :
    Polynomial.eval₂ φ x
        (standardLubinTatePolynomialIterate F π (m + n)) =
      Polynomial.eval₂ φ
        (Polynomial.eval₂ φ x
          (standardLubinTatePolynomialIterate F π n))
        (standardLubinTatePolynomialIterate F π m)

theorem

standardLubinTatePolynomialIterateOverSeparableClosure_eval_add

L123 ↗

LubinTate.standardLubinTatePolynomialIterateOverSeparableClosure_eval_add

Documentation

In the fixed separable closure, evaluation of standard iterates is additive in the iterate index.

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 standardLubinTatePolynomialIterateOverSeparableClosure_eval_add
    (F : LocalField.{u, v} K) (π : F.valuationSubring)
    (m n : ℕ) (x : SeparableClosure K) :
    (standardLubinTatePolynomialIterateOverSeparableClosure
        F π (m + n)).eval x =
      (standardLubinTatePolynomialIterateOverSeparableClosure F π m).eval
        ((standardLubinTatePolynomialIterateOverSeparableClosure
          F π n).eval x)

theorem

standardLubinTatePrimitivePolynomialOverField_eval₂

L140 ↗

LubinTate.standardLubinTatePrimitivePolynomialOverField_eval₂

Documentation

Evaluation of the primitive polynomial after a further coefficient map is the primitive division equation for the mapped iterate.

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 standardLubinTatePrimitivePolynomialOverField_eval₂
    (F : LocalField.{u, v} K) (π : F.valuationSubring)
    {A : Type*} [CommRing A] (φ : K →+* A)
    (n : ℕ) (x : A) :
    Polynomial.eval₂ φ x
        (standardLubinTatePrimitivePolynomialOverField F π n) =
      Polynomial.eval₂
          (φ.comp (algebraMap F.valuationSubring K)) x
          (standardLubinTatePolynomialIterate F π n) ^
          (Nat.card F.residueField - 1) +
        φ (π : K)

theorem

chosenStandardLubinTatePrimitiveRoot_equation

L157 ↗

LubinTate.chosenStandardLubinTatePrimitiveRoot_equation

Documentation

The chosen primitive root satisfies its primitive division equation in the fixed separable closure.

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 chosenStandardLubinTatePrimitiveRoot_equation
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTatePolynomialIterateOverSeparableClosure F π n).eval
          (chosenStandardLubinTatePrimitiveRoot hπ n) ^
        (Nat.card F.residueField - 1) +
      algebraMap K (SeparableClosure K) (π : K) = 0

theorem

chosenStandardLubinTatePrimitiveRoot_iterate_succ_eq_zero

L178 ↗

LubinTate.chosenStandardLubinTatePrimitiveRoot_iterate_succ_eq_zero

Documentation

The chosen primitive level-n + 1 root is killed by the level-n + 1 standard iterate.

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 chosenStandardLubinTatePrimitiveRoot_iterate_succ_eq_zero
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTatePolynomialIterateOverSeparableClosure
        F π (n + 1)).eval
      (chosenStandardLubinTatePrimitiveRoot hπ n) = 0

theorem

chosenStandardLubinTatePrimitiveRoot_iterate_ne_zero

L207 ↗

LubinTate.chosenStandardLubinTatePrimitiveRoot_iterate_ne_zero

Documentation

The chosen primitive level-n + 1 root is not already killed by the level-n standard iterate.

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 chosenStandardLubinTatePrimitiveRoot_iterate_ne_zero
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    (standardLubinTatePolynomialIterateOverSeparableClosure F π n).eval
        (chosenStandardLubinTatePrimitiveRoot hπ n) ≠ 0

theorem

chosenStandardLubinTatePrimitiveRoot_ne_zero

L223 ↗

LubinTate.chosenStandardLubinTatePrimitiveRoot_ne_zero

Documentation

In particular, the chosen primitive root is nonzero.

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

theorem

chosenStandardLubinTatePrimitivePredecessor_isRoot

L238 ↗

LubinTate.chosenStandardLubinTatePrimitivePredecessor_isRoot

Documentation

Applying the (n - m)-fold standard iterate to a primitive level-n + 1 point gives a root of the primitive level-m + 1 polynomial.

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 · full declaration

theorem chosenStandardLubinTatePrimitivePredecessor_isRoot
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    {m n : ℕ} (hmn : m ≤ n) :
    let y :=
      (standardLubinTatePolynomialIterateOverSeparableClosure
        F π (n - m)).eval
          (chosenStandardLubinTatePrimitiveRoot hπ n)
    ((standardLubinTatePrimitivePolynomialOverField F π m).map
      (algebraMap K (SeparableClosure K))).IsRoot y := by
  let y :=
    (standardLubinTatePolynomialIterateOverSeparableClosure
      F π (n - m)).eval
        (chosenStandardLubinTatePrimitiveRoot hπ n)
  have hyIterate :
      (standardLubinTatePolynomialIterateOverSeparableClosure F π m).eval
          y =
        (standardLubinTatePolynomialIterateOverSeparableClosure F π n).eval
          (chosenStandardLubinTatePrimitiveRoot hπ n) := by
    calc
      (standardLubinTatePolynomialIterateOverSeparableClosure F π m).eval
          y =
          (standardLubinTatePolynomialIterateOverSeparableClosure
            F π (m + (n - m))).eval
              (chosenStandardLubinTatePrimitiveRoot hπ n) :=
        (standardLubinTatePolynomialIterateOverSeparableClosure_eval_add
          F π m (n - m)
          (chosenStandardLubinTatePrimitiveRoot hπ n)).symm
      _ =
          (standardLubinTatePolynomialIterateOverSeparableClosure F π n).eval
            (chosenStandardLubinTatePrimitiveRoot hπ n) := by
        rw [Nat.add_sub_of_le hmn]
  have hyEquation :
      (standardLubinTatePolynomialIterateOverSeparableClosure F π m).eval
            y ^ (Nat.card F.residueField - 1) +
        algebraMap K (SeparableClosure K) (π : K) = 0 := by
    rw [hyIterate]
    exact chosenStandardLubinTatePrimitiveRoot_equation hπ n
  change Polynomial.eval y
      ((standardLubinTatePrimitivePolynomialOverField F π m).map
        (algebraMap K (SeparableClosure K))) = 0
  rw [Polynomial.eval_map,
    standardLubinTatePrimitivePolynomialOverField_eval₂]
  simpa only [
    standardLubinTatePolynomialIterateOverSeparableClosure_eval] using
      hyEquation

Module documentation

Primitive Lubin--Tate torsion points

Declarations