Prove2Me

Kronecker--Weber for abelian fields of degree at least 33

Open
Leopoldt.exists_algHom_cyclotomicField_of_three_le_finrank

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

class-field-theorycyclotomic-fieldsnumber-theory

Kronecker–Weber theorem, degree ≥3\ge 3. Let K\mathbb{K} be a number field which is a Galois extension of Q\mathbb{Q} with abelian Galois group Gal(K/Q)\mathrm{Gal}(\mathbb{K}/\mathbb{Q}), and assume [K:Q]≥3[\mathbb{K}:\mathbb{Q}] \ge 3. Then there is an integer n≥1n \ge 1 and an embedding of Q\mathbb{Q}-algebras

K↪Q(ζn).\mathbb{K} \hookrightarrow \mathbb{Q}(\zeta_n).

This is the Kronecker–Weber theorem restricted to fields of degree at least 33. Fields of degree ≤2\le 2 (the field Q\mathbb{Q} and the quadratic fields) are handled separately by the elementary Gauss-sum argument, NumberField.exists_algHom_cyclotomicField_of_finrank_le_two; the present statement is the part that requires the genuine proof of the theorem (e.g. via ramification groups and reduction to cyclic extensions of prime-power degree, as in Washington's Chapter 14, or via Artin reciprocity).

Formalization note. As in Leopoldt.exists_algHom_cyclotomicField, "abelian Galois" is IsGalois ℚ K together with IsMulCommutative (K ≃ₐ[ℚ] K), Q(ζn)\mathbb{Q}(\zeta_n) is CyclotomicField n ℚ, and the embedding is an unspecified K →ₐ[ℚ] CyclotomicField n ℚ. The degree hypothesis is 3 ≤ Module.finrank ℚ K.

Preamble
import Definitions.Def_LeopoldtDefect

open NumberField
Formal statement
namespace Leopoldt
theorem exists_algHom_cyclotomicField_of_three_le_finrank (K : Type*) [Field K] [NumberField K]
    [IsGalois ℚ K] [IsMulCommutative (K ≃ₐ[ℚ] K)] (hK : 3 ≤ Module.finrank ℚ K) :
    ∃ n : ℕ, 0 < n ∧ Nonempty (K →ₐ[ℚ] CyclotomicField n ℚ) := by sorry
end Leopoldt
Source
Kronecker-Weber theorem: L. C. Washington, Introduction to Cyclotomic Fields, 2nd ed., GTM 83, Chapter 14, Theorem 14.1 (every finite abelian extension of Q is contained in a cyclotomic field); first complete proof D. Hilbert, 'Ein neuer Beweis des Kronecker'schen Fundamentalsatzes ueber Abel'sche Zahlkoerper', Nachr. Ges. Wiss. Goettingen (1896), 29-39. Here restricted to degree >= 3, the degree <= 2 case being NumberField.exists_algHom_cyclotomicField_of_finrank_le_two.

View graph