NYLL
Module

FiniteParameters.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.FiniteParameters
16 declarations indexed from sourceView source ↗

Module documentation

The uniformizer norm identity: finite parameters for the Lubin--Tate action

A unit power series modulo its first n+1 coefficients is represented by a nonzero constant coefficient and n arbitrary further coefficients. We use the concrete finite parameter type κˣ × (Fin n → κ), construct its genuine power-series units, and prove that their bracket images of a primitive point are pairwise distinct. Its cardinality is (q - 1) q^n, exactly the degree of the primitive polynomial.

Imports2
Imported by8

Declarations

structure

equalCharacteristicLubinTateUnitParameter

L37 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameter
Documentation

The visible coefficients of a unit power series through level n.

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 · full declaration
structure equalCharacteristicLubinTateUnitParameter
    (F : LocalField.{u, v} K) (n : ℕ) where
  /-- The nonzero constant coefficient of the represented unit power series. -/
  constantUnit : F.residueFieldˣ
  /-- The coefficients in degrees `1` through `n`, indexed with degree shifted down by one. -/
  higherCoeff : Fin n → F.residueField
theorem

equalCharacteristicLubinTateUnitParameter_ext

L46 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameter_ext
Documentation

Unit parameters agree when their constant units and higher coefficients agree.

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 equalCharacteristicLubinTateUnitParameter_ext
    (F : LocalField.{u, v} K) (n : ℕ)
    {a b : equalCharacteristicLubinTateUnitParameter F n}
    (hconstant : a.constantUnit = b.constantUnit)
    (hhigher : a.higherCoeff = b.higherCoeff) :
    a = b
def

equalCharacteristicLubinTateUnitParameterOfCoefficients

L60 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterOfCoefficients
Documentation

Constructor exposing the mathematical coefficient data without relying on the implementation of the finite parameter.

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 equalCharacteristicLubinTateUnitParameterOfCoefficients
    (F : LocalField.{u, v} K) (n : ℕ)
    (constantUnit : F.residueFieldˣ)
    (higherCoeff : Fin n → F.residueField) :
    equalCharacteristicLubinTateUnitParameter F n
def

equalCharacteristicLubinTateUnitParameterEquiv

L68 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterEquiv
Documentation

Comparison with the elementary product of visible coefficients.

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 · full declaration
def equalCharacteristicLubinTateUnitParameterEquiv
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicLubinTateUnitParameter F n ≃
      F.residueFieldˣ × (Fin n → F.residueField) where
  toFun a := (a.constantUnit, a.higherCoeff)
  invFun a := equalCharacteristicLubinTateUnitParameterOfCoefficients
    F n a.1 a.2
  left_inv a := by cases a; rfl
  right_inv a := rfl
instance

equalCharacteristicLubinTateUnitParameter_finite

L79 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameter_finite
Documentation

The finite-level unit parameter space is finite.

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
instance equalCharacteristicLubinTateUnitParameter_finite
    (F : LocalField.{u, v} K) (n : ℕ) :
    Finite (equalCharacteristicLubinTateUnitParameter F n)
def

equalCharacteristicLubinTateUnitParameterSeries

L87 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterSeries
Documentation

The finite polynomial power series represented by a visible unit parameter.

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 equalCharacteristicLubinTateUnitParameterSeries
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    F.residueField⟦X⟧
theorem

equalCharacteristicLubinTateUnitParameterSeries_coeff_zero

L97 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterSeries_coeff_zero
Documentation

The parameter series has the stored unit as its 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 equalCharacteristicLubinTateUnitParameterSeries_coeff_zero
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    PowerSeries.coeff 0
      (equalCharacteristicLubinTateUnitParameterSeries F n a) =
        a.constantUnit
theorem

equalCharacteristicLubinTateUnitParameterSeries_coeff_succ

L107 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterSeries_coeff_succ
Documentation

Positive coefficients of the parameter series recover the stored higher coefficients.

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 equalCharacteristicLubinTateUnitParameterSeries_coeff_succ
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) (i : Fin n) :
    PowerSeries.coeff (i + 1)
      (equalCharacteristicLubinTateUnitParameterSeries F n a) =
        a.higherCoeff i
theorem

equalCharacteristicLubinTateUnitParameterSeries_isUnit

L117 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterSeries_isUnit
Documentation

A represented series is a unit because its constant coefficient is the nonzero value of a residue-field unit.

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 equalCharacteristicLubinTateUnitParameterSeries_isUnit
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    IsUnit (equalCharacteristicLubinTateUnitParameterSeries F n a)
def

equalCharacteristicLubinTateUnitParameterUnit

L127 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterUnit
Documentation

The actual power-series unit attached to a finite parameter.

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 equalCharacteristicLubinTateUnitParameterUnit
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    F.residueField⟦X⟧ˣ
theorem

equalCharacteristicLubinTateUnitParameterUnit_val

L135 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterUnit_val
Documentation

The unit built from a parameter has the parameter series as its value.

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 equalCharacteristicLubinTateUnitParameterUnit_val
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    (equalCharacteristicLubinTateUnitParameterUnit F n a :
      F.residueField⟦X⟧) =
      equalCharacteristicLubinTateUnitParameterSeries F n a
theorem

equalCharacteristicLubinTateUnitParameter_eq_of_coeff_eq

L144 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameter_eq_of_coeff_eq
Documentation

Visible coefficient equality determines the finite parameter.

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 equalCharacteristicLubinTateUnitParameter_eq_of_coeff_eq
    (F : LocalField.{u, v} K) (n : ℕ)
    (a b : equalCharacteristicLubinTateUnitParameter F n)
    (hcoeff : ∀ i ≤ n,
      PowerSeries.coeff i
          (equalCharacteristicLubinTateUnitParameterSeries F n a) =
        PowerSeries.coeff i
          (equalCharacteristicLubinTateUnitParameterSeries F n b)) :
    a = b
def

equalCharacteristicLubinTateUnitParameterRoot

L160 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterRoot
Documentation

The primitive-root image attached to a finite unit parameter.

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

equalCharacteristicLubinTateUnitParameterRoot_injective

L172 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterRoot_injective
Documentation

Distinct visible unit parameters give distinct primitive roots.

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 equalCharacteristicLubinTateUnitParameterRoot_injective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Injective
      (equalCharacteristicLubinTateUnitParameterRoot F n)
theorem

equalCharacteristicLubinTateUnitParameterRoot_isRoot

L185 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterRoot_isRoot
Documentation

Every parameter root is a root of the primitive 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 equalCharacteristicLubinTateUnitParameterRoot_isRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    ((equalCharacteristicLubinTatePrimitivePolynomial F n).map
      (equalCharacteristicSeparableBaseHom F)).IsRoot
        (equalCharacteristicLubinTateUnitParameterRoot F n a)
theorem

equalCharacteristicLubinTateUnitParameter_natCard

L198 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameter_natCard
Documentation

The finite parameter set has the expected cardinality.

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 equalCharacteristicLubinTateUnitParameter_natCard
    (F : LocalField.{u, v} K) (n : ℕ) :
    Nat.card (equalCharacteristicLubinTateUnitParameter F n) =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n

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