Module

FiniteAbelianLocalExistence.lean

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FiniteAbelianLocalExistence

1 declaration indexed from sourceView source ↗

Module documentation

Finite abelian local existence

This module states the existence half of finite abelian local class field theory. Both sides of the correspondence are expressed directly with Mathlib objects: intermediate fields of SeparableClosure K and subgroups of Kˣ. No implementation-specific class-formation object appears in the statement.

Imports3

Imported by1

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.All

theorem

finiteAbelianLocalExistence

L29 ↗

ClassFieldTheory.finiteAbelianLocalExistence

Documentation

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

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem finiteAbelianLocalExistence
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∀ H : OpenFiniteIndexSubgroup K,
      ∃ E : FiniteAbelianLocalExtension K,
        E.normSubgroup = H.1

Module documentation

Finite abelian local existence

Declarations

finiteAbelianLocalExistence