Module

MathlibTopologicalGlobalReciprocity.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.MathlibTopologicalGlobalReciprocity

1 declaration indexed from sourceView source ↗

Module documentation

Topological global reciprocity in Mathlib's groups

The existing maximal-abelian Artin isomorphism is transported through the topological comparison of idèle class groups and the canonical comparison of absolute Galois abelianizations. This module proves the small-universe case; universe transport for the public statement is separate.

Imports5

Imported by2

def

mathlibIdeleClassConnectedQuotientEquivAbelianization

L30 ↗

GlobalClassFieldTheory.Reciprocity.mathlibIdeleClassConnectedQuotientEquivAbelianization

Documentation

The maximal-abelian Artin isomorphism, expressed entirely in Mathlib's idèle-class and absolute-Galois groups, for a small number-field carrier.

Source context 3 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory.Reciprocity

Lean source · statement

def mathlibIdeleClassConnectedQuotientEquivAbelianization
    (K : Type) [Field K] [NumberField K] :
    ClassFieldTheory.IdeleClassConnectedQuotient K ≃ₜ*
      Field.absoluteGaloisGroupAbelianization K

Module documentation

Topological global reciprocity in Mathlib's groups

Declarations

mathlibIdeleClassConnectedQuotientEquivAbelianization