Module

GaloisParameterFiltration.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.GaloisParameterFiltration

5 declarations indexed from sourceView source ↗

Module documentation

Principal-unit filtration on finite Lubin--Tate Galois groups

The multiplicative equivalence between finite unit parameters and the Galois group transports the image of U_F^k to a subgroup of the Galois group. This file records membership both for quotient parameters and for valuation-ring unit representatives, and preserves the expected cardinality q ^ (n + 1 - k).

Imports2

Imported by2

def

standardLubinTateGaloisParameterSubgroup

L35 ↗

LubinTate.standardLubinTateGaloisParameterSubgroup

Documentation

The image of the k-th finite unit-parameter subgroup in the Galois group of the standard level-n + 1 Lubin--Tate extension.

Source context 6 commands

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

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

Lean source · statement

def standardLubinTateGaloisParameterSubgroup
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) :
    Subgroup (Gal((standardLubinTateLevelField hπ n) / K))

theorem

standardLubinTateUnitParameterToGal_mem_galoisParameterSubgroup_iff

L45 ↗

LubinTate.standardLubinTateUnitParameterToGal_mem_galoisParameterSubgroup_iff

Documentation

The explicit parameter-to-Galois map reflects membership in every transported parameter subgroup.

Source context 6 commands

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

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

Lean source · statement

theorem standardLubinTateUnitParameterToGal_mem_galoisParameterSubgroup_iff
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) (a : standardLubinTateUnitParameter F n) :
    standardLubinTateUnitParameterToGal F hπ n a ∈
        standardLubinTateGaloisParameterSubgroup F hπ n k ↔
      a ∈ standardLubinTateUnitParameterSubgroup F n k

theorem

standardLubinTateUnitParameterToGal_class_mem_galoisParameterSubgroup_iff

L71 ↗

LubinTate.standardLubinTateUnitParameterToGal_class_mem_galoisParameterSubgroup_iff

Documentation

On a valuation-ring unit representative, membership in the transported Galois subgroup is exactly membership in U_F^k.

Source context 6 commands

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

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

Lean source · statement

theorem
    standardLubinTateUnitParameterToGal_class_mem_galoisParameterSubgroup_iff
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) (hkn : k ≤ n + 1) (u : F.valuationSubringˣ) :
    standardLubinTateUnitParameterToGal F hπ n
          (standardLubinTateUnitParameterClass F n u) ∈
        standardLubinTateGaloisParameterSubgroup F hπ n k ↔
      u ∈ higherPrincipalUnitGroup F.toCompleteDVF k

def

standardLubinTateUnitParameterSubgroupEquivGaloisParameterSubgroup

L85 ↗

LubinTate.standardLubinTateUnitParameterSubgroupEquivGaloisParameterSubgroup

Documentation

Restricting the parameter-to-Galois homomorphism gives a multiplicative equivalence onto the transported subgroup.

Source context 6 commands

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

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

Lean source · statement

def
    standardLubinTateUnitParameterSubgroupEquivGaloisParameterSubgroup
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) :
    standardLubinTateUnitParameterSubgroup F n k ≃*
      standardLubinTateGaloisParameterSubgroup F hπ n k

theorem

standardLubinTateGaloisParameterSubgroup_natCard

L106 ↗

LubinTate.standardLubinTateGaloisParameterSubgroup_natCard

Documentation

The transported Galois filtration has the same cardinality as its finite unit-parameter source.

Source context 6 commands

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

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

Lean source · statement

theorem standardLubinTateGaloisParameterSubgroup_natCard
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1) :
    Nat.card (standardLubinTateGaloisParameterSubgroup F hπ n k) =
      Nat.card F.residueField ^ (n + 1 - k)

Module documentation

Principal-unit filtration on finite Lubin--Tate Galois groups

Declarations

standardLubinTateGaloisParameterSubgroup

standardLubinTateUnitParameterToGal_mem_galoisParameterSubgroup_iff

standardLubinTateUnitParameterToGal_class_mem_galoisParameterSubgroup_iff

standardLubinTateUnitParameterSubgroupEquivGaloisParameterSubgroup

standardLubinTateGaloisParameterSubgroup_natCard