NYLL
Module

LowerGroups.lean

Nyll.ClassFieldTheory.LubinTate.EqualCharacteristic.Ramification.LowerGroups
26 declarations indexed from sourceView source ↗

Module documentation

Lower ramification groups of equal-characteristic Lubin--Tate levels

This module identifies the actual lower ramification groups attached to the chosen complete valuation, both by visible unit-parameter coefficients and by their exact cardinalities.

Imports4
Imported by2

Declarations

def

equalCharacteristicLubinTateRealLowerRamificationGroup

L45 ↗
LubinTate.equalCharacteristicLubinTateRealLowerRamificationGroup
Documentation

The actual real lower ramification group of the explicit equal-characteristic Lubin--Tate level, formed from the chosen integral-closure valuation.

Source context 12 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₀]
Lean source · statement
def equalCharacteristicLubinTateRealLowerRamificationGroup
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) (s : ℝ) :
    Subgroup Gal((equalCharacteristicLubinTateLevelField F n) /
      F.residueField⸨X⸩)
instance

equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups

L60 ↗
LubinTate.equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
Documentation

Finite-dimensionality for the explicit level while computing its lower ramification groups.

Source context 12 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₀]
Lean source · statement
instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)
instance

equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups

L71 ↗
LubinTate.equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
Documentation

Galoisness for the explicit level while computing its lower ramification groups.

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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (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_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n)
theorem

mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_primitivePoint

L83 ↗
LubinTate.mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_primitivePoint
Documentation

At a natural lower index, membership in the actual Lubin--Tate lower ramification group is detected by the displacement of its primitive uniformizer alone.

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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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
    mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_primitivePoint
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n i : ℕ)
    (sigma : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩)) :
    sigma ∈ equalCharacteristicLubinTateRealLowerRamificationGroup
        F n (i : ℝ) ↔
      ((i + 1 : ℕ) : ℕ∞) ≤
        IsDiscreteValuationRing.addVal
          (equalCharacteristicLubinTateLevelCompleteDVF F n).valuationSubring
          (valuationSubringAutOfUniqueExtension
              (equalCharacteristicLubinTateLevelCompleteDVF_hasUniqueDVFValuationExtension
                F n)
              sigma (equalCharacteristicLubinTatePrimitivePointInteger F n) -
            equalCharacteristicLubinTatePrimitivePointInteger F n)
theorem

mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_parameterPower_of_ne_one

L151 ↗
LubinTate.mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_parameterPower_of_ne_one
Documentation

Elementwise lower-ramification form: if a nonidentity automorphism first differs from the identity unit parameter in degree k, then it belongs to the natural lower group G_i exactly when i + 1 ≤ q^k.

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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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
    mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_parameterPower_of_ne_one
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n i : ℕ)
    (sigma : Gal((equalCharacteristicLubinTateLevelField F n)/F.residueField⸨X⸩))
    (a : equalCharacteristicLubinTateUnitParameter F n)
    (ha :
      sigma (equalCharacteristicLubinTateLevelPowerBasis F n).gen =
        equalCharacteristicLubinTateLevelBracket F n (n + 1)
          (equalCharacteristicLubinTateUnitParameterSeries F n a)
          (equalCharacteristicLubinTateLevelPowerBasis F n).gen)
    (hsigma : sigma ≠ 1) :
    sigma ∈ equalCharacteristicLubinTateRealLowerRamificationGroup
        F n (i : ℝ) ↔
      ((i + 1 : ℕ) : ℕ∞) ≤
        (Nat.card F.residueField ^
          (equalCharacteristicLubinTateUnitParameterSeries F n a - 1).order.toNat :
            ℕ)
def

equalCharacteristicLubinTateUnitParameterEquivGal

L178 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterEquivGal
Documentation

The explicit finite unit-parameter bijection with the Galois group of the chosen equal-characteristic Lubin--Tate level.

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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateUnitParameterEquivGal
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateUnitParameter F n ≃
      Gal((equalCharacteristicLubinTateLevelField F n) /
        LaurentSeries F.residueField)
theorem

equalCharacteristicLubinTateUnitParameterEquivGal_apply

