Topological global reciprocity

Mathematical statement

Let $K$ be a number field, $\mathbb A_K^\times$ its idèle group, and $C_K=\mathbb A_K^\times/K^\times$ its idèle class group. Write $C_K^0$ for the connected component of the identity. Then

$$C_K/C_K^0\ \simeq_{\mathrm{top}}\ G_K^{\mathrm{ab}}.$$

Here $G_K=\operatorname{Gal}(K^{\mathrm{sep}}/K)$, and $G_K^{\mathrm{ab}}$ denotes its topological abelianization.

Lean code

`ClassFieldTheory.topologicalGlobalReciprocity`

Published library source ↗Same source in NYLL ↗

theorem topologicalGlobalReciprocity
    (K : Type u) [Field K] [NumberField K] :
    Nonempty (IdeleClassConnectedQuotient K ≃ₜ*
      Field.absoluteGaloisGroupAbelianization K)

In-scope Lean context

open scoped NumberField

namespace ClassFieldTheory

universe u

Full declaration and proof

/-- The topological form of global class field theory. -/
theorem topologicalGlobalReciprocity
    (K : Type u) [Field K] [NumberField K] :
    Nonempty (IdeleClassConnectedQuotient K ≃ₜ*
      Field.absoluteGaloisGroupAbelianization K) := by
  let : Small.{0} K := numberField_small K
  let S := Shrink.{0} K
  let : NumberField S := numberField_shrink K
  let e : S ≃ₐ[ℚ] K := (Shrink.ringEquiv K).toRatAlgEquiv
  let cS : IdeleClassGroup S ≃ₜ*
      NumberField.IdeleClassGroup (𝓞 S) S :=
    IdeleGroup.ideleClassGroupContinuousMulEquivMathlib S
  let cK : IdeleClassGroup K ≃ₜ*
      NumberField.IdeleClassGroup (𝓞 K) K :=
    IdeleGroup.ideleClassGroupContinuousMulEquivMathlib K
  let c : NumberField.IdeleClassGroup (𝓞 S) S ≃ₜ*
      NumberField.IdeleClassGroup (𝓞 K) K :=
    cS.symm.trans ((ideleClassCongrContinuousMulEquiv e).trans cK)
  let q : IdeleClassConnectedQuotient S ≃ₜ*
      IdeleClassConnectedQuotient K :=
    connectedComponentQuotientCongr c
  let g : Field.absoluteGaloisGroupAbelianization S ≃ₜ*
      Field.absoluteGaloisGroupAbelianization K :=
    absoluteGaloisGroupAbelianizationEquivOfRingEquiv e.toRingEquiv
  let r : IdeleClassConnectedQuotient S ≃ₜ*
      Field.absoluteGaloisGroupAbelianization S :=
    GlobalClassFieldTheory.Reciprocity.mathlibIdeleClassConnectedQuotientEquivAbelianization S
  exact ⟨q.symm.trans (r.trans g)⟩

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

J. S. Milne. Class Field Theory, version 4.03. 2020. Author's notes, dated 6 August 2020. Chapters I, III, V, VII, and VIII give complementary formulations and historical notes.