The norm group of ℚ(ζ_n)/ℚ and the Kronecker–Weber theorem

Let F = ℚ(ζ_n) be the n-th cyclotomic field. Its global Artin map is explicit: it is the ray class map C_ℚ → Cl_{(n)·∞} followed by the identification GlobalNumberFields.ratModulusEquivGal n F : Cl_{(n)·∞} ≃* Gal(F/ℚ) (ideleClassArtinMap_eq_ratModulusEquivGal_rayClassQuotient), which sends the ray class of a prime p ∤ n to the automorphism ζ_n ↦ ζ_n ^ p. Consequently the idele-class norm group N_{F/ℚ}(C_F) is the ray subgroup of (n)·∞ (range_ideleClassNormMap_eq_raySubgroup_ratModulus), the modulus (n)·∞ is admissible for F/ℚ (isAdmissibleModulus_ratModulus), and the ray-class Artin map of F/ℚ at (n)·∞ is ratModulusEquivGal n F (rayClassArtinMap_ratModulus).

The comparison is made through the conductor: the global Artin map of F/ℚ factors through the ray class group of some admissible modulus (N)·∞ with n ∣ N, and on the ray classes of primes p ∤ N both maps are arithmetic Frobenius at p, so they agree, because the ideal-theoretic Artin map is determined by its values on primes.

The Kronecker–Weber theorem (kroneckerWeber) follows from the uniqueness half of the global class-field correspondence. Norm groups detect embeddings of abelian extensions (range_ideleClassNormMap_le_iff_nonempty_algHom), so a finite abelian extension E/ℚ embeds in ℚ(ζ_n) exactly when the ray subgroup of (n)·∞ lies in the norm group of E, that is, when the conductor of E/ℚ divides (n)·∞ (nonempty_algHom_iff_abelianConductor_dvd_ratModulus). The real place imposes no condition, so this happens exactly when the absolute norm of the finite part of the conductor divides n (nonempty_algHom_iff_absNorm_abelianConductor_finitePart_dvd), and in particular E embeds in the cyclotomic field of that level.

Main results

• TauCeti.ClassFieldTheory.ideleClassArtinMap_eq_ratModulusEquivGal_rayClassQuotient: the global Artin map of ℚ(ζ_n)/ℚ is the ray class map modulo (n)·∞ followed by ratModulusEquivGal.
• TauCeti.ClassFieldTheory.range_ideleClassNormMap_eq_raySubgroup_ratModulus: the idele-class norm group of ℚ(ζ_n)/ℚ is the ray subgroup of (n)·∞.
• TauCeti.ClassFieldTheory.isAdmissibleModulus_ratModulus: (n)·∞ is admissible for ℚ(ζ_n)/ℚ.
• TauCeti.ClassFieldTheory.rayClassArtinMap_ratModulus: the ray-class Artin map of ℚ(ζ_n)/ℚ at (n)·∞ is ratModulusEquivGal.
• TauCeti.ClassFieldTheory.nonempty_algHom_iff_abelianConductor_dvd_ratModulus: a finite abelian extension E/ℚ embeds in ℚ(ζ_n) exactly when its conductor divides (n)·∞.
• TauCeti.ClassFieldTheory.nonempty_algHom_iff_absNorm_abelianConductor_finitePart_dvd and TauCeti.ClassFieldTheory.nonempty_algHom_cyclotomicField_iff: it embeds in ℚ(ζ_n) exactly when the absolute norm of the finite part of its conductor divides n.
• TauCeti.ClassFieldTheory.kroneckerWeber: every finite abelian extension of ℚ embeds in a cyclotomic field.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter V, Example 3.11, and Chapter VIII, Theorem 3.4.
• J. Neukirch, Algebraic Number Theory, Chapter VI, Theorem 7.7 and Corollary 7.8.

The global Artin map of ℚ(ζ_n)/ℚ

theorem TauCeti.ClassFieldTheory.ideleClassArtinMap_eq_ratModulusEquivGal_rayClassQuotient (n : ℕ) [NeZero n] (F : Type) [Field F] [NumberField F] [IsCyclotomicExtension {n} ℚ F] [IsAbelianGalois ℚ F] (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers ℚ) ℚ) : (ideleClassArtinMap ℚ F) c = (GlobalNumberFields.ratModulusEquivGal n F) ((GlobalNumberFields.rayClassQuotient (GlobalNumberFields.ratModulus n ⋯)) c)