L191 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterEquivGal_apply
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateUnitParameterEquivGal_apply
    (F : LocalField.{u, v} K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterEquivGal F n a =
      equalCharacteristicLubinTateUnitParameterToGal F n a
theorem

mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_parameterPower

L202 ↗
LubinTate.mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_parameterPower
Documentation

For the automorphism attached to a finite unit parameter, membership in a natural lower group is the parameter-power inequality, with the identity case included explicitly and no side hypotheses.

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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_parameterPower
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n i : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterToGal F n a ∈
        equalCharacteristicLubinTateRealLowerRamificationGroup F n (i : ℝ) ↔
      equalCharacteristicLubinTateUnitParameterToGal F n a = 1 ∨
        ((i + 1 : ℕ) : ℕ∞) ≤
          (Nat.card F.residueField ^
            (equalCharacteristicLubinTateUnitParameterSeries F n a - 1).order.toNat :
              ℕ)
def

equalCharacteristicLubinTateOneUnitParameter

L240 ↗
LubinTate.equalCharacteristicLubinTateOneUnitParameter
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateOneUnitParameter
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicLubinTateUnitParameter F n
theorem

equalCharacteristicLubinTateOneUnitParameterSeries

L246 ↗
LubinTate.equalCharacteristicLubinTateOneUnitParameterSeries
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateOneUnitParameterSeries
    (F : LocalField.{u, v} K) (n : ℕ) :
    equalCharacteristicLubinTateUnitParameterSeries F n
        (equalCharacteristicLubinTateOneUnitParameter F n) = 1
theorem

equalCharacteristicLubinTateOneUnitParameterToGal

L267 ↗
LubinTate.equalCharacteristicLubinTateOneUnitParameterToGal
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateOneUnitParameterToGal
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    equalCharacteristicLubinTateUnitParameterToGal F n
        (equalCharacteristicLubinTateOneUnitParameter F n) = 1
theorem

equalCharacteristicLubinTateUnitParameterToGal_eq_one_iff

L295 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterToGal_eq_one_iff
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateUnitParameterToGal_eq_one_iff
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterToGal F n a = 1 ↔
      a = equalCharacteristicLubinTateOneUnitParameter F n
theorem

equalCharacteristicLubinTateUnitParameterSeries_sub_one_eq_zero_iff

L310 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterSeries_sub_one_eq_zero_iff
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateUnitParameterSeries_sub_one_eq_zero_iff
    (F : LocalField.{u, v} K)
    (n : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterSeries F n a - 1 = 0 ↔
      a = equalCharacteristicLubinTateOneUnitParameter F n
theorem

mem_equalCharacteristicLubinTateRealLowerRamificationGroup_pow_sub_one_iff_coeff_zero

L329 ↗
LubinTate.mem_equalCharacteristicLubinTateRealLowerRamificationGroup_pow_sub_one_iff_coeff_zero
Documentation

At the lower endpoint q^k - 1, membership is equivalent to vanishing of the first k coefficients of the visible difference from the identity.

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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 mem_equalCharacteristicLubinTateRealLowerRamificationGroup_pow_sub_one_iff_coeff_zero
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterToGal F n a ∈
        equalCharacteristicLubinTateRealLowerRamificationGroup F n
          ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ) ↔
      ∀ j < k,
        PowerSeries.coeff j
            (equalCharacteristicLubinTateUnitParameterSeries F n a - 1) = 0
def

equalCharacteristicLubinTateUnitParameterVanishesBefore

L402 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterVanishesBefore
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateUnitParameterVanishesBefore
    (F : LocalField.{u, v} K) (n k : ℕ)
    (a : equalCharacteristicLubinTateUnitParameter F n) : Prop
theorem

equalCharacteristicLubinTateUnitParameter_coeff_zero_iff_vanishesBefore

L408 ↗
LubinTate.equalCharacteristicLubinTateUnitParameter_coeff_zero_iff_vanishesBefore
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateUnitParameter_coeff_zero_iff_vanishesBefore
    (F : LocalField.{u, v} K)
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    (∀ j < k,
        PowerSeries.coeff j
            (equalCharacteristicLubinTateUnitParameterSeries F n a - 1) = 0) ↔
      equalCharacteristicLubinTateUnitParameterVanishesBefore
        F n k a
def

equalCharacteristicLubinTateTailIndex

L456 ↗
LubinTate.equalCharacteristicLubinTateTailIndex
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateTailIndex
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (j : Fin (n + 1 - k)) : Fin n
def

equalCharacteristicLubinTateTailOffset

L461 ↗
LubinTate.equalCharacteristicLubinTateTailOffset
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateTailOffset
    (n k : ℕ) (_hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (i : Fin n) (hi : k ≤ i.val + 1) : Fin (n + 1 - k)
theorem

equalCharacteristicLubinTateTailIndex_offset

L466 ↗
LubinTate.equalCharacteristicLubinTateTailIndex_offset
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateTailIndex_offset
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (i : Fin n) (hi : k ≤ i.val + 1) :
    equalCharacteristicLubinTateTailIndex n k hk hkn
        (equalCharacteristicLubinTateTailOffset n k hk hkn i hi) = i
theorem

equalCharacteristicLubinTateTailOffset_index

L476 ↗
LubinTate.equalCharacteristicLubinTateTailOffset_index
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · full declaration
theorem equalCharacteristicLubinTateTailOffset_index
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (j : Fin (n + 1 - k)) :
    equalCharacteristicLubinTateTailOffset n k hk hkn
        (equalCharacteristicLubinTateTailIndex n k hk hkn j)
        (by
          simp [equalCharacteristicLubinTateTailIndex]
          omega) = j := by
  apply Fin.ext
  simp [equalCharacteristicLubinTateTailIndex,
    equalCharacteristicLubinTateTailOffset]
  omega
def

equalCharacteristicLubinTateUnitParameterVanishesBeforeEquiv

L489 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterVanishesBeforeEquiv
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · full declaration
def equalCharacteristicLubinTateUnitParameterVanishesBeforeEquiv
    (F : LocalField.{u, v} K)
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1) :
    {a : equalCharacteristicLubinTateUnitParameter F n //
      equalCharacteristicLubinTateUnitParameterVanishesBefore
        F n k a} ≃
      (Fin (n + 1 - k) → F.residueField) where
  toFun a j :=
    a.1.higherCoeff
      (equalCharacteristicLubinTateTailIndex n k hk hkn j)
  invFun g :=
    ⟨equalCharacteristicLubinTateUnitParameterOfCoefficients F n 1
        (fun i =>
          if hi : k ≤ i.val + 1 then
            g (equalCharacteristicLubinTateTailOffset
              n k hk hkn i hi)
          else 0),
      by
        constructor
        · rfl
        · intro i hi
          simp [equalCharacteristicLubinTateUnitParameterOfCoefficients,
            not_le.mpr hi]⟩
  left_inv a := by
    apply Subtype.ext
    apply equalCharacteristicLubinTateUnitParameter_ext F n
    · change 1 = a.1.constantUnit
      exact a.2.1.symm
    · funext i
      by_cases hi : k ≤ i.val + 1
      · change
          (if h : k ≤ i.val + 1 then
              a.1.higherCoeff
                (equalCharacteristicLubinTateTailIndex n k hk hkn
                  (equalCharacteristicLubinTateTailOffset
                    n k hk hkn i h))
            else 0) =
            a.1.higherCoeff i
        rw [dite_eq_left hi,
          equalCharacteristicLubinTateTailIndex_offset
            n k hk hkn i]
      · change
          (if h : k ≤ i.val + 1 then
              a.1.higherCoeff
                (equalCharacteristicLubinTateTailIndex n k hk hkn
                  (equalCharacteristicLubinTateTailOffset
                    n k hk hkn i h))
            else 0) =
            a.1.higherCoeff i
        rw [dite_eq_right hi]
        exact (a.2.2 i (Nat.lt_of_not_ge hi)).symm
  right_inv g := by
    funext j
    change
      (if hi :
          k ≤
            (equalCharacteristicLubinTateTailIndex
              n k hk hkn j).val + 1 then
          g (equalCharacteristicLubinTateTailOffset n k hk hkn
            (equalCharacteristicLubinTateTailIndex
              n k hk hkn j) hi)
        else 0) = g j
    have hi :
        k ≤
          (equalCharacteristicLubinTateTailIndex
            n k hk hkn j).val + 1 := by
      simp [equalCharacteristicLubinTateTailIndex]
      omega
    rw [dite_eq_left hi,
      equalCharacteristicLubinTateTailOffset_index n k hk hkn j]
theorem

equalCharacteristicLubinTateUnitParameterVanishesBefore_natCard

L560 ↗
LubinTate.equalCharacteristicLubinTateUnitParameterVanishesBefore_natCard
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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 equalCharacteristicLubinTateUnitParameterVanishesBefore_natCard
    (F : LocalField.{u, v} K)
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1) :
    Nat.card
        {a : equalCharacteristicLubinTateUnitParameter F n //
          equalCharacteristicLubinTateUnitParameterVanishesBefore
            F n k a} =
      Nat.card F.residueField ^ (n + 1 - k)
