Module

Core.lean

Nyll.ClassFieldTheory.KroneckerWeber.Core

1 declaration indexed from sourceView source ↗

Module documentation

Kronecker--Weber

The reader-facing entry point for the local and global Kronecker--Weber theorems. Importing this module exposes both supported endpoints.

The global Kronecker--Weber theorem

Every finite abelian extension of ℚ is contained in a cyclotomic field. The arithmetic construction and global degree estimate are kept in the semantic support modules under KroneckerWeber.Global; this root exposes the canonical theorem statement.

Imports14

Imported by2

theorem

exists_cyclotomicEmbedding

L47 ↗

KroneckerWeber.exists_cyclotomicEmbedding

Documentation

Global Kronecker--Weber.

Every finite abelian extension of ℚ embeds in ℚ(ζₙ) for some positive integer n. Here CyclotomicField n ℚ is the concrete model of ℚ(ζₙ).

Source context 2 commands

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

noncomputable section
namespace KroneckerWeber

Lean source · statement

theorem exists_cyclotomicEmbedding
    (L : Type) [Field L] [NumberField L] [IsAbelianGalois ℚ L] :
    ∃ n : ℕ, 0 < n ∧
      Nonempty (L →ₐ[ℚ] CyclotomicField n ℚ)

Module documentation

Kronecker--Weber

The global Kronecker--Weber theorem

Declarations

exists_cyclotomicEmbedding