NYLL
Module

Core.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.Core
12 declarations indexed from sourceView source ↗

Module documentation

Herbrand function and upper ramification groups of Lubin--Tate levels

The lower-group calculation is integrated here to compute the actual Herbrand function and the resulting upper ramification groups of the chosen equal-characteristic Lubin--Tate level.

Imports5
Imported by5

Declarations

theorem

equalCharacteristicLubinTateUnitParameterToGal_mem_lowerRamificationGroup_zero

L47 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterToGal_mem_lowerRamificationGroup_zero
Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
theorem
    equalCharacteristicLubinTateUnitParameterToGal_mem_lowerRamificationGroup_zero
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterToGal F n a ∈
      equalCharacteristicLubinTateRealLowerRamificationGroup F n 0
def

equalCharacteristicLubinTateUnitParameterEquivLowerRamificationGroupZero

L72 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterEquivLowerRamificationGroupZero
Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · full declaration
def
    equalCharacteristicLubinTateUnitParameterEquivLowerRamificationGroupZero
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateUnitParameter F n ≃
      equalCharacteristicLubinTateRealLowerRamificationGroup F n 0 where
  toFun a :=
    ⟨equalCharacteristicLubinTateUnitParameterToGal F n a,
      equalCharacteristicLubinTateUnitParameterToGal_mem_lowerRamificationGroup_zero
        F n a⟩
  invFun sigma :=
    (equalCharacteristicLubinTateUnitParameterEquivGal F n).symm sigma.1
  left_inv a :=
    (equalCharacteristicLubinTateUnitParameterEquivGal F n).symm_apply_apply a
  right_inv sigma := by
    apply Subtype.ext
    exact
      (equalCharacteristicLubinTateUnitParameterEquivGal F n).apply_symm_apply
        sigma.1
theorem

equalCharacteristicLubinTateRealLowerRamificationGroup_zero_natCard

L93 ↗
LubinTate.equalCharacteristicLubinTateRealLowerRamificationGroup_zero_natCard
Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
theorem equalCharacteristicLubinTateRealLowerRamificationGroup_zero_natCard
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    Nat.card (equalCharacteristicLubinTateRealLowerRamificationGroup F n 0) =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n
def

equalCharacteristicLubinTateLowerRamificationFiltration

L109 ↗
LubinTate.equalCharacteristicLubinTateLowerRamificationFiltration
Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
def
    equalCharacteristicLubinTateLowerRamificationFiltration
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
      Gal((equalCharacteristicLubinTateLevelField F n) /
        LaurentSeries F.residueField)
theorem

equalCharacteristicLubinTateHerbrandSlope_eq_of_pow_interval

L123 ↗
LubinTate.equalCharacteristicLubinTateHerbrandSlope_eq_of_pow_interval
Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
theorem equalCharacteristicLubinTateHerbrandSlope_eq_of_pow_interval
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k i : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (hlow : Nat.card F.residueField ^ (k - 1) ≤ i + 1)
    (hhigh : i + 1 < Nat.card F.residueField ^ k) :
    RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandSlope
        (equalCharacteristicLubinTateLowerRamificationFiltration F n) i =
      (Nat.card F.residueField ^ (n + 1 - k) : ℕ) /
        ((Nat.card F.residueField - 1) *
          Nat.card F.residueField ^ n : ℕ)
theorem

equalCharacteristicLubinTateHerbrandValueNat_pow_sub_one

L159 ↗
LubinTate.equalCharacteristicLubinTateHerbrandValueNat_pow_sub_one
Source context 14 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
open _root_.RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration
  (herbrandSlope) in
Lean source · statement
theorem equalCharacteristicLubinTateHerbrandValueNat_pow_sub_one
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ) (hkn : k ≤ n + 1) :
    RamificationTheory.DiscreteValuationField.AntitoneNormalSubgroupFiltration.herbrandValueNat
        (equalCharacteristicLubinTateLowerRamificationFiltration F n)
        (Nat.card F.residueField ^ k - 1) =
      (k : ℝ)
