Module

MaximalAbelianGlobalArtin.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.MaximalAbelianGlobalArtin

4 declarations indexed from sourceView source ↗

Module documentation

Global Artin map for the maximal abelian extension

This module specializes the continuous infinite global Artin map to the maximal abelian subextension of the separable closure. It also exposes the idele-representative evaluation and its finite Galois projections.

Imports3

Imported by5

def

maximalAbelianGlobalArtin

L32 ↗

GlobalClassFieldTheory.Reciprocity.maximalAbelianGlobalArtin

Documentation

The continuous global Artin homomorphism from the idele class group to the Galois group of the maximal abelian extension.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

def maximalAbelianGlobalArtin :
    IdeleClassGroup K →ₜ* Gal(maximalAbelianExtension K / K)

theorem

maximalAbelianGlobalArtin_mk

L40 ↗

GlobalClassFieldTheory.Reciprocity.maximalAbelianGlobalArtin_mk

Documentation

Evaluation of the maximal abelian global Artin map on an idele representative recovers the infinite global Artin map.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem maximalAbelianGlobalArtin_mk (a : IdeleGroup K) :
    maximalAbelianGlobalArtin K
        (QuotientGroup.mk' (IdeleGroup.principalSubgroup K) a) =
      infiniteGlobalArtinMonoidHom K (maximalAbelianExtension K) a

theorem

maximalAbelianGlobalArtin_finiteProjection

L51 ↗

GlobalClassFieldTheory.Reciprocity.maximalAbelianGlobalArtin_finiteProjection

Documentation

Projection of the maximal abelian global Artin map at an idele representative to a finite Galois intermediate field agrees with the finite global Artin map.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable (K : Type) [Field K] [NumberField K]

Lean source · full declaration

theorem maximalAbelianGlobalArtin_finiteProjection
    (a : IdeleGroup K)
    (E : FiniteGaloisIntermediateField K (maximalAbelianExtension K)) :
    letI : NumberField E := NumberField.of_module_finite K E
    AlgEquiv.restrictNormalHom E
        (maximalAbelianGlobalArtin K
          (QuotientGroup.mk' (IdeleGroup.principalSubgroup K) a)) =
      globalArtinMonoidHom (K := K) (L := E) a := by
  let : NumberField E := NumberField.of_module_finite K E
  rw [maximalAbelianGlobalArtin_mk]
  exact
    restrictNormalHom_infiniteGlobalArtinMonoidHom
      K (maximalAbelianExtension K) a E

theorem

maximalAbelianGlobalArtin_surjective

L66 ↗

GlobalClassFieldTheory.Reciprocity.maximalAbelianGlobalArtin_surjective

Documentation

The maximal abelian global Artin homomorphism is surjective.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem maximalAbelianGlobalArtin_surjective :
    Function.Surjective (maximalAbelianGlobalArtin K)

Module documentation

Global Artin map for the maximal abelian extension

Declarations

maximalAbelianGlobalArtin

maximalAbelianGlobalArtin_mk

maximalAbelianGlobalArtin_finiteProjection

maximalAbelianGlobalArtin_surjective