Module

LevelAbelian.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.LevelAbelian

8 declarations indexed from sourceView source ↗

Module documentation

Abelian standard Lubin--Tate level fields

The finite unit parameter group

O_F^* / U_F^(n + 1)

acts multiplicatively and faithfully on the primitive level-n + 1 division point. The finite-level automorphism calculation identifies this parameter group bijectively with the full Galois group. We package that identification as a multiplicative equivalence and transport commutativity to the Galois group.

Imports2

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.LevelAutomorphisms
Mathlib.FieldTheory.Galois.Abelian

Imported by5

def

standardLubinTateUnitParameterToGalHom

L38 ↗

LubinTate.standardLubinTateUnitParameterToGalHom

Documentation

The multiplicative map from finite unit parameters to automorphisms of the standard Lubin--Tate level field.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

def standardLubinTateUnitParameterToGalHom
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    standardLubinTateUnitParameter F n →*
      Gal((standardLubinTateLevelField hπ n) / K) where
  toFun := standardLubinTateUnitParameterToGal F hπ n
  map_one' := standardLubinTateUnitParameterToGal_one F hπ n
  map_mul' := standardLubinTateUnitParameterToGal_mul F hπ n

theorem

standardLubinTateUnitParameterToGalHom_apply

L51 ↗

LubinTate.standardLubinTateUnitParameterToGalHom_apply

Documentation

The homomorphism has the original parameter-to-Galois map as its underlying function.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTateUnitParameterToGalHom_apply
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) :
    standardLubinTateUnitParameterToGalHom F hπ n a =
      standardLubinTateUnitParameterToGal F hπ n a

def

standardLubinTateUnitParameterEquivGal

L61 ↗

LubinTate.standardLubinTateUnitParameterEquivGal

Documentation

Finite unit parameters are multiplicatively equivalent to the full Galois group of the standard level field.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

def standardLubinTateUnitParameterEquivGal
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    standardLubinTateUnitParameter F n ≃*
      Gal((standardLubinTateLevelField hπ n) / K)

theorem

standardLubinTateUnitParameterEquivGal_apply

L77 ↗

LubinTate.standardLubinTateUnitParameterEquivGal_apply

Documentation

The multiplicative equivalence evaluates as the original explicit parameter automorphism.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTateUnitParameterEquivGal_apply
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) :
    standardLubinTateUnitParameterEquivGal F hπ n a =
      standardLubinTateUnitParameterToGal F hπ n a

theorem

standardLubinTateUnitParameterEquivGal_inv_class_apply_gen

L92 ↗

LubinTate.standardLubinTateUnitParameterEquivGal_inv_class_apply_gen

Documentation

The inverse of the explicit unit-parameter automorphism acts on the chosen primitive generator through the inverse Lubin--Tate unit action.

This is the pointwise [u⁻¹] target needed for the later comparison with the actual local Artin map; it does not identify the two maps merely from their kernels.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTateUnitParameterEquivGal_inv_class_apply_gen
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (u : F.valuationSubringˣ) :
    (standardLubinTateUnitParameterEquivGal F hπ n
        (standardLubinTateUnitParameterClass F n u))⁻¹
        (standardLubinTateLevelPowerBasis hπ n).gen =
      standardLubinTatePrimitiveLevelAction hπ n u⁻¹

theorem

standardLubinTateLevelField_gal_comm

L125 ↗

LubinTate.standardLubinTateLevelField_gal_comm

Documentation

The full Galois group of a standard finite Lubin--Tate level is commutative.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

theorem standardLubinTateLevelField_gal_comm
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ)
    (σ τ : Gal((standardLubinTateLevelField hπ n)/K)) :
    σ * τ = τ * σ

instance

standardLubinTateLevelField_isMulCommutative

L139 ↗

LubinTate.standardLubinTateLevelField_isMulCommutative

Documentation

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

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · statement

instance standardLubinTateLevelField_isMulCommutative
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    IsMulCommutative
      (Gal((standardLubinTateLevelField hπ n) / K))

instance

standardLubinTateLevelField_isAbelianGalois

L149 ↗

LubinTate.standardLubinTateLevelField_isAbelianGalois

Documentation

Every standard finite Lubin--Tate level is abelian Galois over its base local field.

Source context 5 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]

Lean source · full declaration

instance standardLubinTateLevelField_isAbelianGalois
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    IsAbelianGalois K (standardLubinTateLevelField hπ n) where
  toIsGalois :=
    standardLubinTateLevelField_isGalois (F := F) hπ n
  toIsMulCommutative :=
    standardLubinTateLevelField_isMulCommutative F hπ n

Module documentation

Abelian standard Lubin--Tate level fields

Declarations