Genus fields of quadratic fields

This file gives an intrinsic characterization of the genus field and proves that the prime-discriminant compositum candidateGenusField hd has that characterization when d < 0. For positive nonsquare d, its maximal totally real subfield candidateGenusFieldReal hd has the same characterization.

For a chosen square root y² = d in an abelian extension L / ℚ, the predicate TauCeti.Multiquadratic.IsGenusField d L y says that:

• y generates a quadratic subfield of L;
• L is unramified over that subfield at every finite and infinite place; and
• every other abelian extension of ℚ with these properties embeds into L over ℚ, carrying its chosen square root to y.

The last clause is the maximality in the classical definition. It is stated by a universal property, rather than by choosing a maximal element of a collection of fields. The theorem IsGenusField.exists_algEquiv_apply_eq makes the resulting root-preserving uniqueness explicit.

For squarefree negative d, isGenusField_candidateGenusField assembles the arithmetic and archimedean inputs for the full compositum. For positive nonsquare d, isGenusField_candidateGenusFieldReal instead uses the descended finite-place theorem, total reality at the infinite places, and the real candidate's root-preserving maximality.

References

• D. A. Cox, Primes of the Form x² + ny², Section 6.A.
• F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, Section 2.2.

structure TauCeti.Multiquadratic.IsGenusField (d : ℤ) (L : Type u) [Field L] [NumberField L] (y : L) : Prop

An abelian extension L / ℚ, with a chosen quadratic subfield generated by y² = d, is a genus field when it is unramified over that subfield at every place and is maximal among abelian extensions with those properties.

This predicate is the ordinary, all-places notion. A narrow genus-field predicate for real quadratic fields, imposing only the finite-place condition, remains future work.

• root_sq : y ^ 2 = (algebraMap ℤ L) d

  The chosen element is a square root of the radicand.

• finrank_adjoin : Module.finrank ℚ ↥ℚ⟮y⟯ = 2

  The chosen root generates a quadratic subfield.

• isAbelianGalois : IsAbelianGalois ℚ L

  The ambient extension is abelian and Galois over ℚ.

• isUnramifiedAtFinitePlaces (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮y⟯)) : q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers L) q

  The extension is unramified at every finite prime over its quadratic subfield.

• isUnramifiedAtInfinitePlaces : IsUnramifiedAtInfinitePlaces (↥ℚ⟮y⟯) L

  The extension is unramified at every infinite place over its quadratic subfield.

• maximal {M : Type v} [Field M] [NumberField M] [IsAbelianGalois ℚ M] {z : M} : z ^ 2 = (algebraMap ℤ M) d → (∀ (q : Ideal (NumberField.RingOfIntegers ↥ℚ⟮z⟯)), q.IsPrime → q ≠ ⊥ → Algebra.IsUnramifiedIn (NumberField.RingOfIntegers M) q) → IsUnramifiedAtInfinitePlaces (↥ℚ⟮z⟯) M → ∃ (φ : M →ₐ[ℚ] L), φ z = y

  Root-preserving maximality among abelian extensions unramified at every place over ℚ(√d).

theorem TauCeti.Multiquadratic.IsGenusField.exists_algEquiv_apply_eq {d : ℤ} {L : Type u} [Field L] [NumberField L] {M : Type v} [Field M] [NumberField M] {y : L} {z : M} (hL : IsGenusField d L y) (hM : IsGenusField d M z) : ∃ (e : L ≃ₐ[ℚ] M), e y = z

Any two genus fields for the same radicand are isomorphic as ℚ-algebras by an equivalence carrying one chosen square root to the other.

theorem TauCeti.Multiquadratic.isGenusField_candidateGenusField {d : ℤ} (hd : Squarefree d) (hneg : d < 0) : IsGenusField d (↥(candidateGenusField hd)) (candidateGenusFieldBaseRoot hd)

The prime-discriminant compositum is the genus field in the imaginary quadratic case. For a squarefree negative integer d, candidateGenusField hd is abelian over ℚ, is unramified at every place over its embedded copy of ℚ(√d), and admits a root-preserving embedding from every other abelian extension with those properties.

theorem TauCeti.Multiquadratic.isGenusField_candidateGenusFieldReal {d : ℤ} (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) (hpos : 0 < d) : IsGenusField d (↥(candidateGenusFieldReal hd)) (candidateGenusFieldRealBaseRoot hd hpos)

The maximal totally real subfield of the prime-discriminant compositum is the genus field in the real quadratic case. For positive squarefree d whose image in ℚ is not a square, the real candidate is abelian over ℚ, unramified at every finite and infinite place over its embedded copy of ℚ(√d), and admits a root-preserving embedding from every other abelian extension with those properties.