Module

HerbrandFormula.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.HerbrandFormula

16 declarations indexed from sourceView source ↗

Module documentation

Herbrand formula for finite Lubin--Tate levels

The explicit lower ramification groups determine the slopes of the Herbrand function. Summing those slopes sends the lower breaks q ^ k - 1 to the integral upper breaks k. Consequently the upper ramification group at k is the Galois image of the k-th principal-unit subgroup and has order q ^ (n + 1 - k).

Imports2

Imported by2

instance

standardLubinTateLevelField_finiteDimensional_forHerbrandFormula

L35 ↗

LubinTate.standardLubinTateLevelField_finiteDimensional_forHerbrandFormula

Source context 8 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]

Lean source · statement

instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n)

instance

standardLubinTateLevelField_isGalois_forHerbrandFormula

L42 ↗

LubinTate.standardLubinTateLevelField_isGalois_forHerbrandFormula

Source context 9 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n

Lean source · statement

instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n)

theorem

standardLubinTateUnitParameterSubgroup_zero_eq_top

L49 ↗

LubinTate.standardLubinTateUnitParameterSubgroup_zero_eq_top

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateUnitParameterSubgroup_zero_eq_top
    (F : LocalField.{u, v} K) (n : ℕ) :
    standardLubinTateUnitParameterSubgroup F n 0 = ⊤

theorem

standardLubinTateRealLowerRamificationGroup_zero_eq_top

L61 ↗

LubinTate.standardLubinTateRealLowerRamificationGroup_zero_eq_top

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateRealLowerRamificationGroup_zero_eq_top
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    standardLubinTateRealLowerRamificationGroup hπ n 0 = ⊤

theorem

standardLubinTateRealLowerRamificationGroup_zero_natCard

L83 ↗

LubinTate.standardLubinTateRealLowerRamificationGroup_zero_natCard

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateRealLowerRamificationGroup_zero_natCard
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) :
    Nat.card (standardLubinTateRealLowerRamificationGroup hπ n 0) =
      (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n

theorem

standardLubinTateHerbrandSlope_eq_of_pow_interval

L97 ↗

LubinTate.standardLubinTateHerbrandSlope_eq_of_pow_interval

Documentation

On a lower-numbering power interval, the Herbrand slope is the ratio of the corresponding lower-group order to the inertia-group order.

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateHerbrandSlope_eq_of_pow_interval
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (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) :
    AntitoneNormalSubgroupFiltration.herbrandSlope
        (standardLubinTateLowerRamificationFiltration hπ n) i =
      (Nat.card F.residueField ^ (n + 1 - k) : ℕ) /
        ((Nat.card F.residueField - 1) *
          Nat.card F.residueField ^ n : ℕ)

theorem

standardLubinTateHerbrandValueNat_pow_sub_one

L128 ↗

LubinTate.standardLubinTateHerbrandValueNat_pow_sub_one

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateHerbrandValueNat_pow_sub_one
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) (hkn : k ≤ n + 1) :
    AntitoneNormalSubgroupFiltration.herbrandValueNat
        (standardLubinTateLowerRamificationFiltration hπ n)
        (Nat.card F.residueField ^ k - 1) =
      (k : ℝ)

theorem

standardLubinTateHerbrandFunction_pow_sub_one

L231 ↗

LubinTate.standardLubinTateHerbrandFunction_pow_sub_one

Documentation

The lower endpoints q ^ k - 1 map to the integral upper endpoints k, including the endpoint k = 0.

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateHerbrandFunction_pow_sub_one
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) (hkn : k ≤ n + 1) :
    standardLubinTateHerbrandFunction hπ n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ) =
      (k : ℝ)

theorem

standardLubinTateInverseHerbrandFunction_nat_eq_pow_sub_one

L249 ↗

LubinTate.standardLubinTateInverseHerbrandFunction_nat_eq_pow_sub_one

Documentation

At an integral upper endpoint, the 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
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateInverseHerbrandFunction_nat_eq_pow_sub_one
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) (hkn : k ≤ n + 1) :
    standardLubinTateInverseHerbrandFunction hπ n (k : ℝ) =
      ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)

theorem

standardLubinTateRealUpperRamificationGroup_nat_eq_lower_pow_sub_one

L270 ↗

LubinTate.standardLubinTateRealUpperRamificationGroup_nat_eq_lower_pow_sub_one

Documentation

At an integral upper index, the upper group is the lower group at the corresponding power break.

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem
    standardLubinTateRealUpperRamificationGroup_nat_eq_lower_pow_sub_one
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) (hkn : k ≤ n + 1) :
    standardLubinTateRealUpperRamificationGroup hπ n (k : ℝ) =
      standardLubinTateRealLowerRamificationGroup hπ n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)

