Module

MaximalAbelianGlobalArtin.lean

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.MaximalAbelianGlobalArtin

1 declaration indexed from sourceView source ↗

Module documentation

The maximal abelian global Artin map

This map from Mathlib's idèle class group to Mathlib's abelianized absolute Galois group is continuous, surjective, and has the identity component as its kernel. It is induced by a topological reciprocity isomorphism. The statement does not yet fix Frobenius normalization at finite levels, so it does not assert uniqueness of the map.

Imports2

Imported by1

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.All

theorem

maximalAbelianGlobalArtin

L29 ↗

ClassFieldTheory.maximalAbelianGlobalArtin

Documentation

A continuous surjective global Artin map with the expected kernel exists.

Source context 4 commands

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

open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

theorem maximalAbelianGlobalArtin
    (K : Type u) [Field K] [NumberField K] :
    ∃ artin : NumberField.IdeleClassGroup (𝓞 K) K →ₜ*
        Field.absoluteGaloisGroupAbelianization K,
      IsMaximalAbelianGlobalArtin K artin

Module documentation

The maximal abelian global Artin map

Declarations

maximalAbelianGlobalArtin