The candidate genus field of ℚ(√d)

For a squarefree integer d, the candidate genus field of ℚ(√d) built here is the compositum over ℚ of the quadratic fields ℚ(√(radicand P)) attached to the prime discriminants P dividing the fundamental discriminant fundamentalDiscriminant d. This compositum is unramified at the finite places. For imaginary d, where the narrow and ordinary genus fields coincide, it is the genus field of ℚ(√d). For real d it is only the narrow candidate and may ramify at the infinite places: e.g. d = 3 has disc = 12 = (-4)·(-3), so the compositum is ℚ(i, √3), ramified at the real places over ℚ(√3). The imaginary identification is isGenusField_candidateGenusField; identifying the ordinary genus field for real d, which needs the infinite-place condition, remains future work.

This file gives the object a name. CandidateGenusField.Construction proves the underlying square-class facts for an arbitrary finite set of prime discriminants with chosen roots; here we fix a choice — the factorization finset genusPrimeDiscriminants from Int.IsFundamentalDiscr.exists_finset_primeDiscriminant, and chosen complex roots genusFieldRoot of the radicands (using that ℂ is algebraically closed) — and package the compositum as candidateGenusField. The factorization is uniquely characterized by genusPrimeDiscriminants_eq; only the roots retain a choice. As a first property we record that it contains a square root of d, so it really is a candidate genus field of ℚ(√d).

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

Main definitions

• TauCeti.Multiquadratic.candidateGenusField: the candidate genus field of ℚ(√d), as an intermediate field of ℂ / ℚ.
• TauCeti.Multiquadratic.candidateGenusFieldGen: each chosen root, viewed inside the candidate genus field.

Main results

• TauCeti.Multiquadratic.genusPrimeDiscriminants_eq: the chosen factor finset is equal to every prime-discriminant factorization satisfying the defining conditions.
• TauCeti.Multiquadratic.candidateGenusFieldGen_ne_zero: every chosen generator is nonzero.
• TauCeti.Multiquadratic.candidateGenusField_le_iff: its universal property — it is below an intermediate field iff that field contains every chosen root.
• TauCeti.Multiquadratic.exists_mem_candidateGenusField_sq_eq: it contains an element squaring to d.

noncomputable def TauCeti.Multiquadratic.genusPrimeDiscriminants {d : ℤ} (hd : Squarefree d) : Finset ℤ

The chosen prime-discriminant factorization of fundamentalDiscriminant d: for squarefree d, the finite set of prime discriminants dividing the discriminant of ℚ(√d), from Int.IsFundamentalDiscr.exists_finset_primeDiscriminant.

theorem TauCeti.Multiquadratic.genusPrimeDiscriminants_spec {d : ℤ} (hd : Squarefree d) : (∀ P ∈ genusPrimeDiscriminants hd, IsPrimeDiscriminant P) ∧ (∀ P ∈ genusPrimeDiscriminants hd, ∀ Q ∈ genusPrimeDiscriminants hd, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) ∧ ∏ P ∈ genusPrimeDiscriminants hd, P = fundamentalDiscriminant d

The defining properties of genusPrimeDiscriminants: its members are prime discriminants, at most one of which is even, and their product is fundamentalDiscriminant d.

theorem TauCeti.Multiquadratic.genusPrimeDiscriminants_eq {d : ℤ} (hd : Squarefree d) {s : Finset ℤ} (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) : genusPrimeDiscriminants hd = s

Characterization of the chosen prime-discriminant factorization. Every factorization of fundamentalDiscriminant d into distinct prime discriminants is the finset genusPrimeDiscriminants hd.

noncomputable def TauCeti.Multiquadratic.genusFieldRoot {d : ℤ} (hd : Squarefree d) (P : ↥(genusPrimeDiscriminants hd)) : ℂ

A chosen complex square root of the radicand of each prime discriminant in genusPrimeDiscriminants hd (available since ℂ is algebraically closed).

@[simp]

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

Each genusFieldRoot squares to its radicand (in ℂ-cast normal form).

noncomputable def TauCeti.Multiquadratic.candidateGenusField {d : ℤ} (hd : Squarefree d) : IntermediateField ℚ ℂ

The candidate genus field of ℚ(√d). For squarefree d, the compositum over ℚ of the chosen complex square roots of the radicands of the prime discriminants dividing fundamentalDiscriminant d. Unramified at the finite places, it is the genus field of ℚ(√d) for imaginary d by isGenusField_candidateGenusField and only the narrow candidate for real d; the ordinary real genus field remains future work.

theorem TauCeti.Multiquadratic.candidateGenusField_def {d : ℤ} (hd : Squarefree d) : candidateGenusField hd = IntermediateField.adjoin ℚ (Set.range (genusFieldRoot hd))

candidateGenusField presented as the adjoin of its chosen roots.

@[simp]

theorem TauCeti.Multiquadratic.genusFieldRoot_mem_candidateGenusField {d : ℤ} (hd : Squarefree d) (P : ↥(genusPrimeDiscriminants hd)) : genusFieldRoot hd P ∈ candidateGenusField hd

Each chosen root lies in the candidate genus field.

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

The chosen root indexed by P, regarded as an element of the candidate genus field.

@[simp]

theorem TauCeti.Multiquadratic.candidateGenusFieldGen_val {d : ℤ} (hd : Squarefree d) (P : ↥(genusPrimeDiscriminants hd)) : ↑(candidateGenusFieldGen hd P) = genusFieldRoot hd P

The chosen candidate-genus-field generator has the corresponding chosen complex root as its underlying value.

@[simp]

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

The chosen candidate-genus-field generator squares to its prime-discriminant radicand.

@[simp]

theorem TauCeti.Multiquadratic.candidateGenusFieldGen_ne_zero {d : ℤ} (hd : Squarefree d) (P : ↥(genusPrimeDiscriminants hd)) : candidateGenusFieldGen hd P ≠ 0

Every chosen candidate-genus-field generator is nonzero.

@[simp]

theorem TauCeti.Multiquadratic.candidateGenusField_le_iff {d : ℤ} (hd : Squarefree d) {F : IntermediateField ℚ ℂ} : candidateGenusField hd ≤ F ↔ ∀ (P : ↥(genusPrimeDiscriminants hd)), genusFieldRoot hd P ∈ F

Universal property of the candidate genus field. It is contained in an intermediate field F exactly when F contains every chosen root.

theorem TauCeti.Multiquadratic.exists_mem_candidateGenusField_sq_eq {d : ℤ} (hd : Squarefree d) : ∃ x ∈ candidateGenusField hd, x ^ 2 = (algebraMap ℚ ℂ) ↑d

The candidate genus field of ℚ(√d) contains a square root of d. This is what makes it a candidate genus field of ℚ(√d); it specializes the square-class containment from CandidateGenusField.Construction to the chosen factorization and roots.