def

equalCharacteristicLubinTateRealLowerRamificationGroupEquivVanishesBefore

L573 ↗
LubinTate.equalCharacteristicLubinTateRealLowerRamificationGroupEquivVanishesBefore
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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    IsGalois F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_isGalois F n
Lean source · full declaration
def
    equalCharacteristicLubinTateRealLowerRamificationGroupEquivVanishesBefore
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1) :
    equalCharacteristicLubinTateRealLowerRamificationGroup F n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ) ≃
      {a : equalCharacteristicLubinTateUnitParameter F n //
        equalCharacteristicLubinTateUnitParameterVanishesBefore
          F n k a} where
  toFun sigma := by
    let e := equalCharacteristicLubinTateUnitParameterEquivGal F n
    let a := e.symm sigma.1
    refine ⟨a, ?_⟩
    apply
      (equalCharacteristicLubinTateUnitParameter_coeff_zero_iff_vanishesBefore
        F n k hk hkn a).mp
    apply
      (mem_equalCharacteristicLubinTateRealLowerRamificationGroup_pow_sub_one_iff_coeff_zero
        F n k a).mp
    change e (e.symm sigma.1) ∈
      equalCharacteristicLubinTateRealLowerRamificationGroup F n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)
    simpa using sigma.2
  invFun a := by
    let e := equalCharacteristicLubinTateUnitParameterEquivGal F n
    refine ⟨e a.1, ?_⟩
    change equalCharacteristicLubinTateUnitParameterToGal F n a.1 ∈
      equalCharacteristicLubinTateRealLowerRamificationGroup F n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)
    apply
      (mem_equalCharacteristicLubinTateRealLowerRamificationGroup_pow_sub_one_iff_coeff_zero
        F n k a.1).mpr
    exact
      (equalCharacteristicLubinTateUnitParameter_coeff_zero_iff_vanishesBefore
        F n k hk hkn a.1).mpr a.2
  left_inv sigma := by
    apply Subtype.ext
    exact
      (equalCharacteristicLubinTateUnitParameterEquivGal F n).apply_symm_apply
        sigma.1
  right_inv a := by
    apply Subtype.ext
    exact
      (equalCharacteristicLubinTateUnitParameterEquivGal F n).symm_apply_apply
        a.1
