NYLL
Module

LevelAutomorphisms.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.FiniteLevel.LevelAutomorphisms
22 declarations indexed from sourceView source ↗

Module documentation

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

The explicit Lubin--Tate brackets preserve the simple level field. Each finite unit parameter therefore gives a root of the generator's minimal polynomial inside that field, hence an automorphism obtained from its power basis. The parameter action is faithful and has as many elements as the degree of the extension. Comparing this lower bound with the standard upper bound for field automorphisms proves that the level extension is Galois.

No commutativity of the automorphism group is asserted here: that requires the multiplicative composition law for the bracket action, not merely the root-counting argument below.

Imports5
Imported by6

Declarations

theorem

equalCharacteristicSeparableUniformizer_mem_lubinTateLevelField

L46 ↗
LubinTate.EqualCharacteristic.equalCharacteristicSeparableUniformizer_mem_lubinTateLevelField
Documentation

The image of the Laurent-series uniformizer belongs to every 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicSeparableUniformizer_mem_lubinTateLevelField
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicSeparableUniformizer F ∈
      equalCharacteristicLubinTateLevelField F n
theorem

equalCharacteristicSeparableCoefficient_mem_lubinTateLevelField

L57 ↗
LubinTate.EqualCharacteristic.equalCharacteristicSeparableCoefficient_mem_lubinTateLevelField
Documentation

Embedded residue-field coefficients belong to every 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicSeparableCoefficient_mem_lubinTateLevelField
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (c : F.residueField) :
    equalCharacteristicSeparableCoefficientHom F c ∈
      equalCharacteristicLubinTateLevelField F n
theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_mem_levelField

L68 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_mem_levelField
Documentation

The chosen primitive point belongs to its simple 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenEqualCharacteristicLubinTatePrimitiveRoot_mem_levelField
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    chosenEqualCharacteristicLubinTatePrimitiveRoot F n ∈
      equalCharacteristicLubinTateLevelField F n
theorem

equalCharacteristicLubinTateAmbientPiIterate_mem_levelField_of_mem

L79 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientPiIterate_mem_levelField_of_mem
Documentation

Every iterate of the distinguished Lubin--Tate endomorphism preserves 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateAmbientPiIterate_mem_levelField_of_mem
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n i : ℕ) {x : SeparableClosure F.residueField⸨X⸩}
    (hx : x ∈ equalCharacteristicLubinTateLevelField F n) :
    equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicSeparableUniformizer F) i x ∈
      equalCharacteristicLubinTateLevelField F n
theorem

chosenEqualCharacteristicLubinTatePrimitiveRoot_piIterate_mem_levelField

L100 ↗
LubinTate.EqualCharacteristic.chosenEqualCharacteristicLubinTatePrimitiveRoot_piIterate_mem_levelField
Documentation

In particular, every distinguished iterate of the chosen primitive point lies in its 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenEqualCharacteristicLubinTatePrimitiveRoot_piIterate_mem_levelField
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n i : ℕ) :
    equalCharacteristicLubinTateAmbientPiIterate F
        (equalCharacteristicSeparableUniformizer F) i
        (chosenEqualCharacteristicLubinTatePrimitiveRoot F n) ∈
      equalCharacteristicLubinTateLevelField F n
theorem

equalCharacteristicLubinTateAmbientBracket_mem_levelField_of_mem

L112 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateAmbientBracket_mem_levelField_of_mem
Documentation

Every truncated Lubin--Tate bracket preserves the 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateAmbientBracket_mem_levelField_of_mem
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n m : ℕ) (a : F.residueField⟦X⟧)
    {x : SeparableClosure F.residueField⸨X⸩}
    (hx : x ∈ equalCharacteristicLubinTateLevelField F n) :
    equalCharacteristicLubinTateAmbientBracket F
        (equalCharacteristicSeparableCoefficientHom F)
        (equalCharacteristicSeparableUniformizer F) m a x ∈
      equalCharacteristicLubinTateLevelField F n
theorem

equalCharacteristicLubinTateUnitParameterRoot_mem_levelField

L131 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterRoot_mem_levelField
Documentation

The explicit root attached to a finite unit parameter lies in the simple level field generated by the chosen 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateUnitParameterRoot_mem_levelField
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterRoot F n a ∈
      equalCharacteristicLubinTateLevelField F n
def

equalCharacteristicLubinTateUnitParameterLevelRoot

L143 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterLevelRoot
Documentation

The parameter root, regarded as an element of the 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTateUnitParameterLevelRoot
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateLevelField F n
theorem

equalCharacteristicLubinTateUnitParameterLevelRoot_coe

L153 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterLevelRoot_coe
Documentation

