Cyclotomic Galois characters as ray class characters

Let F = K(μ_m) be an m-th cyclotomic extension of a number field K, and let 𝔪 be the modulus of K with finite part (m) and every real place in its infinite part. This file provides the Artin map of the abelian extension F / K as a homomorphism from the ray class group of 𝔪 to Gal(F/K). It sends the ray class of a prime 𝔭 ∤ m to the Frobenius at 𝔭.

Composing with it, every character χ of Gal(F/K) gives a ray class character of 𝔪, and on the integral ideals prime to m the ideal weight galoisCharacterWeight χ of χ agrees with that ray class character.

Main definitions

• NumberField.Chebotarev.cyclotomicModulus: the modulus of K with finite part (m) and every real place in its infinite part.
• NumberField.Chebotarev.cyclotomicArtin: the Artin map RayClassGroup (cyclotomicModulus K m) →* (F ≃ₐ[K] F).

Main results

• NumberField.Chebotarev.cyclotomicArtin_idealClass_of_isArithFrobAt: the Artin map sends the ray class of a prime 𝔭 ∤ m to the Frobenius at 𝔭.
• NumberField.Chebotarev.cyclotomicArtin_comp_classMap_eq: if F is both the m-th and the n-th cyclotomic extension of K, the Artin maps of levels m and n agree on the ray class group of every common multiple of the two cyclotomic moduli.
• MonoidHom.galoisCharacterWeight_eq_onIdeals_cyclotomicArtin: on the integral ideals prime to m, the ideal weight of a character χ of Gal(F/K) is the ray class character χ ∘ cyclotomicArtin.

noncomputable def NumberField.Chebotarev.cyclotomicModulus (K : Type u_1) [Field K] [NumberField K] (m : ℕ) [NeZero m] : TauCeti.GlobalNumberFields.Modulus K

The cyclotomic modulus of level m: finite part the ideal (m) of 𝓞 K, and every real place of K in the infinite part. The Artin map of K(μ_m) / K factors through its ray class group (cyclotomicArtin). The definition does not unfold outside this file; use cyclotomicModulus_finitePart, mem_cyclotomicModulus_infinitePart and mem_cyclotomicModulus_support_iff.

@[simp]

theorem NumberField.Chebotarev.cyclotomicModulus_finitePart (K : Type u_1) [Field K] [NumberField K] (m : ℕ) [NeZero m] : (cyclotomicModulus K m).finitePart = Ideal.span {↑m}

The finite part of the cyclotomic modulus of level m is the principal ideal (m).

@[simp]