theorem

equalCharacteristicLubinTateRealLowerRamificationGroup_natCard_pow_sub_one

L622 ↗
LubinTate.equalCharacteristicLubinTateRealLowerRamificationGroup_natCard_pow_sub_one
Documentation

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

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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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_natCard_pow_sub_one
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1) :
    Nat.card
        (equalCharacteristicLubinTateRealLowerRamificationGroup F n
          ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)) =
      Nat.card F.residueField ^ (n + 1 - k)
theorem

mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_coeff_zero_of_pow_interval

L638 ↗
LubinTate.mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_coeff_zero_of_pow_interval
Documentation

On the whole interval q^(k-1) ≤ r < q^k, lower-group membership is controlled by the same first-k coefficient condition.

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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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
  mem_equalCharacteristicLubinTateRealLowerRamificationGroup_nat_iff_coeff_zero_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)
    (a : equalCharacteristicLubinTateUnitParameter F n) :
    equalCharacteristicLubinTateUnitParameterToGal F n a ∈
        equalCharacteristicLubinTateRealLowerRamificationGroup F n (r : ℝ) ↔
      ∀ j < k,
        PowerSeries.coeff j
            (equalCharacteristicLubinTateUnitParameterSeries F n a - 1) = 0
theorem

equalCharacteristicLubinTateRealLowerRamificationGroup_natCard_of_pow_interval

L719 ↗
LubinTate.equalCharacteristicLubinTateRealLowerRamificationGroup_natCard_of_pow_interval
Documentation

The lower-group order is constant on q^(k-1) ≤ r < q^k.

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₀]
/-- Finite-dimensionality for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_finiteDimensional_forLowerGroups
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n : ℕ) :
    FiniteDimensional F.residueField⸨X⸩
      (equalCharacteristicLubinTateLevelField F n) :=
  equalCharacteristicLubinTateLevelField_finiteDimensional F n
/-- Galoisness for the explicit level while computing its lower
ramification groups. -/
noncomputable local instance
    equalCharacteristicLubinTateLevelField_isGalois_forLowerGroups
    (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_natCard_of_pow_interval
    (F : LocalField.{0, v} K₀)
    [CharP K₀ F.residueCharacteristic]
    (n k r : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1)
    (hlow : Nat.card F.residueField ^ (k - 1) ≤ r)
    (hhigh : r < Nat.card F.residueField ^ k) :
    Nat.card
        (equalCharacteristicLubinTateRealLowerRamificationGroup F 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.