Module

IsMaximalAbelianGlobalArtin.lean

Nyll.ClassFieldTheory.Definitions.GlobalClassFieldTheory.IsMaximalAbelianGlobalArtin

1 declaration indexed from sourceView source ↗

Module documentation

A maximal-abelian reciprocity-map property

This predicate records surjectivity and kernel equal to the identity component of the idèle class group. These properties alone do not determine the normalized Artin map: finite-level Frobenius compatibility is a separate assertion. Existence is asserted in Theorems.

Imports2

Nyll.ClassFieldTheory.Definitions.GlobalClassFieldTheory.IdeleClassConnectedQuotient
Mathlib.FieldTheory.AbsoluteGaloisGroup

Imported by2

def

IsMaximalAbelianGlobalArtin

L27 ↗

ClassFieldTheory.IsMaximalAbelianGlobalArtin

Documentation

A continuous map to the abelianized Galois group with the expected image and kernel; normalization is not part of this predicate.

Source context 3 commands

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

open scoped NumberField
namespace ClassFieldTheory
universe u

Lean source · statement

def IsMaximalAbelianGlobalArtin
    (K : Type u) [Field K] [NumberField K]
    (artin : NumberField.IdeleClassGroup (𝓞 K) K →ₜ*
      Field.absoluteGaloisGroupAbelianization K) : Prop

Module documentation

A maximal-abelian reciprocity-map property

Declarations

IsMaximalAbelianGlobalArtin