Module

Classification.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.Classification

4 declarations indexed from sourceView source ↗

Module documentation

Classification by open finite-index norm subgroups

Combining the mixed- and equal-characteristic existence arguments gives the unconditional order isomorphism between finite abelian subextensions of the fixed separable closure and open finite-index subgroups of the local multiplicative group.

Imports3

Imported by4

theorem

finiteAbelianNormSubgroupMap_surjective

L34 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupMap_surjective

Documentation

Every native open finite-index subgroup of Kˣ is the norm subgroup of a finite abelian subextension of the fixed separable closure.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finiteAbelianNormSubgroupMap_surjective :
    Function.Surjective (finiteAbelianNormSubgroupMap K)

def

finiteAbelianNormSubgroupOrderIso

L48 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupOrderIso

Documentation

Finite local existence theorem. Finite abelian subextensions, ordered by field inclusion, correspond to native open finite-index subgroups of Kˣ with the opposite inclusion order.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · full declaration

def finiteAbelianNormSubgroupOrderIso :
    FiniteAbelianSubextension (intrinsicAbstractBase K) ≃o
      (OpenFiniteIndexSubgroup K)ᵒᵈ where
  toEquiv := Equiv.ofBijective (finiteAbelianNormSubgroupMap K)
    ⟨finiteAbelianNormSubgroupMap_injective K,
      finiteAbelianNormSubgroupMap_surjective K⟩
  map_rel_iff' := by
    intro L₁ L₂
    change finiteAbelianNormSubgroup K L₂ ≤
        finiteAbelianNormSubgroup K L₁ ↔ L₁ ≤ L₂
    exact (finiteAbelianSubextension_le_iff_normSubgroup_le K L₁ L₂).symm

def

finiteAbelianNormSubgroupEquiv

L61 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupEquiv

Documentation

Underlying equivalence of the finite local existence order isomorphism.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

def finiteAbelianNormSubgroupEquiv :
    FiniteAbelianSubextension (intrinsicAbstractBase K) ≃
      OpenFiniteIndexSubgroup K

theorem

finiteAbelianNormSubgroupOrderIso_apply

L68 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupOrderIso_apply

Documentation

States the theorem finiteAbelianNormSubgroupOrderIso_apply.

Source context 5 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]

Lean source · statement

theorem finiteAbelianNormSubgroupOrderIso_apply
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    finiteAbelianNormSubgroupOrderIso K L =
      finiteAbelianNormSubgroupMap K L

Module documentation

Classification by open finite-index norm subgroups

Declarations

finiteAbelianNormSubgroupMap_surjective

finiteAbelianNormSubgroupOrderIso

finiteAbelianNormSubgroupEquiv

finiteAbelianNormSubgroupOrderIso_apply