def

equalCharacteristicLubinTateHerbrandFunction

L263 ↗
LubinTate.equalCharacteristicLubinTateHerbrandFunction
Documentation

The Herbrand function of the chosen equal-characteristic Lubin--Tate level and its chosen complete discrete valuation.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
def equalCharacteristicLubinTateHerbrandFunction
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (s : ℝ) : ℝ
theorem

equalCharacteristicLubinTateHerbrandFunction_pow_sub_one

L276 ↗
LubinTate.equalCharacteristicLubinTateHerbrandFunction_pow_sub_one
Documentation

The lower endpoints q^k - 1 map to the integral upper endpoints k. This also includes the harmless endpoint k = 0.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
theorem equalCharacteristicLubinTateHerbrandFunction_pow_sub_one
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ) (hkn : k ≤ n + 1) :
    equalCharacteristicLubinTateHerbrandFunction F n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ) =
      (k : ℝ)
def

equalCharacteristicLubinTateRealUpperRamificationGroup

L296 ↗
LubinTate.equalCharacteristicLubinTateRealUpperRamificationGroup
Documentation

The actual real upper ramification group of the chosen equal-characteristic Lubin--Tate level valuation.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
def equalCharacteristicLubinTateRealUpperRamificationGroup
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (s : ℝ) :
    Subgroup Gal((equalCharacteristicLubinTateLevelField F n) /
      LaurentSeries F.residueField)
theorem

equalCharacteristicLubinTateRealUpperRamificationGroup_nat_eq_lower_pow_sub_one

L311 ↗
LubinTate.equalCharacteristicLubinTateRealUpperRamificationGroup_nat_eq_lower_pow_sub_one
Documentation

At an integral upper index k ≤ n + 1, the actual upper group is the actual lower group at q^k - 1.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
theorem
    equalCharacteristicLubinTateRealUpperRamificationGroup_nat_eq_lower_pow_sub_one
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ) (hkn : k ≤ n + 1) :
    equalCharacteristicLubinTateRealUpperRamificationGroup F n (k : ℝ) =
      equalCharacteristicLubinTateRealLowerRamificationGroup F n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)
theorem

equalCharacteristicLubinTateRealUpperRamificationGroup_natCard

L346 ↗
LubinTate.equalCharacteristicLubinTateRealUpperRamificationGroup_natCard
Documentation

For 1 ≤ k ≤ n + 1, the integral upper group has order q^(n + 1 - k).

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
theorem equalCharacteristicLubinTateRealUpperRamificationGroup_natCard
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1) :
    Nat.card
        (equalCharacteristicLubinTateRealUpperRamificationGroup
          F n (k : ℝ)) =
      Nat.card F.residueField ^ (n + 1 - k)
theorem

mem_equalCharacteristicLubinTateRealUpperRamificationGroup_nat_iff_coeff_zero

L362 ↗
LubinTate.mem_equalCharacteristicLubinTateRealUpperRamificationGroup_nat_iff_coeff_zero
Documentation

Parameter membership in the integral upper group is equivalent to vanishing of the first k visible coefficients.

Source context 13 commands

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

noncomputable section
open scoped LaurentSeries Pointwise PowerSeries
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
open RamificationTheory.HilbertRamification.Higher
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe u v y
variable {K : Type u} [Field K]
section ChosenRamificationTarget
variable {K₀ : Type} [Field K₀]
attribute [local instance]
  equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
  equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Lean source · statement
theorem
    mem_equalCharacteristicLubinTateRealUpperRamificationGroup_nat_iff_coeff_zero
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ) (hkn : k ≤ n + 1)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterToGal F n a ∈
        equalCharacteristicLubinTateRealUpperRamificationGroup
          F n (k : ℝ) ↔
      ∀ j < k,
        PowerSeries.coeff j
            (equalCharacteristicLubinTateUnitParameterSeries F n a - 1) = 0

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