Galois group of the candidate genus field

For a squarefree integer d, candidateGenusField hd is generated over ℚ by the chosen square roots of the radicands of the prime discriminants in genusPrimeDiscriminants hd. This file proves that the resulting extension is abelian Galois and identifies its Galois group with

Multiplicative ({P // P ∈ genusPrimeDiscriminants hd} → ZMod 2).

The isomorphism records the sign by which an automorphism acts on each chosen root. The prime-discriminant factorization contains at most one even prime discriminant, so the radicands are square-class independent and all sign patterns occur. In particular, the Galois group has order 2 ^ (genusPrimeDiscriminants hd).card.

This supplies the Galois and abelian parts of the multiquadratic description of the candidate genus field. For negative d, isGenusField_candidateGenusField identifies this candidate with the maximal extension satisfying the genus-field ramification conditions. The real case and the identification of its relative Galois group with Cl/Cl² remain future work.

The prime-discriminant description of the genus field is classical; see D. A. Cox, Primes of the Form x² + ny², and F. Lemmermeyer, Reciprocity Laws.

Main results

• TauCeti.Multiquadratic.isAbelianGalois_candidateGenusField: the candidate genus field is an abelian Galois extension of ℚ.
• TauCeti.Multiquadratic.galoisGroupEquivCandidateGenusField: its Galois group is the group of sign patterns on the chosen prime-discriminant roots.
• TauCeti.Multiquadratic.card_aut_candidateGenusField: the Galois group has order 2 to the number of prime discriminants in the chosen factorization.

noncomputable def TauCeti.Multiquadratic.candidateGenusFieldEquivAdjoin {d : ℤ} (hd : Squarefree d) : ↥(candidateGenusField hd) ≃ₐ[ℚ] ↥(IntermediateField.adjoin ℚ (Set.range (genusFieldRoot hd)))

The candidate genus field identified with its presentation as the field generated by the chosen prime-discriminant roots.

theorem TauCeti.Multiquadratic.genusFieldRoot_sq_algebraMap {d : ℤ} (hd : Squarefree d) (P : ↥(genusPrimeDiscriminants hd)) : genusFieldRoot hd P ^ 2 = (algebraMap ℚ ℂ) ↑(primeDiscriminantRadicand ↑P)

Each chosen complex root squares to the rational radicand of its prime discriminant.

@[simp]

theorem TauCeti.Multiquadratic.candidateGenusFieldEquivAdjoin_apply_gen {d : ℤ} (hd : Squarefree d) (P : ↥(genusPrimeDiscriminants hd)) : (candidateGenusFieldEquivAdjoin hd) (candidateGenusFieldGen hd P) = gen (genusFieldRoot hd) P

The presentation equivalence sends each candidate-genus-field generator to the corresponding generator of the adjoin presentation.

noncomputable def TauCeti.Multiquadratic.candidateGenusFieldSignPattern {d : ℤ} (hd : Squarefree d) (σ : Gal(↥(candidateGenusField hd)/ℚ)) : ↥(genusPrimeDiscriminants hd) → ZMod 2

The sign pattern of an automorphism of the candidate genus field, obtained by transporting the automorphism to the presentation generated by genusFieldRoot and recording its action on each chosen root.

@[simp]

theorem TauCeti.Multiquadratic.candidateGenusFieldSignPattern_apply {d : ℤ} (hd : Squarefree d) (σ : Gal(↥(candidateGenusField hd)/ℚ)) (P : ↥(genusPrimeDiscriminants hd)) : candidateGenusFieldSignPattern hd σ P = if σ (candidateGenusFieldGen hd P) = candidateGenusFieldGen hd P then 0 else 1

The sign recorded at P is zero exactly when the automorphism fixes the corresponding chosen generator.

noncomputable def TauCeti.Multiquadratic.galoisGroupEquivCandidateGenusField {d : ℤ} (hd : Squarefree d) : Gal(↥(candidateGenusField hd)/ℚ) ≃* Multiplicative (↥(genusPrimeDiscriminants hd) → ZMod 2)

The Galois group of the candidate genus field is the group of sign patterns. An automorphism is sent to the function recording whether it fixes or negates each chosen prime-discriminant root. Square-class independence makes this map bijective.

@[simp]

theorem TauCeti.Multiquadratic.galoisGroupEquivCandidateGenusField_apply {d : ℤ} (hd : Squarefree d) (σ : Gal(↥(candidateGenusField hd)/ℚ)) : (galoisGroupEquivCandidateGenusField hd) σ = Multiplicative.ofAdd (candidateGenusFieldSignPattern hd σ)

The candidate-genus-field Galois equivalence sends an automorphism to its sign pattern on the chosen prime-discriminant roots.

@[simp]

theorem TauCeti.Multiquadratic.galoisGroupEquivCandidateGenusField_symm_apply_gen {d : ℤ} (hd : Squarefree d) (ε : ↥(genusPrimeDiscriminants hd) → ZMod 2) (P : ↥(genusPrimeDiscriminants hd)) : ((galoisGroupEquivCandidateGenusField hd).symm (Multiplicative.ofAdd ε)) (candidateGenusFieldGen hd P) = (-1) ^ (ε P).val * candidateGenusFieldGen hd P

The inverse candidate-genus-field Galois equivalence realizes a sign pattern by sending each chosen generator to (-1)^(ε P) times that generator.

instance TauCeti.Multiquadratic.isAbelianGalois_candidateGenusField {d : ℤ} {hd : Squarefree d} : IsAbelianGalois ℚ ↥(candidateGenusField hd)

The candidate genus field is abelian Galois over ℚ. It is generated by square roots of rational elements, so the field-generic multiquadratic abelian-Galois theorem applies.

theorem TauCeti.Multiquadratic.card_aut_candidateGenusField {d : ℤ} (hd : Squarefree d) : Nat.card Gal(↥(candidateGenusField hd)/ℚ) = 2 ^ (genusPrimeDiscriminants hd).card

Cardinality of the candidate-genus-field Galois group. Its order is 2 to the number of prime discriminants in the chosen factorization of fundamentalDiscriminant d.