The genus-field candidate of a real quadratic field

For positive squarefree nonsquare d, the prime-discriminant compositum candidateGenusField hd is the narrow genus field of ℚ(√d), but it can ramify at the real places. Its maximal totally real subfield is the candidate for the ordinary genus field. This file defines that field and relates it to the embedded quadratic base. Since the full compositum is unramified over the base at every finite prime, its real subfield is too.

The key archimedean fact is intrinsic: an extension of a totally real field is unramified at all infinite places exactly when it is totally real. Consequently every abelian Galois extension of ℚ containing the chosen square root and unramified everywhere over the quadratic base maps into this maximal real subfield.

The construction is classical; see F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, Section 2.2, and D. A. Cox, Primes of the Form x² + ny², Section 6.A.

Main definitions

• TauCeti.Multiquadratic.candidateGenusFieldReal: the maximal totally real subfield of the prime-discriminant compositum.
• TauCeti.Multiquadratic.candidateGenusFieldRealBaseRoot: its chosen square root of d.

Main results

• TauCeti.Multiquadratic.candidateGenusFieldBase_le_candidateGenusFieldReal: the real quadratic base lies in the real candidate.
• TauCeti.Multiquadratic.isAbelianGalois_candidateGenusFieldReal: the real candidate is abelian and Galois over ℚ.
• TauCeti.Multiquadratic.isUnramifiedIn_candidateGenusFieldReal: the real candidate is unramified over its quadratic base at every finite prime.
• TauCeti.Multiquadratic.exists_algHom_candidateGenusFieldReal: every abelian Galois extension of ℚ containing the chosen square root and unramified over the quadratic base at all places embeds into the real candidate.

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

The ordinary genus-field candidate of a real quadratic field. This is the maximal totally real subfield of the prime-discriminant compositum. It is viewed as an intermediate field over ℚ; rational elements belong because every embedding into ℂ fixes them and hence has real image.

@[simp]

theorem TauCeti.Multiquadratic.mem_candidateGenusFieldReal_iff {d : ℤ} (hd : Squarefree d) (x : ↥(candidateGenusField hd)) : x ∈ candidateGenusFieldReal hd ↔ ∀ (φ : ↥(candidateGenusField hd) →+* ℂ), star (φ x) = φ x

Membership in the real candidate means that every complex embedding has real value.

theorem TauCeti.Multiquadratic.isTotallyReal_candidateGenusFieldBase {d : ℤ} (hd : Squarefree d) (hpos : 0 < d) : NumberField.IsTotallyReal ↥(candidateGenusFieldBase hd)

For positive d, the subfield generated by the chosen square root of d is totally real.

theorem TauCeti.Multiquadratic.candidateGenusFieldBase_le_candidateGenusFieldReal {d : ℤ} (hd : Squarefree d) (hpos : 0 < d) : candidateGenusFieldBase hd ≤ candidateGenusFieldReal hd

The embedded base generated by the chosen root lies in the real genus-field candidate.

noncomputable def TauCeti.Multiquadratic.candidateGenusFieldRealBaseRoot {d : ℤ} (hd : Squarefree d) (hpos : 0 < d) : ↥(candidateGenusFieldReal hd)

The chosen square root of d, regarded as an element of the real genus-field candidate.

@[simp]

theorem TauCeti.Multiquadratic.coe_candidateGenusFieldRealBaseRoot {d : ℤ} (hd : Squarefree d) (hpos : 0 < d) : ↑(candidateGenusFieldRealBaseRoot hd hpos) = candidateGenusFieldBaseRoot hd

The chosen root in the real candidate coerces to candidateGenusFieldBaseRoot hd.

@[simp]

theorem TauCeti.Multiquadratic.candidateGenusFieldRealBaseRoot_sq {d : ℤ} (hd : Squarefree d) (hpos : 0 < d) : candidateGenusFieldRealBaseRoot hd hpos ^ 2 = (algebraMap ℚ ↥(candidateGenusFieldReal hd)) ↑d

The chosen root in the real candidate squares to d.

instance TauCeti.Multiquadratic.isTotallyReal_candidateGenusFieldReal {d : ℤ} (hd : Squarefree d) : NumberField.IsTotallyReal ↥(candidateGenusFieldReal hd)

The real genus-field candidate is totally real.

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

The real genus-field candidate is an abelian Galois extension of ℚ.

theorem TauCeti.Multiquadratic.finrank_adjoin_candidateGenusFieldRealBaseRoot {d : ℤ} (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) (hpos : 0 < d) : Module.finrank ℚ ↥ℚ⟮candidateGenusFieldRealBaseRoot hd hpos⟯ = 2

The quadratic subfield generated by the chosen base root inside the real candidate has degree two over ℚ.

theorem TauCeti.Multiquadratic.isUnramifiedIn_candidateGenusFieldReal {d : ℤ} (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) (hpos : 0 < d) (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮candidateGenusFieldRealBaseRoot hd hpos⟯)) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers ↥(candidateGenusFieldReal hd)) q

The real genus-field candidate is unramified over its quadratic base at every finite place. This descends from finite-place unramifiedness of the full prime-discriminant compositum; the canonical equivalence between the two copies of ℚ(√d) then identifies the base rings.

theorem TauCeti.Multiquadratic.isUnramifiedAtInfinitePlaces_candidateGenusFieldReal {d : ℤ} (hd : Squarefree d) (hpos : 0 < d) : IsUnramifiedAtInfinitePlaces ↥ℚ⟮candidateGenusFieldRealBaseRoot hd hpos⟯ ↥(candidateGenusFieldReal hd)

The real genus-field candidate is unramified at every infinite place over its embedded base. In fact its total reality makes it unramified at infinity over every subfield.

theorem TauCeti.Multiquadratic.exists_algHom_candidateGenusFieldReal {d : ℤ} {M : Type u_1} [Field M] [NumberField M] [IsAbelianGalois ℚ M] (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) (hpos : 0 < d) {z : M} (hz : z ^ 2 = (algebraMap ℤ M) d) (hfinite : ∀ (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮z⟯)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers M) q) (hinfinite : IsUnramifiedAtInfinitePlaces (↥ℚ⟮z⟯) M) : ∃ (φ : M →ₐ[ℚ] ↥(candidateGenusFieldReal hd)), φ z = candidateGenusFieldRealBaseRoot hd hpos

Every abelian Galois extension of ℚ containing the chosen square root and unramified everywhere over the quadratic base embeds into the real candidate. The narrow genus-field maximality first embeds it into the full prime-discriminant compositum. Unramifiedness at infinity over the real quadratic base makes the source totally real, so its image lies in the maximal totally real subfield. The embedding can then be adjusted to carry the chosen square root to the chosen root in the real candidate.