The global Artin map of ℚ(ζ_n)/ℚ is explicit: the Artin symbol of an idele class is the image under ratModulusEquivGal of its ray class modulo (n)·∞.

theorem TauCeti.ClassFieldTheory.range_ideleClassNormMap_eq_raySubgroup_ratModulus (n : ℕ) [NeZero n] (F : Type) [Field F] [NumberField F] [IsCyclotomicExtension {n} ℚ F] : (↑(GlobalNumberFields.ideleClassNormMap ℚ F)).range = GlobalNumberFields.raySubgroup (GlobalNumberFields.ratModulus n ⋯)

The norm group of ℚ(ζ_n)/ℚ is the ray subgroup of (n)·∞: an idele class of ℚ is a norm from ℚ(ζ_n) exactly when it satisfies the congruence and sign conditions of (n)·∞.

theorem TauCeti.ClassFieldTheory.isAdmissibleModulus_ratModulus (n : ℕ) [NeZero n] (F : Type) [Field F] [NumberField F] [IsCyclotomicExtension {n} ℚ F] : IsAdmissibleModulus ℚ F (GlobalNumberFields.ratModulus n ⋯)

The modulus (n)·∞ is admissible for ℚ(ζ_n)/ℚ: the conductor of ℚ(ζ_n)/ℚ divides (n)·∞.

@[simp]

theorem TauCeti.ClassFieldTheory.rayClassArtinMap_ratModulus (n : ℕ) [NeZero n] (F : Type) [Field F] [NumberField F] [IsCyclotomicExtension {n} ℚ F] [IsAbelianGalois ℚ F] (c : GlobalNumberFields.RayClassGroup (GlobalNumberFields.ratModulus n ⋯)) : (rayClassArtinMap (GlobalNumberFields.ratModulus n ⋯) ⋯) c = (GlobalNumberFields.ratModulusEquivGal n F) c

Ray-class reciprocity for ℚ(ζ_n)/ℚ: the ray-class Artin map at (n)·∞ is the identification ratModulusEquivGal of the ray class group with Gal(ℚ(ζ_n)/ℚ).

The cyclotomic fields containing an abelian extension

theorem TauCeti.ClassFieldTheory.nonempty_algHom_iff_abelianConductor_dvd_ratModulus (E : Type) [Field E] [NumberField E] [IsAbelianGalois ℚ E] (n : ℕ) [NeZero n] (F : Type) [Field F] [NumberField F] [IsCyclotomicExtension {n} ℚ F] : Nonempty (E →ₐ[ℚ] F) ↔ abelianConductor ℚ E ∣ GlobalNumberFields.ratModulus n ⋯

A finite abelian extension E/ℚ embeds in ℚ(ζ_n) exactly when its conductor divides (n)·∞: the norm group of ℚ(ζ_n) is the ray subgroup of (n)·∞, and norm groups detect embeddings of abelian extensions.

theorem TauCeti.ClassFieldTheory.nonempty_algHom_iff_absNorm_abelianConductor_finitePart_dvd (E : Type) [Field E] [NumberField E] [IsAbelianGalois ℚ E] (n : ℕ) [NeZero n] (F : Type) [Field F] [NumberField F] [IsCyclotomicExtension {n} ℚ F] : Nonempty (E →ₐ[ℚ] F) ↔ Ideal.absNorm (abelianConductor ℚ E).finitePart ∣ n

A finite abelian extension E/ℚ embeds in ℚ(ζ_n) exactly when the absolute norm of the finite part of its conductor divides n.

theorem TauCeti.ClassFieldTheory.nonempty_algHom_cyclotomicField_iff (E : Type) [Field E] [NumberField E] [IsAbelianGalois ℚ E] (n : ℕ) [NeZero n] : Nonempty (E →ₐ[ℚ] CyclotomicField n ℚ) ↔ Ideal.absNorm (abelianConductor ℚ E).finitePart ∣ n

A finite abelian extension E/ℚ embeds in CyclotomicField n ℚ exactly when the absolute norm of the finite part of its conductor divides n.

The Kronecker–Weber theorem

theorem TauCeti.ClassFieldTheory.kroneckerWeber (E : Type) [Field E] [NumberField E] [IsAbelianGalois ℚ E] : ∃ (n : ℕ), n ≠ 0 ∧ Nonempty (E →ₐ[ℚ] CyclotomicField n ℚ)

The Kronecker–Weber theorem: every finite abelian extension of ℚ embeds in a cyclotomic field ℚ(ζ_n).