The relative Galois group of the candidate genus field

For a squarefree integer d, the candidate genus field is abelian Galois over ℚ, with absolute Galois group the sign vectors on the chosen prime-discriminant roots. It contains the embedded base candidateGenusFieldBase hd, generated by a chosen square root of d. This file identifies the relative Galois group over that base with the subspace of sign vectors whose automorphisms fix the base.

More precisely, candidateGenusFieldRelativeSignSubmodule hd is the parity-zero subspace of sign vectors. The product of all the prime-discriminant generators is a nonzero rational multiple of candidateGenusFieldBaseRoot hd, so an automorphism fixes the embedded base exactly when its sign vector has even parity. Restriction of scalars then gives

Gal(candidateGenusField hd / candidateGenusFieldBase hd) ≃* Multiplicative U.

This is the relative Galois-group side of the genus-field construction; the sign subspace found here is matched with the genus characters of ℚ(√d), hence with the maximal elementary-2 quotient Cl⁺(ℚ(√d)) / Cl⁺(ℚ(√d))², in TauCeti.NumberTheory.Multiquadratic.CandidateGenusField.Relative.GenusCharacter. When d is nonsquare, its order is the predicted 2 ^ (t - 1), where t is the number of chosen prime discriminants.

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.

Provenance

The relative Galois equivalence and its action on generators specialize TauCeti.NumberTheory.Multiquadratic.Galois.Relative, whose Layer-0 multiquadratic machinery is migrated from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture.

Main definitions

• TauCeti.Multiquadratic.candidateGenusFieldRelativeSignSubmodule: the sign vectors fixing the embedded base.
• TauCeti.Multiquadratic.galoisGroupEquivCandidateGenusFieldRelative: the relative Galois group as that sign subspace.

Main results

• TauCeti.Multiquadratic.galoisGroupEquivCandidateGenusFieldRelative_apply: the equivalence is given by the sign pattern of the restricted automorphism.
• TauCeti.Multiquadratic.card_aut_candidateGenusField_over_base: the relative Galois group has order 2 ^ (t - 1) when d is nonsquare.

noncomputable def TauCeti.Multiquadratic.candidateGenusFieldProdRoot {d : ℤ} (hd : Squarefree d) : ↥(candidateGenusField hd)

The product of the chosen prime-discriminant generators of the candidate genus field.

@[simp]

theorem TauCeti.Multiquadratic.candidateGenusFieldProdRoot_sq {d : ℤ} (hd : Squarefree d) : candidateGenusFieldProdRoot hd ^ 2 = (algebraMap ℚ ↥(candidateGenusField hd)) (∏ P : ↥(genusPrimeDiscriminants hd), ↑(primeDiscriminantRadicand ↑P))

The square of the product root is the product of the prime-discriminant radicands.

theorem TauCeti.Multiquadratic.exists_candidateGenusFieldProdRoot_eq_mul_baseRoot {d : ℤ} (hd : Squarefree d) : ∃ (a : ℚ), a ≠ 0 ∧ candidateGenusFieldProdRoot hd = (algebraMap ℚ ↥(candidateGenusField hd)) a * candidateGenusFieldBaseRoot hd

The product of all prime-discriminant generators is a nonzero rational multiple of the chosen base root. Thus the embedded base candidateGenusFieldBase is the subfield generated by this concrete product root.

noncomputable def TauCeti.Multiquadratic.candidateGenusFieldRelativeSignSubmodule {d : ℤ} (hd : Squarefree d) : Submodule (ZMod 2) (↥(genusPrimeDiscriminants hd) → ZMod 2)

The 𝔽₂-subspace of even-parity sign patterns. These, independently of the Galois action, are the functions whose coordinate sum is zero.

@[simp]

theorem TauCeti.Multiquadratic.mem_candidateGenusFieldRelativeSignSubmodule_iff {d : ℤ} (hd : Squarefree d) (v : ↥(genusPrimeDiscriminants hd) → ZMod 2) : v ∈ candidateGenusFieldRelativeSignSubmodule hd ↔ ∑ P : ↥(genusPrimeDiscriminants hd), v P = 0

A sign vector belongs to the relative sign subspace exactly when its coordinate sum vanishes.

@[instance_reducible]

noncomputable def TauCeti.Multiquadratic.candidateGenusFieldAdjoinAlgebra {d : ℤ} (hd : Squarefree d) : Algebra ℚ ↥(IntermediateField.adjoin ℚ (Set.range (genusFieldRoot hd)))

The rational algebra structure inherited by the adjoin presentation of the candidate genus field.

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

The sign pattern of a relative automorphism, obtained by restricting it to an absolute ℚ-automorphism of the candidate genus field.

@[simp]

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

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

theorem TauCeti.Multiquadratic.candidateGenusFieldRelativeSignPattern_mem {d : ℤ} (hd : Squarefree d) (σ : Gal(↥(candidateGenusField hd)/↥(candidateGenusFieldBase hd))) : candidateGenusFieldRelativeSignPattern hd σ ∈ candidateGenusFieldRelativeSignSubmodule hd

The sign pattern of a relative automorphism lies in the relative sign subspace.

noncomputable def TauCeti.Multiquadratic.galoisGroupEquivCandidateGenusFieldRelative {d : ℤ} (hd : Squarefree d) : Gal(↥(candidateGenusField hd)/↥(candidateGenusFieldBase hd)) ≃* Multiplicative ↥(candidateGenusFieldRelativeSignSubmodule hd)

The relative Galois group of the candidate genus field is its base-fixing sign subspace. Restriction of a relative automorphism to ℚ, followed by the absolute sign-pattern equivalence, identifies Gal(candidateGenusField hd / candidateGenusFieldBase hd) with the multiplicative form of candidateGenusFieldRelativeSignSubmodule hd.

@[simp]

theorem TauCeti.Multiquadratic.galoisGroupEquivCandidateGenusFieldRelative_apply {d : ℤ} (hd : Squarefree d) (σ : Gal(↥(candidateGenusField hd)/↥(candidateGenusFieldBase hd))) : (galoisGroupEquivCandidateGenusFieldRelative hd) σ = Multiplicative.ofAdd ⟨candidateGenusFieldRelativeSignPattern hd σ, ⋯⟩

The relative Galois equivalence sends an automorphism to the sign pattern of its restriction to an absolute ℚ-automorphism.

@[simp]

theorem TauCeti.Multiquadratic.galoisGroupEquivCandidateGenusFieldRelative_symm_apply_gen {d : ℤ} (hd : Squarefree d) (v : ↥(candidateGenusFieldRelativeSignSubmodule hd)) (P : ↥(genusPrimeDiscriminants hd)) : ((galoisGroupEquivCandidateGenusFieldRelative hd).symm (Multiplicative.ofAdd v)) (candidateGenusFieldGen hd P) = (-1) ^ (↑v P).val * candidateGenusFieldGen hd P

The inverse relative Galois equivalence realizes a base-fixing sign vector by its prescribed sign changes on the chosen prime-discriminant generators.

theorem TauCeti.Multiquadratic.card_aut_candidateGenusField_over_base {d : ℤ} (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) : Nat.card Gal(↥(candidateGenusField hd)/↥(candidateGenusFieldBase hd)) = 2 ^ ((genusPrimeDiscriminants hd).card - 1)

Order of the relative candidate-genus-field Galois group. If the squarefree integer d is not a rational square, the relative group over its embedded quadratic base has order 2 ^ (t - 1), where t = (genusPrimeDiscriminants hd).card.