Module

FiniteParameterFiltration.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.FiniteParameterFiltration

3 declarations indexed from sourceView source ↗

Module documentation

Principal-unit filtration on finite Lubin--Tate parameters

The parameter group at primitive level n + 1 is O_Fˣ / U_F^(n + 1). The image of U_F^k gives its natural decreasing filtration. For 1 ≤ k ≤ n + 1, that image has cardinality q ^ (n + 1 - k).

Imports1

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.FiniteParameters

Imported by2

def

standardLubinTateUnitParameterSubgroup

L33 ↗

LubinTate.standardLubinTateUnitParameterSubgroup

Documentation

The image of the k-th higher principal-unit group in the finite parameter quotient at primitive level n + 1.

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 standardLubinTateUnitParameterSubgroup
    (F : LocalField.{u, v} K) (n k : ℕ) :
    Subgroup (standardLubinTateUnitParameter F n)

theorem

standardLubinTateUnitParameterClass_mem_subgroup_iff

L42 ↗

LubinTate.standardLubinTateUnitParameterClass_mem_subgroup_iff

Documentation

A represented finite parameter belongs to the k-th parameter subgroup exactly when its representative lies 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 standardLubinTateUnitParameterClass_mem_subgroup_iff
    (F : LocalField.{u, v} K) (n k : ℕ) (hk : k ≤ n + 1)
    (u : F.valuationSubringˣ) :
    standardLubinTateUnitParameterClass F n u ∈
        standardLubinTateUnitParameterSubgroup F n k ↔
      u ∈ higherPrincipalUnitGroup F.toCompleteDVF k

theorem

standardLubinTateUnitParameterSubgroup_natCard

L62 ↗

LubinTate.standardLubinTateUnitParameterSubgroup_natCard

Documentation

The k-th finite parameter subgroup has cardinality q ^ (n + 1 - k) throughout the principal-unit range.

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 standardLubinTateUnitParameterSubgroup_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 (standardLubinTateUnitParameterSubgroup F n k) =
      Nat.card F.residueField ^ (n + 1 - k)

Module documentation

Principal-unit filtration on finite Lubin--Tate parameters

Declarations

standardLubinTateUnitParameterSubgroup

standardLubinTateUnitParameterClass_mem_subgroup_iff

standardLubinTateUnitParameterSubgroup_natCard