Module

CharacteristicZero.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.CharacteristicZero

4 declarations indexed from sourceView source ↗

Module documentation

Local existence theorem in characteristic zero

Kummer theory supplies a finite Galois norm subgroup inside the power subgroup attached to any finite-index subgroup of Kˣ. Consequently the ordinary norm-subgroup order embedding is surjective, hence an order isomorphism.

Imports3

Imported by2

theorem

finiteAbelianNormSubgroupMap_surjective_of_charZero

L34 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupMap_surjective_of_charZero

Documentation

In characteristic zero, every native open finite-index subgroup of Kˣ is the norm subgroup of a finite abelian extension.

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] [CharZero K]

Lean source · statement

theorem finiteAbelianNormSubgroupMap_surjective_of_charZero :
    Function.Surjective (finiteAbelianNormSubgroupMap K)

def

finiteAbelianNormSubgroupOrderIso_of_charZero

L58 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupOrderIso_of_charZero

Documentation

Characteristic-zero local existence as an order isomorphism: finite abelian subextensions, ordered by 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] [CharZero K]

Lean source · full declaration

def finiteAbelianNormSubgroupOrderIso_of_charZero :
    FiniteAbelianSubextension (intrinsicAbstractBase K) ≃o
      (OpenFiniteIndexSubgroup K)ᵒᵈ where
  toEquiv := Equiv.ofBijective (finiteAbelianNormSubgroupMap K)
    ⟨finiteAbelianNormSubgroupMap_injective K,
      finiteAbelianNormSubgroupMap_surjective_of_charZero 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_of_charZero

L72 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupEquiv_of_charZero

Documentation

Underlying equivalence of the characteristic-zero 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] [CharZero K]

Lean source · statement

def finiteAbelianNormSubgroupEquiv_of_charZero :
    FiniteAbelianSubextension (intrinsicAbstractBase K) ≃
      OpenFiniteIndexSubgroup K

theorem

finiteAbelianNormSubgroupOrderIso_of_charZero_apply

L79 ↗

LocalClassFieldTheory.finiteAbelianNormSubgroupOrderIso_of_charZero_apply

Documentation

States the theorem finiteAbelianNormSubgroupOrderIso_of_charZero_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] [CharZero K]

Lean source · statement

theorem finiteAbelianNormSubgroupOrderIso_of_charZero_apply
    (L : FiniteAbelianSubextension (intrinsicAbstractBase K)) :
    finiteAbelianNormSubgroupOrderIso_of_charZero K L =
      finiteAbelianNormSubgroupMap K L

Module documentation

Local existence theorem in characteristic zero

Declarations

finiteAbelianNormSubgroupMap_surjective_of_charZero

finiteAbelianNormSubgroupOrderIso_of_charZero

finiteAbelianNormSubgroupEquiv_of_charZero

finiteAbelianNormSubgroupOrderIso_of_charZero_apply