The candidate genus field as a cyclotomic character subfield

For squarefree d with fundamental discriminant D, the candidate genus field of ℚ(√d) is the compositum of the quadratic fields ℚ(√P) over the prime discriminants P dividing D. It lies in every cyclotomic subfield K ⊆ ℂ of level |D|, and inside K the Galois correspondence identifies it with the intermediate field attached to the genus characters, the Dirichlet characters of level |D| that are products of the quadratic characters of the prime discriminants dividing D. This is the explicit Kronecker–Weber description of the candidate genus field: it is cut out of ℚ(ζ_|D|) by the genus character group. For imaginary d the candidate genus field is the genus field of ℚ(√d) (isGenusField_candidateGenusField); for real d it is the narrow genus field.

For real d the genus field of ℚ(√d) is instead the maximal real subfield candidateGenusFieldReal hd of the candidate (isGenusField_candidateGenusFieldReal). Since the maximal real subfield of ℚ(ζ_|D|) is cut out by the even characters, this real subfield is cut out by the even genus characters, those with χ (-1) = 1.

Main results

• TauCeti.Multiquadratic.candidateGenusField_eq_map_characterSubfield_genusCharGroup: the candidate genus field is the image in ℂ of the character subfield of the genus character group. The generators are the rescaled roots of TauCeti.NumberTheory.Multiquadratic.Cyclotomic.FundamentalDiscriminant.
• TauCeti.Multiquadratic.map_candidateGenusFieldReal_eq_map_characterSubfield_inf_evenSubgroup: the maximal real subfield of the candidate genus field is the image in ℂ of the character subfield of the even genus characters.

References

• D. A. Cox, Primes of the Form x² + ny², §6.A.

theorem TauCeti.Multiquadratic.candidateGenusField_eq_map_characterSubfield_genusCharGroup {d : ℤ} (hd : Squarefree d) (K : IntermediateField ℚ ℂ) [NumberField ↥K] [IsCyclotomicExtension {(∏ P ∈ genusPrimeDiscriminants hd, P).natAbs} ℚ ↥K] (R : Type u_1) [CommRing R] [CharZero R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod (∏ P ∈ genusPrimeDiscriminants hd, P).natAbs)ˣ)] : candidateGenusField hd = IntermediateField.map K.val ((IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar (∏ P ∈ genusPrimeDiscriminants hd, P).natAbs (↥K) R).symm (Subgroup.map (MulChar.ringHomCompHom (Int.castRingHom R)) (genusCharGroup (genusPrimeDiscriminants hd) ⋯)))

The candidate genus field is cut out of the cyclotomic field by the genus characters. For squarefree d with fundamental discriminant D and a cyclotomic subfield K ⊆ ℂ of level |D|, the candidate genus field of ℚ(√d) is the image in ℂ of the intermediate field of K that the character correspondence attaches to the genus character group of D. The correspondence is taken for the abelian Galois structure of the cyclotomic extension.

theorem TauCeti.Multiquadratic.map_candidateGenusFieldReal_eq_map_characterSubfield_inf_evenSubgroup {d : ℤ} (hd : Squarefree d) (K : IntermediateField ℚ ℂ) [NumberField ↥K] [IsCyclotomicExtension {(∏ P ∈ genusPrimeDiscriminants hd, P).natAbs} ℚ ↥K] (R : Type u_1) [CommRing R] [CharZero R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod (∏ P ∈ genusPrimeDiscriminants hd, P).natAbs)ˣ)] : IntermediateField.map (candidateGenusField hd).val (candidateGenusFieldReal hd) = IntermediateField.map K.val ((IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar (∏ P ∈ genusPrimeDiscriminants hd, P).natAbs (↥K) R).symm (Subgroup.map (MulChar.ringHomCompHom (Int.castRingHom R)) (genusCharGroup (genusPrimeDiscriminants hd) ⋯) ⊓ DirichletCharacter.evenSubgroup R (∏ P ∈ genusPrimeDiscriminants hd, P).natAbs))

The real genus field is cut out of the cyclotomic field by the even genus characters. For squarefree d with fundamental discriminant D and a cyclotomic subfield K ⊆ ℂ of level |D|, the maximal real subfield of the candidate genus field of ℚ(√d) is the image in ℂ of the intermediate field of K that the character correspondence attaches to the even genus characters of D. For positive nonsquare d this real subfield is the genus field of ℚ(√d) (isGenusField_candidateGenusFieldReal).