NYLL

theorem · Class Field Theory

The conductor of an abelian extension

A unique least modulus measures which ray class fields contain the extension.

The conductor packages the congruence conditions needed to realize an extension as a class field. Its finite exponents measure ramification depth, while its infinite part records real places that become complex; comparison with this one modulus decides which ray class fields contain the extension. Ray class groups are the classical means of allowing ramification, developed with conductors in Milne's ideal-theoretic presentation.

ClassFieldTheory on GitHub ↗

Mathematical statement

For a finite abelian extension $L/K$ of number fields, there is a unique ray class modulus $\mathfrak f$ such that, for every modulus $\mathfrak m$,

$$L\text{ embeds over }K\text{ in a ray class field for }\mathfrak m\quad\Longleftrightarrow\quad\mathfrak f\leq\mathfrak m.$$

The order compares the finite exponents and the allowed infinite part. Thus the conclusion specifies the whole upward-closed set of admissible moduli.

Lean code

ClassFieldTheory.existsUnique_abelianConductor

Published library source ↗Same source in NYLL ↗

theorem existsUnique_abelianConductor
    (K : Type) [Field K] [NumberField K]
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [IsAbelianGalois K L] :
    ∃! c : RayClassModulus K, IsAbelianConductor K L c
In-scope Lean context
namespace ClassFieldTheory
Full declaration and proof
/-- The conductor of a finite abelian extension of number fields exists
uniquely. -/
theorem existsUnique_abelianConductor
    (K : Type) [Field K] [NumberField K]
    (L : Type) [Field L] [NumberField L]
    [Algebra K L] [IsAbelianGalois K L] :
    ∃! c : RayClassModulus K, IsAbelianConductor K L c := by
  obtain ⟨c, hc⟩ := exists_abelianConductor K L
  exact ⟨c, hc, fun d hd => hd.unique hc⟩
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)
Related Lean sources

References

  1. 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.

Published source: 26f52ca8.

← All selected results in Class Field Theory