theorem

standardLubinTateRealUpperRamificationGroup_nat_eq_galoisParameterSubgroup

L285 ↗

LubinTate.standardLubinTateRealUpperRamificationGroup_nat_eq_galoisParameterSubgroup

Documentation

For 1 ≤ k ≤ n + 1, the integral upper group is the Galois image of the k-th finite principal-unit subgroup.

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem
    standardLubinTateRealUpperRamificationGroup_nat_eq_galoisParameterSubgroup
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n + 1) :
    standardLubinTateRealUpperRamificationGroup hπ n (k : ℝ) =
      standardLubinTateGaloisParameterSubgroup F hπ n k

theorem

standardLubinTateRealUpperRamificationGroup_natCard

L300 ↗

LubinTate.standardLubinTateRealUpperRamificationGroup_natCard

Documentation

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

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateRealUpperRamificationGroup_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
        (standardLubinTateRealUpperRamificationGroup hπ n (k : ℝ)) =
      Nat.card F.residueField ^ (n + 1 - k)

theorem

standardLubinTateRealLowerRamificationGroup_eq_break_of_pow_interval

L314 ↗

LubinTate.standardLubinTateRealLowerRamificationGroup_eq_break_of_pow_interval

Documentation

On a lower-numbering power interval, the 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
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateRealLowerRamificationGroup_eq_break_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)
    (hlow : Nat.card F.residueField ^ (k - 1) ≤ r)
    (hhigh : r < Nat.card F.residueField ^ k) :
    standardLubinTateRealLowerRamificationGroup hπ n (r : ℝ) =
      standardLubinTateRealLowerRamificationGroup hπ n
        ((Nat.card F.residueField ^ k - 1 : ℕ) : ℝ)

theorem

standardLubinTateRealUpperRamificationGroup_eq_natCeil

L331 ↗

LubinTate.standardLubinTateRealUpperRamificationGroup_eq_natCeil

Documentation

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

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateRealUpperRamificationGroup_eq_natCeil
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (t : ℝ)
    (hk : 1 ≤ ⌈t⌉₊) (hkn : ⌈t⌉₊ ≤ n + 1) :
    standardLubinTateRealUpperRamificationGroup hπ n t =
      standardLubinTateRealUpperRamificationGroup
        hπ n (⌈t⌉₊ : ℝ)

theorem

standardLubinTateRealUpperRamificationGroup_eq_galoisParameterSubgroup_of_ceil

L425 ↗

LubinTate.standardLubinTateRealUpperRamificationGroup_eq_galoisParameterSubgroup_of_ceil

Documentation

On the positive visible range, the real upper group is the Galois image at its natural-ceiling principal-unit level.

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem
    standardLubinTateRealUpperRamificationGroup_eq_galoisParameterSubgroup_of_ceil
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (t : ℝ)
    (hk : 1 ≤ ⌈t⌉₊) (hkn : ⌈t⌉₊ ≤ n + 1) :
    standardLubinTateRealUpperRamificationGroup hπ n t =
      standardLubinTateGaloisParameterSubgroup F hπ n ⌈t⌉₊

theorem

standardLubinTateRealUpperRamificationGroup_natCard_of_ceil

L440 ↗

LubinTate.standardLubinTateRealUpperRamificationGroup_natCard_of_ceil

Documentation

On the positive visible range, the real upper group has the order prescribed by its natural-ceiling principal-unit level.

Source context 10 commands

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

noncomputable section
universe u v
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open RamificationTheory.DiscreteValuationField
open RamificationTheory.HilbertRamification.Higher
variable {K : Type u} [Field K]
noncomputable local instance
    standardLubinTateLevelField_finiteDimensional_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    FiniteDimensional K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_finiteDimensional hπ n
noncomputable local instance
    standardLubinTateLevelField_isGalois_forHerbrandFormula
    {F : LocalField.{u, v} K} {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K)) (n : ℕ) :
    IsGalois K (standardLubinTateLevelField hπ n) :=
  standardLubinTateLevelField_isGalois hπ n

Lean source · statement

theorem standardLubinTateRealUpperRamificationGroup_natCard_of_ceil
    (F : LocalField.{u, v} K) {π : F.valuationSubring}
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (n : ℕ) (t : ℝ)
    (hk : 1 ≤ ⌈t⌉₊) (hkn : ⌈t⌉₊ ≤ n + 1) :
    Nat.card (standardLubinTateRealUpperRamificationGroup hπ n t) =
      Nat.card F.residueField ^ (n + 1 - ⌈t⌉₊)

Module documentation

Herbrand formula for finite Lubin--Tate levels

Declarations