NYLL
Module

TopologicalGlobalReciprocity.lean

Nyll.ClassFieldTheory.Theorems.GlobalClassFieldTheory.TopologicalGlobalReciprocity
1 declaration indexed from sourceView source ↗

Module documentation

Topological global reciprocity

For a number field K, the idèle class group modulo its identity component is topologically isomorphic to the maximal abelian quotient of the absolute Galois group. The statement uses Mathlib's groups on both sides.

Imports8
Imported by2

Declarations

theorem

topologicalGlobalReciprocity

L31 ↗
ClassFieldTheory.topologicalGlobalReciprocity
Documentation

The topological form of global class field theory.

Source context 3 commands

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

open scoped NumberField
namespace ClassFieldTheory
universe u
Lean source · statement
theorem topologicalGlobalReciprocity
    (K : Type u) [Field K] [NumberField K] :
    Nonempty (IdeleClassConnectedQuotient K ≃ₜ*
      Field.absoluteGaloisGroupAbelianization K)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.