theorem NumberField.Chebotarev.mem_cyclotomicModulus_infinitePart (K : Type u_1) [Field K] [NumberField K] (m : ℕ) [NeZero m] (w : { w : InfinitePlace K // w.IsReal }) : w ∈ (cyclotomicModulus K m).infinitePart

Every real place of K lies in the infinite part of the cyclotomic modulus.

theorem NumberField.Chebotarev.mem_cyclotomicModulus_support_iff {K : Type u_1} [Field K] [NumberField K] {m : ℕ} [NeZero m] {v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} : v ∈ (cyclotomicModulus K m).support ↔ ↑m ∈ v.asIdeal

A prime lies in the support of the cyclotomic modulus exactly when it divides m.

theorem NumberField.Chebotarev.cyclotomicModulus_dvd_cyclotomicModulus {K : Type u_1} [Field K] [NumberField K] {m : ℕ} [NeZero m] {n : ℕ} [NeZero n] (h : m ∣ n) : cyclotomicModulus K m ∣ cyclotomicModulus K n

The cyclotomic modulus of level m divides that of every multiple n of m.

theorem NumberField.Chebotarev.asIdeal_mem_integralIdealsPrimeTo_cyclotomicModulus_iff {K : Type u_1} [Field K] [NumberField K] {m : ℕ} [NeZero m] {v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} : v.asIdeal ∈ TauCeti.GlobalNumberFields.integralIdealsPrimeTo (cyclotomicModulus K m) ↔ ↑m ∉ v.asIdeal

A height-one prime is prime to the cyclotomic modulus exactly when it does not divide m.

theorem NumberField.Chebotarev.isUnramifiedAt_of_notMem_cyclotomicModulus_support {K : Type u_1} [Field K] [NumberField K] (F : Type u_2) [Field F] [Algebra K F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K F] {v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} (hv : v ∉ (cyclotomicModulus K m).support) (Q : Ideal (RingOfIntegers F)) [Q.IsPrime] [Q.LiesOver v.asIdeal] : Algebra.IsUnramifiedAt (RingOfIntegers K) Q

For F = K(μ_m), every prime of 𝓞 F above a prime v of 𝓞 K outside the support of cyclotomicModulus K m (that is, with (m : 𝓞 K) ∉ v.asIdeal) is unramified over 𝓞 K.

noncomputable def NumberField.Chebotarev.cyclotomicArtin (K : Type u_1) [Field K] [NumberField K] (F : Type u_2) [Field F] [NumberField F] [Algebra K F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K F] [IsGalois K F] : TauCeti.GlobalNumberFields.RayClassGroup (cyclotomicModulus K m) →* Gal(F/K)

The Artin map of a cyclotomic extension on the ray class group. For F = K(μ_m) the Artin map of the abelian extension F / K on the fractional ideals prime to m is trivial on the ray of cyclotomicModulus K m, and so factors through its ray class group. The definition does not unfold outside this file; it sends the ray class of a prime 𝔭 ∤ m to the Frobenius at 𝔭 (cyclotomicArtin_idealClass_of_isArithFrobAt).

theorem NumberField.Chebotarev.cyclotomicArtin_comp_rayClassMk {K : Type u_1} [Field K] [NumberField K] (F : Type u_2) [Field F] [NumberField F] [Algebra K F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K F] [IsGalois K F] : (cyclotomicArtin K F m).comp (TauCeti.GlobalNumberFields.rayClassMk (cyclotomicModulus K m)) = TauCeti.NumberFieldArithmetic.artinHomAway ⋯ (cyclotomicModulus K m).support ⋯

The cyclotomic Artin map composed with the ray class map is the ideal-theoretic Artin map on fractional ideals prime to the cyclotomic modulus.

theorem NumberField.Chebotarev.cyclotomicArtin_idealClass_of_isArithFrobAt {K : Type u_1} [Field K] [NumberField K] (F : Type u_2) [Field F] [NumberField F] [Algebra K F] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K F] [IsGalois K F] (𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (h𝔭 : 𝔭.asIdeal ∈ TauCeti.GlobalNumberFields.integralIdealsPrimeTo (cyclotomicModulus K m)) (Q : Ideal (RingOfIntegers F)) [Q.LiesOver 𝔭.asIdeal] {σ : Gal(F/K)} (hσ : IsArithFrobAt (RingOfIntegers K) σ Q) : (cyclotomicArtin K F m) ((TauCeti.GlobalNumberFields.idealClass (cyclotomicModulus K m)) ⟨𝔭.asIdeal, h𝔭⟩) = σ

The Artin map sends the ray class of a prime to its Frobenius. At a height-one prime 𝔭 not dividing m, every arithmetic Frobenius at every prime of 𝓞 F above 𝔭 is the image of the ray class of 𝔭.

theorem NumberField.Chebotarev.cyclotomicArtin_comp_classMap_eq {K : Type u_1} [Field K] [NumberField K] {F : Type u_2} [Field F] [NumberField F] [Algebra K F] [IsGalois K F] {m n : ℕ} [NeZero m] [NeZero n] [IsCyclotomicExtension {m} K F] [IsCyclotomicExtension {n} K F] {𝔐 : TauCeti.GlobalNumberFields.Modulus K} (hm : cyclotomicModulus K m ∣ 𝔐) (hn : cyclotomicModulus K n ∣ 𝔐) : (cyclotomicArtin K F m).comp (TauCeti.GlobalNumberFields.classMap hm) = (cyclotomicArtin K F n).comp (TauCeti.GlobalNumberFields.classMap hn)

The Artin maps of two levels agree. If F is both the m-th and the n-th cyclotomic extension of K, the Artin maps of levels m and n agree on the ray class group of every common multiple of the two cyclotomic moduli.

theorem MonoidHom.galoisCharacterWeight_eq_onIdeals_cyclotomicArtin {K : Type u_1} [Field K] [NumberField K] {F : Type u_2} [Field F] [NumberField F] [Algebra K F] {m : ℕ} [NeZero m] [IsCyclotomicExtension {m} K F] [IsGalois K F] (χ : Gal(F/K) →* ℂˣ) (I : ↥(TauCeti.GlobalNumberFields.integralIdealsPrimeTo (NumberField.Chebotarev.cyclotomicModulus K m))) : χ.galoisCharacterWeight ↑I = ↑((TauCeti.GlobalNumberFields.RayClassCharacter.onIdeals (χ.comp (NumberField.Chebotarev.cyclotomicArtin K F m))) I)

The ideal weight of a cyclotomic Galois character is a ray class character. For a character χ of Gal(F/K) with F = K(μ_m), the ideal weight galoisCharacterWeight χ agrees, on the integral ideals prime to m, with the ray class character χ ∘ cyclotomicArtin K F m of cyclotomicModulus K m.