NYLL
Module

PrimitiveAction.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.PrimitiveAction
8 declarations indexed from sourceView source ↗

Module documentation

The uniformizer norm identity: the unit action on primitive division points

The genuine truncated Lubin--Tate bracket attached to a unit power series sends a primitive level-n+1 point to another root of the same Eisenstein polynomial. This is the source of the finite-level Galois action; no automorphism or normality is assumed here.

Imports3
Imported by5

Declarations

theorem

equalCharacteristicLubinTateAmbientBracket_apply_of_levelOne_torsion

L38 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientBracket_apply_of_levelOne_torsion
Documentation

On a level-one torsion point, every longer bracket only sees the constant coefficient of the power series.

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 equalCharacteristicLubinTateAmbientBracket_apply_of_levelOne_torsion
    (F : LocalField.{u, v} K)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (m : ℕ) (a : F.residueField⟦X⟧) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t 1 x) :
    equalCharacteristicLubinTateAmbientBracket F ι t (m + 1) a x =
      ι (PowerSeries.coeff 0 a) * x
theorem

equalCharacteristicLubinTateAmbientPrimitive_iterate_bracket

L62 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientPrimitive_iterate_bracket
Documentation

Applying e^n after a bracket scales the level-one predecessor of any primitive level-n+1 point by the bracket's constant coefficient.

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 equalCharacteristicLubinTateAmbientPrimitive_iterate_bracket
    (F : LocalField.{u, v} K)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (a : F.residueField⟦X⟧) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t (n + 1) x) :
    equalCharacteristicLubinTateAmbientPiIterate F t n
        (equalCharacteristicLubinTateAmbientBracket F ι t (n + 1) a x) =
      ι (PowerSeries.coeff 0 a) *
        equalCharacteristicLubinTateAmbientPiIterate F t n x
theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_iterate_bracket

L82 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_iterate_bracket
Documentation

Applying e^n after a unit bracket scales the primitive level-one predecessor by the unit's constant coefficient.

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_iterate_bracket
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧) :
    equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicSeparableUniformizer F) n
        (equalCharacteristicLubinTateAmbientBracket F
          (equalCharacteristicSeparableCoefficientHom F)
          (equalCharacteristicSeparableUniformizer F) (n + 1) a
          (chosenEqualCharacteristicLubinTatePrimitiveRoot F n)) =
      equalCharacteristicSeparableCoefficientHom F
          (PowerSeries.coeff 0 a) *
        equalCharacteristicLubinTateAmbientPiIterate F
          (equalCharacteristicSeparableUniformizer F) n
          (chosenEqualCharacteristicLubinTatePrimitiveRoot F n)
theorem

powerSeries_unit_coeff_zero_ne_zero

L104 ↗
LubinTate.EqualCharacteristic.powerSeries_unit_coeff_zero_ne_zero
Documentation

The constant coefficient of a unit power series 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 powerSeries_unit_coeff_zero_ne_zero
    {k : Type*} [Field k] (a : k⟦X⟧ˣ) :
    PowerSeries.coeff 0 (a : k⟦X⟧) ≠ 0
theorem

equalCharacteristicLubinTateAmbientBracket_sub

L112 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientBracket_sub
Documentation

The ambient bracket is additive in its power-series coordinate, in subtraction form.

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 equalCharacteristicLubinTateAmbientBracket_sub
    (F : LocalField.{u, v} K)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (m : ℕ) (a b : F.residueField⟦X⟧) :
    equalCharacteristicLubinTateAmbientBracket F ι t m (a - b) =
      equalCharacteristicLubinTateAmbientBracket F ι t m a -
        equalCharacteristicLubinTateAmbientBracket F ι t m b
theorem

equalCharacteristicLubinTateAmbientPrimitive_bracket_eq_coeff

L137 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientPrimitive_bracket_eq_coeff
Documentation

Faithfulness of the truncated bracket on any primitive level-n+1 point. This is the intrinsic Lubin--Tate statement used both before and after passage to the completed maximal-unramified 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 equalCharacteristicLubinTateAmbientPrimitive_bracket_eq_coeff
    (F : LocalField.{u, v} K)
    {A : Type*} [Field A] [CharP A F.residueCharacteristic]
    (ι : F.residueField →+* A) (t : A)
    (n : ℕ) (x : A)
    (hx : IsEqualCharacteristicLubinTateAmbientTorsion F t (n + 1) x)
    (hxpred : ¬ IsEqualCharacteristicLubinTateAmbientTorsion F t n x)
    (a b : F.residueField⟦X⟧)
    (hbracket :
      equalCharacteristicLubinTateAmbientBracket F ι t (n + 1) a x =
        equalCharacteristicLubinTateAmbientBracket F ι t (n + 1) b x) :
    ∀ i ≤ n, PowerSeries.coeff i a = PowerSeries.coeff i b
theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_bracket_eq_coeff

L209 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_bracket_eq_coeff
Documentation

Faithfulness on a primitive level-n+1 point: equality of two bracket images forces equality of all coefficients visible at that level.

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_bracket_eq_coeff
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a b : F.residueField⟦X⟧)
    (hbracket :
      equalCharacteristicLubinTateAmbientBracket F
          (equalCharacteristicSeparableCoefficientHom F)
          (equalCharacteristicSeparableUniformizer F) (n + 1) a
          (chosenEqualCharacteristicLubinTatePrimitiveRoot F n) =
        equalCharacteristicLubinTateAmbientBracket F
          (equalCharacteristicSeparableCoefficientHom F)
          (equalCharacteristicSeparableUniformizer F) (n + 1) b
          (chosenEqualCharacteristicLubinTatePrimitiveRoot F n)) :
    ∀ i ≤ n, PowerSeries.coeff i a = PowerSeries.coeff i b
theorem

equalCharacteristicLubinTatePrimitivePolynomial_isRoot_bracket

L233 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTatePrimitivePolynomial_isRoot_bracket
Documentation

Every unit bracket of the chosen primitive point is again a root of the primitive 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 equalCharacteristicLubinTatePrimitivePolynomial_isRoot_bracket
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    ((equalCharacteristicLubinTatePrimitivePolynomial F n).map
      (equalCharacteristicSeparableBaseHom F)).IsRoot
        (equalCharacteristicLubinTateAmbientBracket F
          (equalCharacteristicSeparableCoefficientHom F)
          (equalCharacteristicSeparableUniformizer F) (n + 1)
          (a : F.residueField⟦X⟧)
          (chosenEqualCharacteristicLubinTatePrimitiveRoot F n))

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