NYLL
Module

StandardSubgroupIndex.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.LubinTateApplication.StandardSubgroupIndex
5 declarations indexed from sourceView source ↗

Module documentation

The canonical standard subgroup index

For the topology-first nonarchimedean local field K, the canonical Lubin--Tate uniformizer and the (n + 1)-st principal units generate a subgroup of Kˣ of index

(Nat.card 𝓀[K] - 1) * Nat.card 𝓀[K] ^ n.

The proof passes from field units to integer units, transports the latter through the canonical packaged local-field equivalence, and then uses the finite standard Lubin--Tate unit-parameter count.

Imports6
Imported by3

Declarations

theorem

standardLubinTateCanonicalBaseUniformizerUnit_eq_integerRingUniformizerFieldUnit

L48 ↗
LubinTate.standardLubinTateCanonicalBaseUniformizerUnit_eq_integerRingUniformizerFieldUnit
Documentation

The canonical packaged Lubin--Tate uniformizer is the topology-first chosen integer-ring uniformizer, viewed as a field unit.

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLubinTateCanonicalBaseUniformizerUnit_eq_integerRingUniformizerFieldUnit :
    standardLubinTateBaseUniformizerUnit
        (standardLocalFieldUniformizer_isUniformizer K) =
      integerRingUniformizerFieldUnit K
theorem

standardLubinTateCanonicalBaseUniformizerUnit_inv_valuationMap

L57 ↗
LubinTate.standardLubinTateCanonicalBaseUniformizerUnit_inv_valuationMap
Documentation

The inverse of the canonical packaged Lubin--Tate uniformizer has positive normalized additive valuation.

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLubinTateCanonicalBaseUniformizerUnit_inv_valuationMap :
    valuationMap K
        (Additive.ofMul
          (standardLubinTateBaseUniformizerUnit
            (standardLocalFieldUniformizer_isUniformizer K))⁻¹) =
      1
def

standardLubinTateUnitParameterEquivIntegerUnitsPrincipalQuotient

L70 ↗
LubinTate.standardLubinTateUnitParameterEquivIntegerUnitsPrincipalQuotient
Documentation

The canonical integer-unit equivalence identifies the standard finite Lubin--Tate unit parameters with the topology-first principal-unit quotient.

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def
    standardLubinTateUnitParameterEquivIntegerUnitsPrincipalQuotient
    (n : ℕ) :
    standardLubinTateUnitParameter (standardLocalField K) n ≃*
      IntegerUnitsPrincipalQuot K (n + 1)
theorem

standardLubinTateCanonicalUniformizerPrincipalSubgroup_index

L82 ↗
LubinTate.standardLubinTateCanonicalUniformizerPrincipalSubgroup_index
Documentation

The subgroup generated by the canonical Lubin--Tate uniformizer and U^(n+1) has the expected standard finite-level index.

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem standardLubinTateCanonicalUniformizerPrincipalSubgroup_index
    (n : ℕ) :
    (LocalFieldTheory.uniformizerPrincipalSubgroup K
        (standardLubinTateBaseUniformizerUnit
          (standardLocalFieldUniformizer_isUniformizer K))
        1 (n + 1)).index =
      (Nat.card 𝓀[K] - 1) * Nat.card 𝓀[K] ^ n
theorem

subgroup_eq_of_le_of_index_eq_of_ne_zero

L124 ↗
LubinTate.subgroup_eq_of_le_of_index_eq_of_ne_zero
Documentation

A finite-index subgroup contained in another subgroup with the same index is already equal to it. The nonzero-index hypothesis excludes the infinite-index convention index = 0.

Source context 9 commands

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

noncomputable section
open scoped ValuativeRel
namespace LubinTate
open LocalFieldTheory
open LocalFieldTheory
open LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem subgroup_eq_of_le_of_index_eq_of_ne_zero
    {G : Type*} [Group G] {H N : Subgroup G}
    (hHN : H ≤ N) (hindex : H.index = N.index)
    (hindex_ne : H.index ≠ 0) :
    H = N

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