NYLL
Module

NormIndex.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.LubinTateApplication.NormIndex
2 declarations indexed from sourceView source ↗

Module documentation

Lubin--Tate application: index of the explicit level norm subgroup

The equality between the norm-subgroup index and the extension degree uses finite local reciprocity. It therefore belongs to the concrete local class field theory application layer, not to the reusable Lubin--Tate library.

Imports4
Imported by2

Declarations

theorem

normSubgroup_index_eq_finrank_of_isAbelianGalois

L34 ↗
LubinTate.EqualCharacteristic.normSubgroup_index_eq_finrank_of_isAbelianGalois
Source context 7 commands

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

noncomputable section
open scoped LaurentSeries ValuativeRel
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
variable {K : Type} [Field K]
Lean source · statement
theorem normSubgroup_index_eq_finrank_of_isAbelianGalois
    {B E : Type} [Field B] [Field E] [Algebra B E]
    (hab : IsAbelianGalois B E)
    (hfd : FiniteDimensional B E)
    [ValuativeRel B] [TopologicalSpace B]
    [IsNonarchimedeanLocalField B] :
    (localNormSubgroup B E).index = Module.finrank B E
theorem

equalCharacteristicLubinTateNormSubgroup_index

L48 ↗
LubinTate.EqualCharacteristic.equalCharacteristicLubinTateNormSubgroup_index
Documentation

The norm subgroup of the level-n+1 Lubin--Tate extension has index (q - 1) q^n, its extension degree.

Source context 7 commands

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

noncomputable section
open scoped LaurentSeries ValuativeRel
namespace LubinTate
namespace EqualCharacteristic
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory
variable {K : Type} [Field K]
Lean source · full declaration
theorem equalCharacteristicLubinTateNormSubgroup_index
    (F : LocalField K)
    [CharP K F.residueCharacteristic]
    (n : ℕ) :
    letI : ValuativeRel F.residueField⸨X⸩ :=
      equalCharacteristicLaurentValuativeRel F
    (equalCharacteristicLubinTateNormSubgroup F n).index =
      (Nat.card F.residueField - 1) * Nat.card F.residueField ^ n := by
  let B := F.residueField⸨X⸩
  let E := equalCharacteristicLubinTateLevelField F n
  let : ValuativeRel B := equalCharacteristicLaurentValuativeRel F
  let : IsNonarchimedeanLocalField B :=
    equalCharacteristicLaurentIsNonarchimedeanLocalField F
  let : Algebra B E := equalCharacteristicLubinTateLevelAlgebra F n
  change (localNormSubgroup B E).index = _
  calc
    (localNormSubgroup B E).index = Module.finrank B E :=
      normSubgroup_index_eq_finrank_of_isAbelianGalois
        (equalCharacteristicLubinTateLevelField_isAbelianGalois F n)
        (equalCharacteristicLubinTateLevelField_finiteDimensional F n)
    _ = (Nat.card F.residueField - 1) *
        Nat.card F.residueField ^ n :=
      equalCharacteristicLubinTateLevelField_finrank F n

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