NYLL
Module

RealIndexSteps.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.RealIndexSteps
7 declarations indexed from sourceView source ↗

Module documentation

Real-index steps for equal-characteristic Lubin--Tate levels

This file packages the ceiling behavior of the chosen real lower filtration and the integral values of its inverse Herbrand function. Together they show that, on the positive range covered by an explicit finite Lubin--Tate level, the real upper filtration is constant on the natural-ceiling steps.

Imports2
Imported by4

Declarations

instance

equalCharacteristicLubinTateLevelField_finiteDimensional_forRealIndexSteps

L37 ↗
LubinTate.equalCharacteristicLubinTateLevelField_finiteDimensional_forRealIndexSteps
Documentation

Finite-dimensionality for explicit levels while forming the real-index Herbrand functions in this module.

Source context 8 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
open LubinTate.EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
universe v
variable {K₀ : Type} [Field K₀]
Lean source · statement
instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)
instance

equalCharacteristicLubinTateLevelField_isGalois_forRealIndexSteps

L48 ↗
LubinTate.equalCharacteristicLubinTateLevelField_isGalois_forRealIndexSteps
Documentation

Galoisness for explicit levels while forming the real-index Herbrand functions in this module.

Source context 9 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
open LubinTate.EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
universe v
variable {K₀ : Type} [Field K₀]
/-- Finite-dimensionality for explicit levels while forming the real-index
Herbrand functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
Lean source · statement
instance
    equalCharacteristicLubinTateLevelField_isGalois_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)
theorem

equalCharacteristicLubinTateRealLowerRamificationGroup_eq_natCeil

L59 ↗
LubinTate.equalCharacteristicLubinTateRealLowerRamificationGroup_eq_natCeil
Documentation

At a nonnegative real lower index, the chosen equal-characteristic Lubin--Tate lower group is the group at the natural-number ceiling.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
open LubinTate.EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
universe v
variable {K₀ : Type} [Field K₀]
/-- Finite-dimensionality for explicit levels while forming the real-index
Herbrand functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for explicit levels while forming the real-index Herbrand
functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem
    equalCharacteristicLubinTateRealLowerRamificationGroup_eq_natCeil
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (s : ℝ) (hs : 0 ≤ s) :
    equalCharacteristicLubinTateRealLowerRamificationGroup F n s =
      equalCharacteristicLubinTateRealLowerRamificationGroup
        F n (⌈s⌉₊ : ℝ)
def

equalCharacteristicLubinTateInverseHerbrandFunction

L95 ↗
LubinTate.equalCharacteristicLubinTateInverseHerbrandFunction
Documentation

The inverse Herbrand function attached to the chosen complete-DVF structure on an equal-characteristic Lubin--Tate level.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
open LubinTate.EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
universe v
variable {K₀ : Type} [Field K₀]
/-- Finite-dimensionality for explicit levels while forming the real-index
Herbrand functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for explicit levels while forming the real-index Herbrand
functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
def equalCharacteristicLubinTateInverseHerbrandFunction
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (t : ℝ) : ℝ
theorem

equalCharacteristicLubinTateInverseHerbrandFunction_nat_eq_pow_sub_one

L108 ↗
LubinTate.equalCharacteristicLubinTateInverseHerbrandFunction_nat_eq_pow_sub_one
Documentation

At every integral upper endpoint visible at level n + 1, the chosen inverse Herbrand function returns the lower endpoint q^k - 1.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
open LubinTate.EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
universe v
variable {K₀ : Type} [Field K₀]
/-- Finite-dimensionality for explicit levels while forming the real-index
Herbrand functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for explicit levels while forming the real-index Herbrand
functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem
    equalCharacteristicLubinTateInverseHerbrandFunction_nat_eq_pow_sub_one
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ) (hkn : k ≤ n + 1) :
    equalCharacteristicLubinTateInverseHerbrandFunction F n (k : ℝ) =
      ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)
theorem

equalCharacteristicLubinTateRealLowerRamificationGroup_nat_eq_pow_sub_one_of_pow_interval

L130 ↗
LubinTate.equalCharacteristicLubinTateRealLowerRamificationGroup_nat_eq_pow_sub_one_of_pow_interval
Documentation

On a lower-numbering power interval, the chosen lower group is the group at the right endpoint q^k - 1.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
open LubinTate.EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
universe v
variable {K₀ : Type} [Field K₀]
/-- Finite-dimensionality for explicit levels while forming the real-index
Herbrand functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for explicit levels while forming the real-index Herbrand
functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem
    equalCharacteristicLubinTateRealLowerRamificationGroup_nat_eq_pow_sub_one_of_pow_interval
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k r : ℕ) (hk : 1 ≤ k)
    (hlow : Nat.card F.residueField ^ (k - 1) ≤ r)
    (hhigh : r < Nat.card F.residueField ^ k) :
    equalCharacteristicLubinTateRealLowerRamificationGroup F n (r : ℝ) =
      equalCharacteristicLubinTateRealLowerRamificationGroup F n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)
theorem

equalCharacteristicLubinTateRealUpperRamificationGroup_eq_natCeil

L158 ↗
LubinTate.equalCharacteristicLubinTateRealUpperRamificationGroup_eq_natCeil
Documentation

On the positive range visible at level n + 1, the chosen real upper filtration is the natural-ceiling step extension of its integral values.

Source context 10 commands

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

noncomputable section
open scoped LaurentSeries
namespace LubinTate
open LubinTate.EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
universe v
variable {K₀ : Type} [Field K₀]
/-- Finite-dimensionality for explicit levels while forming the real-index
Herbrand functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for explicit levels while forming the real-index Herbrand
functions in this module. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forRealIndexSteps
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · statement
theorem
    equalCharacteristicLubinTateRealUpperRamificationGroup_eq_natCeil
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (t : ℝ)
    (hk : 1 ≤ ⌈t⌉₊) (hkn : ⌈t⌉₊ ≤ n + 1) :
    equalCharacteristicLubinTateRealUpperRamificationGroup F n t =
      equalCharacteristicLubinTateRealUpperRamificationGroup
        F n (⌈t⌉₊ : ℝ)

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