NYLL
Module

LevelAbelian.lean

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

Module documentation

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

The finite unit parameters constructed previously exhaust the automorphisms of a level field. To prove commutativity genuinely, we express each truncated bracket as evaluation of a polynomial over the Laurent-series base. Algebra maps therefore commute with brackets. Multiplicativity of the genuine truncated brackets on division points and commutativity of power-series multiplication then show that any two parameter automorphisms commute on the power-basis generator, hence everywhere.

Imports3
Imported by5

Declarations

theorem

equalCharacteristicLubinTateUnitParameterToGal_surjective

L41 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterToGal_surjective
Documentation

Since the finite parameter injection and the Galois group have the same cardinality, every level-field automorphism comes from a 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 w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateUnitParameterToGal_surjective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Surjective
      (equalCharacteristicLubinTateUnitParameterToGal F n)
theorem

equalCharacteristicLubinTateLevelField_exists_unitParameter

L68 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField_exists_unitParameter
Documentation

Explicit exhaustion statement for the automorphisms of a level field.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateLevelField_exists_unitParameter
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ)
    (σ : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩)) :
    ∃ a : equalCharacteristicLubinTateUnitParameter F n,
      σ = equalCharacteristicLubinTateUnitParameterAlgEquiv F n a
def

equalCharacteristicLubinTateBracketPolynomial

L81 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracketPolynomial
Documentation

The polynomial over the Laurent-series base whose evaluation is a truncated Lubin--Tate bracket.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTateBracketPolynomial
    (F : LocalField.{u, v} K)
    (m : ℕ) (a : F.residueField⟦X⟧) :
    Polynomial F.residueField⸨X⸩
theorem

equalCharacteristicLubinTateBracketPolynomial_eval₂

L93 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateBracketPolynomial_eval₂
Documentation

Evaluating the bracket polynomial in any ambient field gives the genuine truncated bracket.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateBracketPolynomial_eval₂
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    {A : Type w} [Field A] [CharP A F.residueCharacteristic]
    (φ : F.residueField⸨X⸩ →+* A)
    (m : ℕ) (a : F.residueField⟦X⟧) (x : A) :
    Polynomial.eval₂ φ x
        (equalCharacteristicLubinTateBracketPolynomial F m a) =
      equalCharacteristicLubinTateAmbientBracket F
        (φ.comp (algebraMap F.residueField F.residueField⸨X⸩))
        (φ (equalCharacteristicLaurentUniformizer F)) m a x
def

equalCharacteristicLubinTateLevelBracket

L116 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelBracket
Documentation

A truncated bracket, regarded as an endomorphism of the simple level field. Its membership proof is the previously established closure of the level field under brackets.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTateLevelBracket
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n m : ℕ) (a : F.residueField⟦X⟧)
    (x : equalCharacteristicLubinTateLevelField F n) :
    equalCharacteristicLubinTateLevelField F n
theorem

equalCharacteristicLubinTateLevelBracket_coe

L130 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelBracket_coe
Documentation

States the theorem equalCharacteristicLubinTateLevelBracket_coe.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateLevelBracket_coe
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n m : ℕ) (a : F.residueField⟦X⟧)
    (x : equalCharacteristicLubinTateLevelField F n) :
    (equalCharacteristicLubinTateLevelBracket F n m a x :
      SeparableClosure F.residueField⸨X⸩) =
      equalCharacteristicLubinTateAmbientBracket F
        (equalCharacteristicSeparableCoefficientHom F)
        (equalCharacteristicSeparableUniformizer F) m a x.1
theorem

equalCharacteristicLubinTateLevelBracket_eq_aeval

L144 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelBracket_eq_aeval
Documentation

Inside the level field, a truncated bracket is evaluation of its bracket 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 w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateLevelBracket_eq_aeval
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n m : ℕ) (a : F.residueField⟦X⟧)
    (x : equalCharacteristicLubinTateLevelField F n) :
    equalCharacteristicLubinTateLevelBracket F n m a x =
      Polynomial.aeval x
        (equalCharacteristicLubinTateBracketPolynomial F m a)
theorem

equalCharacteristicLubinTateLevelBracket_map

L173 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelBracket_map
Documentation

