NYLL
Module

LowerRamificationFormula.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.LowerRamificationFormula
6 declarations indexed from sourceView source ↗

Module documentation

Explicit lower ramification groups of finite Lubin--Tate levels

The displacement formula for a primitive Lubin--Tate point identifies the lower ramification filtration with the principal-unit filtration transported to the finite-level Galois group. At the break q ^ k - 1, and throughout the interval q ^ (k - 1) ≤ r < q ^ k, the group is the image of U_F^k. Its cardinality is therefore q ^ (n + 1 - k).

Imports3
Imported by2

Declarations

theorem

standardLubinTateUnitParameterToGal_displacement_addVal_ge_iff_mem_parameterSubgroup

L38 ↗
LubinTate.standardLubinTateUnitParameterToGal_displacement_addVal_ge_iff_mem_parameterSubgroup
Documentation

The primitive-point displacement threshold for a finite parameter is equivalent to membership in the corresponding finite principal-unit subgroup.

Source context 7 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem
    standardLubinTateUnitParameterToGal_displacement_addVal_ge_iff_mem_parameterSubgroup
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) (k : ℕ)
    (hkn : k ≤ n + 1) :
    ((Nat.card F.residueField ^ k : ℕ) : ℕ∞) ≤
        IsDiscreteValuationRing.addVal
          (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
          (valuationSubringAutOfUniqueExtension
              (standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
                hπ n)
              (standardLubinTateUnitParameterToGal F hπ n a)
              (standardLubinTatePrimitivePointInteger hπ n) -
            standardLubinTatePrimitivePointInteger hπ n) ↔
      a ∈ standardLubinTateUnitParameterSubgroup F n k
theorem

standardLubinTateRealLowerRamificationGroup_pow_sub_one_eq_galoisParameterSubgroup

L64 ↗
LubinTate.standardLubinTateRealLowerRamificationGroup_pow_sub_one_eq_galoisParameterSubgroup
Documentation

At the lower break q ^ k - 1, the real lower ramification group is the Galois image of the k-th finite principal-unit subgroup.

Source context 7 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem
    standardLubinTateRealLowerRamificationGroup_pow_sub_one_eq_galoisParameterSubgroup
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1) :
    standardLubinTateRealLowerRamificationGroup hπ n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ) =
      standardLubinTateGaloisParameterSubgroup F hπ n k
theorem

standardLubinTateRealLowerRamificationGroup_pow_sub_one_natCard

L87 ↗
LubinTate.standardLubinTateRealLowerRamificationGroup_pow_sub_one_natCard
Documentation

The lower ramification group at q ^ k - 1 has order q ^ (n + 1 - k).

Source context 7 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTateRealLowerRamificationGroup_pow_sub_one_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
        (standardLubinTateRealLowerRamificationGroup hπ n
          ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)) =
      Nat.card F.residueField ^ (n + 1 - k)
theorem

standardLubinTateUnitParameterToGal_interval_displacement_iff_mem_parameterSubgroup

L103 ↗
LubinTate.standardLubinTateUnitParameterToGal_interval_displacement_iff_mem_parameterSubgroup
Documentation

On a full power interval, the primitive-point displacement threshold for a finite parameter is equivalent to membership in the k-th finite principal-unit subgroup.

Source context 7 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem
    standardLubinTateUnitParameterToGal_interval_displacement_iff_mem_parameterSubgroup
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (a : standardLubinTateUnitParameter F n) (k r : ℕ)
    (hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (hlower : Nat.card F.residueField ^ (k - 1) ≤ r)
    (hupper : r < Nat.card F.residueField ^ k) :
    (((r + 1 : ℕ) : ℕ∞) ≤
        IsDiscreteValuationRing.addVal
          (standardLubinTateLevelCompleteDVF hπ n).valuationSubring
          (valuationSubringAutOfUniqueExtension
              (standardLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
                hπ n)
              (standardLubinTateUnitParameterToGal F hπ n a)
              (standardLubinTatePrimitivePointInteger hπ n) -
            standardLubinTatePrimitivePointInteger hπ n)) ↔
      a ∈ standardLubinTateUnitParameterSubgroup F n k
theorem

standardLubinTateRealLowerRamificationGroup_eq_galoisParameterSubgroup_of_pow_interval

L133 ↗
LubinTate.standardLubinTateRealLowerRamificationGroup_eq_galoisParameterSubgroup_of_pow_interval
Documentation

Throughout q ^ (k - 1) ≤ r < q ^ k, the real lower ramification group is the Galois image of the k-th finite principal-unit subgroup.

Source context 7 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem
    standardLubinTateRealLowerRamificationGroup_eq_galoisParameterSubgroup_of_pow_interval
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k r : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (hlower : Nat.card F.residueField ^ (k - 1) ≤ r)
    (hupper : r < Nat.card F.residueField ^ k) :
    standardLubinTateRealLowerRamificationGroup hπ n (r : ℝ) =
      standardLubinTateGaloisParameterSubgroup F hπ n k
theorem

standardLubinTateRealLowerRamificationGroup_natCard_of_pow_interval

L152 ↗
LubinTate.standardLubinTateRealLowerRamificationGroup_natCard_of_pow_interval
Documentation

Throughout a full power interval, the real lower ramification group has order q ^ (n + 1 - k).

Source context 7 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem
    standardLubinTateRealLowerRamificationGroup_natCard_of_pow_interval
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k r : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (hlower : Nat.card F.residueField ^ (k - 1) ≤ r)
    (hupper : r < Nat.card F.residueField ^ k) :
    Nat.card
        (standardLubinTateRealLowerRamificationGroup hπ n (r : ℝ)) =
      Nat.card F.residueField ^ (n + 1 - k)

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