The cyclotomic subfield cut out by a prime-discriminant character group

Let s be a finite family of prime discriminants and N = |∏ P ∈ s, P|. Inside the N-th cyclotomic field K, Mathlib's character correspondence IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar attaches an intermediate field to every subgroup of Dirichlet characters of level N. This file identifies the field attached to the prime-discriminant character group genusCharGroup s hs (the characters of the subsets of s) with the compositum ℚ(√P : P ∈ s).

The square roots are Gauss sums: for P ∈ s, the Gauss sum of the primitive character of P, formed with a primitive |P|-th root of unity in K, squares to P (gaussSumOfPrimitiveRoot_primeDiscriminantChar_sq), and its Galois stabilizer is the kernel of that character lifted to level N. Intersecting these kernels and applying the Galois correspondence gives the compositum.

Together with the conductor criterion Subgroup.characterSubfield_le_iff_dirichletConductor_dvd and the conductor dirichletConductor_genusCharGroup of the character group, this determines exactly which cyclotomic subfields of K contain the compositum: the field ℚ(ζ_m), for m ∣ N, contains it exactly when the least common multiple of the |P| divides m. When s has at most one even member, this least common multiple is N itself.

See K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 6, and D. A. Cox, Primes of the Form x² + ny², §§3.B and 6.A.

Main results

• characterSubfield_genusCharGroup_eq_adjoin_range: the prime-discriminant character group cuts out the compositum of the fields ℚ(√P).
• adjoin_range_le_iff_lcm_dvd: that compositum lies in the m-th cyclotomic subfield exactly when the least common multiple of the |P| divides m.
• adjoin_range_le_iff_eq_natAbs_prod: with at most one even member, |∏ P ∈ s, P| is the only such level dividing |∏ P ∈ s, P|.

theorem TauCeti.Multiquadratic.characterSubfield_genusCharGroup_eq_adjoin_range (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {(∏ P ∈ s, P).natAbs} ℚ K] [NeZero (∏ P ∈ s, P).natAbs] [IsAbelianGalois ℚ K] (R : Type u_2) [CommRing R] [CharZero R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod (∏ P ∈ s, P).natAbs)ˣ)] (r : ↥s → K) (hr : ∀ (P : ↥s), r P ^ 2 = ↑↑P) : (IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar (∏ P ∈ s, P).natAbs K R).symm (Subgroup.map (MulChar.ringHomCompHom (Int.castRingHom R)) (genusCharGroup s hs)) = IntermediateField.adjoin ℚ (Set.range r)

The prime-discriminant character group cuts out the prime-discriminant compositum. Inside the |∏ P ∈ s, P|-th cyclotomic field K, the intermediate field attached to the characters of the subsets of s (with values pushed into any ring R of characteristic zero with enough roots of unity) is generated by square roots of the members of s.

theorem TauCeti.Multiquadratic.adjoin_range_le_iff_lcm_dvd (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {(∏ P ∈ s, P).natAbs} ℚ K] (r : ↥s → K) (hr : ∀ (P : ↥s), r P ^ 2 = ↑↑P) {m : ℕ} (F : IntermediateField ℚ K) [IsCyclotomicExtension {m} ℚ ↥F] (hmN : m ∣ (∏ P ∈ s, P).natAbs) : IntermediateField.adjoin ℚ (Set.range r) ≤ F ↔ s.lcm Int.natAbs ∣ m

The least cyclotomic level of a prime-discriminant compositum. Inside the |∏ P ∈ s, P|-th cyclotomic field, the field generated by square roots of the members of s lies in the cyclotomic subfield of level m exactly when the least common multiple of the |P| divides m.

theorem TauCeti.Multiquadratic.adjoin_range_le_iff_eq_natAbs_prod (s : Finset ℤ) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {(∏ P ∈ s, P).natAbs} ℚ K] (heven : ∀ P ∈ s, ∀ Q ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) (r : ↥s → K) (hr : ∀ (P : ↥s), r P ^ 2 = ↑↑P) {m : ℕ} (F : IntermediateField ℚ K) [IsCyclotomicExtension {m} ℚ ↥F] (hmN : m ∣ (∏ P ∈ s, P).natAbs) : IntermediateField.adjoin ℚ (Set.range r) ≤ F ↔ m = (∏ P ∈ s, P).natAbs

The exact cyclotomic level of a prime-discriminant compositum. If s has at most one even member, then of the cyclotomic subfields ℚ(ζ_m), m ∣ |∏ P ∈ s, P|, of the |∏ P ∈ s, P|-th cyclotomic field, only the whole field contains the square roots of the members of s.