Algebra endomorphisms of the level field commute with its bracket polynomials.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateLevelBracket_map
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n m : ℕ) (a : F.residueField⟦X⟧)
    (σ : equalCharacteristicLubinTateLevelField F n →ₐ[F.residueField⸨X⸩]
      equalCharacteristicLubinTateLevelField F n)
    (x : equalCharacteristicLubinTateLevelField F n) :
    σ (equalCharacteristicLubinTateLevelBracket F n m a x) =
      equalCharacteristicLubinTateLevelBracket F n m a (σ x)
theorem

equalCharacteristicLubinTateLevelPowerBasis_gen_coe

L198 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelPowerBasis_gen_coe
Documentation

The power-basis generator is the chosen primitive point in the ambient 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 w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateLevelPowerBasis_gen_coe
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    ((equalCharacteristicLubinTateLevelPowerBasis F n).gen :
      SeparableClosure F.residueField⸨X⸩) =
        chosenEqualCharacteristicLubinTatePrimitiveRoot F n
theorem

equalCharacteristicLubinTateLevelBracket_gen

L209 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelBracket_gen
Documentation

Bracketing the power-basis generator with a parameter series gives the corresponding parameter root.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateLevelBracket_gen
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateLevelBracket F n (n + 1)
        (equalCharacteristicLubinTateUnitParameterSeries F n a)
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
      equalCharacteristicLubinTateUnitParameterLevelRoot F n a
theorem

equalCharacteristicLubinTateUnitParameterAlgEquiv_apply_levelRoot

L222 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterAlgEquiv_apply_levelRoot
Documentation

A parameter automorphism sends any parameter root by applying that parameter's bracket to the automorphism's generator image.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateUnitParameterAlgEquiv_apply_levelRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a b : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterAlgEquiv F n a
        (equalCharacteristicLubinTateUnitParameterLevelRoot F n b) =
      equalCharacteristicLubinTateLevelBracket F n (n + 1)
        (equalCharacteristicLubinTateUnitParameterSeries F n b)
        (equalCharacteristicLubinTateUnitParameterLevelRoot F n a)
theorem

equalCharacteristicLubinTateUnitParameterLevelBracket_comm

L255 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterLevelBracket_comm
Documentation

Commutativity of power-series multiplication makes the two possible iterated parameter brackets agree on the primitive 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 w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateUnitParameterLevelBracket_comm
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a b : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateLevelBracket F n (n + 1)
        (equalCharacteristicLubinTateUnitParameterSeries F n b)
        (equalCharacteristicLubinTateUnitParameterLevelRoot F n a) =
      equalCharacteristicLubinTateLevelBracket F n (n + 1)
        (equalCharacteristicLubinTateUnitParameterSeries F n a)
        (equalCharacteristicLubinTateUnitParameterLevelRoot F n b)
theorem

equalCharacteristicLubinTateUnitParameterAlgEquiv_comm

L302 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterAlgEquiv_comm
Documentation

Any two automorphisms arising from finite unit parameters commute.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateUnitParameterAlgEquiv_comm
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a b : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterAlgEquiv F n a *
        equalCharacteristicLubinTateUnitParameterAlgEquiv F n b =
      equalCharacteristicLubinTateUnitParameterAlgEquiv F n b *
        equalCharacteristicLubinTateUnitParameterAlgEquiv F n a
theorem

equalCharacteristicLubinTateLevelField_gal_comm

L327 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField_gal_comm
Documentation

The full finite-level Galois group is commutative.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateLevelField_gal_comm
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ)
    (σ τ : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩)) :
    σ * τ = τ * σ
instance

equalCharacteristicLubinTateLevelField_isMulCommutative

L338 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField_isMulCommutative
Documentation

The Galois group of the explicit level field is a commutative group.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped PowerSeries LaurentSeries Polynomial
universe u v w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
instance equalCharacteristicLubinTateLevelField_isMulCommutative
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    IsMulCommutative
      (Gal((equalCharacteristicLubinTateLevelField F n) /
        F.residueField⸨X⸩))
instance

equalCharacteristicLubinTateLevelField_isAbelianGalois

L349 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField_isAbelianGalois
Documentation

Every explicit equal-characteristic Lubin--Tate level extension is abelian Galois 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 w
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · full declaration
instance equalCharacteristicLubinTateLevelField_isAbelianGalois
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    IsAbelianGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) where
  toIsGalois := equalCharacteristicLubinTateLevelField_isGalois F n
  toIsMulCommutative :=
    equalCharacteristicLubinTateLevelField_isMulCommutative F n

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