Module

EqualCharacteristicUpperFiltration.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.LubinTateApplication.EqualCharacteristicUpperFiltration

6 declarations indexed from sourceView source ↗

Module documentation

Equal-characteristic Lubin--Tate upper filtration

This file identifies the image of the k-th higher-unit subgroup under the explicit finite-level Artin map a ↦ [a⁻¹] with the actual upper ramification group G^k.

Imports5

Imported by1

Nyll.ClassFieldTheory.LocalClassFieldTheory.LubinTateApplication.All

def

artinUnitParameter

L39 ↗

LocalClassFieldTheory.artinUnitParameter

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
variable {K : Type u} [Field K]

Lean source · statement

def artinUnitParameter
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateUnitParameter F n

theorem

artinUnitParameter_coeff

L48 ↗

LocalClassFieldTheory.artinUnitParameter_coeff

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
variable {K : Type u} [Field K]

Lean source · statement

theorem artinUnitParameter_coeff
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : F.residueField⟦X⟧ˣ) (j : ℕ) (hj : j ≤ n) :
    PowerSeries.coeff j
        (equalCharacteristicLubinTateUnitParameterSeries F n
          (artinUnitParameter F n a)) =
      PowerSeries.coeff j (a : F.residueField⟦X⟧)

theorem

artinUnitParameter_reduction

L73 ↗

LocalClassFieldTheory.artinUnitParameter_reduction

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
variable {K : Type u} [Field K]

Lean source · statement

theorem artinUnitParameter_reduction
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateUnitReduction F n
        (equalCharacteristicLubinTateUnitParameterUnit F n
          (artinUnitParameter F n a)) =
      equalCharacteristicLubinTateUnitReduction F n a

theorem

artinUnitToGal_eq_parameter

L93 ↗

LocalClassFieldTheory.artinUnitToGal_eq_parameter

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
variable {K : Type u} [Field K]

Lean source · statement

theorem artinUnitToGal_eq_parameter
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : F.residueField⟦X⟧ˣ) :
    equalCharacteristicLubinTateArtinUnitToGal F n a =
      equalCharacteristicLubinTateUnitParameterToGal F n
        (artinUnitParameter F n a⁻¹)

theorem

mem_span_X_pow_iff_coeff_zero

L132 ↗

LocalClassFieldTheory.mem_span_X_pow_iff_coeff_zero

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
variable {K : Type u} [Field K]

Lean source · statement

theorem mem_span_X_pow_iff_coeff_zero
    {k : Type u} [Field k] (f : k⟦X⟧) (m : ℕ) :
    f ∈ Ideal.span ({PowerSeries.X ^ m} : Set k⟦X⟧) ↔
      ∀ j < m, PowerSeries.coeff j f = 0

theorem

equalCharacteristicLubinTateArtinHigherUnitImage_eq_upper

L139 ↗

LocalClassFieldTheory.equalCharacteristicLubinTateArtinHigherUnitImage_eq_upper

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries PowerSeries
universe u v
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalFieldTheory.DiscreteValuationField
open LubinTate.EqualCharacteristic
variable {K : Type u} [Field K]

Lean source · statement

theorem equalCharacteristicLubinTateArtinHigherUnitImage_eq_upper
    {K₀ : Type} [Field K₀]
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1) :
    (equalCharacteristicLubinTateHigherUnitSubgroup F (k - 1)).map
        (equalCharacteristicLubinTateArtinUnitToGal F n) =
      equalCharacteristicLubinTateRealUpperRamificationGroup F n (k : ℝ)

Module documentation

Equal-characteristic Lubin--Tate upper filtration

Declarations

artinUnitParameter

artinUnitParameter_coeff

artinUnitParameter_reduction

artinUnitToGal_eq_parameter

mem_span_X_pow_iff_coeff_zero

equalCharacteristicLubinTateArtinHigherUnitImage_eq_upper