NYLL
Module

FiniteAbelianLocalExistenceOrderIso.lean

Nyll.ClassFieldTheory.Theorems.LocalClassFieldTheory.FiniteAbelianLocalExistenceOrderIso
1 declaration indexed from sourceView source ↗

Module documentation

Order classification in finite abelian local existence

This module states the classification form of local existence for a nonarchimedean local field K. Finite abelian intermediate fields of SeparableClosure K are ordered by field inclusion, whereas open finite-index subgroups of Kˣ are ordered contravariantly. The statement also records that the order isomorphism sends each extension to its actual field-norm subgroup.

Imports6
Imported by2

Declarations

theorem

finiteAbelianLocalExistence_orderIso

L33 ↗
ClassFieldTheory.finiteAbelianLocalExistence_orderIso
Documentation

Finite abelian local extensions correspond contravariantly to open finite-index norm subgroups.

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_orderIso
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
  ∃ e : FiniteAbelianLocalExtension K ≃o
        (OpenFiniteIndexSubgroup K)ᵒᵈ,
      ∀ E : FiniteAbelianLocalExtension K,
        (OrderDual.ofDual (e E)).1 = E.normSubgroup

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