States the theorem equalCharacteristicLubinTateUnitParameterLevelRoot_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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateUnitParameterLevelRoot_coe
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    (equalCharacteristicLubinTateUnitParameterLevelRoot F n a :
      SeparableClosure F.residueField⸨X⸩) =
        equalCharacteristicLubinTateUnitParameterRoot F n a
theorem

equalCharacteristicLubinTateUnitParameterLevelRoot_injective

L164 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterLevelRoot_injective
Documentation

Finite parameters remain distinct after their roots are regarded as elements of the 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateUnitParameterLevelRoot_injective
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Function.Injective
      (equalCharacteristicLubinTateUnitParameterLevelRoot F n)
def

equalCharacteristicLubinTateLevelPowerBasis

L175 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelPowerBasis
Documentation

The canonical power basis of the simple level extension.

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

equalCharacteristicLubinTateLevelPowerBasis_minpoly

L186 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelPowerBasis_minpoly
Documentation

The minimal polynomial of the power-basis generator is 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 equalCharacteristicLubinTateLevelPowerBasis_minpoly
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    minpoly F.residueField⸨X⸩
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
      equalCharacteristicLubinTatePrimitivePolynomial F n
theorem

equalCharacteristicLubinTateUnitParameterLevelRoot_aeval_minpoly

L204 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterLevelRoot_aeval_minpoly
Documentation

A parameter root annihilates the minimal polynomial of the level-field generator inside the level field itself.

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 equalCharacteristicLubinTateUnitParameterLevelRoot_aeval_minpoly
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    Polynomial.aeval (equalCharacteristicLubinTateUnitParameterLevelRoot F n a)
        (minpoly F.residueField⸨X⸩
          (equalCharacteristicLubinTateLevelPowerBasis F n).gen) = 0
def

equalCharacteristicLubinTateUnitParameterAlgHom

L231 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterAlgHom
Documentation

The algebra endomorphism sending the chosen primitive generator to the explicit root 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 equalCharacteristicLubinTateUnitParameterAlgHom
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateLevelField F n →ₐ[F.residueField⸨X⸩]
      equalCharacteristicLubinTateLevelField F n
theorem

equalCharacteristicLubinTateUnitParameterAlgHom_apply_gen

L243 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterAlgHom_apply_gen
Documentation

States the theorem equalCharacteristicLubinTateUnitParameterAlgHom_apply_gen.

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 equalCharacteristicLubinTateUnitParameterAlgHom_apply_gen
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterAlgHom F n a
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
      equalCharacteristicLubinTateUnitParameterLevelRoot F n a
def

equalCharacteristicLubinTateUnitParameterAlgEquiv

L254 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterAlgEquiv
Documentation

The finite-dimensional algebra endomorphism is automatically an automorphism.

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

equalCharacteristicLubinTateUnitParameterAlgEquiv_apply_gen

L269 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterAlgEquiv_apply_gen
Documentation

States the theorem equalCharacteristicLubinTateUnitParameterAlgEquiv_apply_gen.

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 equalCharacteristicLubinTateUnitParameterAlgEquiv_apply_gen
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterAlgEquiv F n a
        (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
      equalCharacteristicLubinTateUnitParameterLevelRoot F n a
def

equalCharacteristicLubinTateUnitParameterToGal

L282 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterToGal
Documentation

The explicit map from finite unit parameters to the finite-level Galois 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
def equalCharacteristicLubinTateUnitParameterToGal
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateUnitParameter F n →
      Gal((equalCharacteristicLubinTateLevelField F n) /
        F.residueField⸨X⸩)
theorem

equalCharacteristicLubinTateUnitParameterToGal_injective

L293 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateUnitParameterToGal_injective
Documentation

Faithfulness of the bracket action makes the parameter-to-automorphism map injective.

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

equalCharacteristicLubinTateLevelField_galFinite

L308 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField_galFinite
Documentation

Provides the instance equalCharacteristicLubinTateLevelField_galFinite.

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 equalCharacteristicLubinTateLevelField_galFinite
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Finite (Gal((equalCharacteristicLubinTateLevelField F n) /
      F.residueField⸨X⸩))
theorem

equalCharacteristicLubinTateLevelField_natCard_gal

L329 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField_natCard_gal
Documentation

The automorphism group of a level field has cardinality equal to the degree of the extension.

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 equalCharacteristicLubinTateLevelField_natCard_gal
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    Nat.card (Gal((equalCharacteristicLubinTateLevelField F n) /
        F.residueField⸨X⸩)) =
      Module.finrank F.residueField⸨X⸩
        (equalCharacteristicLubinTateLevelField F n)
theorem

equalCharacteristicLubinTateLevelField_isGalois

L357 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateLevelField_isGalois
Documentation

Every equal-characteristic Lubin--Tate level field constructed here is 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
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem equalCharacteristicLubinTateLevelField_isGalois
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)

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