Documentation

TauCeti.NumberTheory.Multiquadratic.CandidateGenusField.Relative.Degree

The candidate genus field over its quadratic base #

For a squarefree integer d, candidateGenusField hd contains a chosen square root of d. This file names that root and the resulting copy of ℚ(√d) inside the candidate genus field. When d is not a rational square, this base has degree two over ℚ, and the full candidate genus field has relative degree

[candidateGenusField hd : ℚ(√d)] = 2 ^ ((genusPrimeDiscriminants hd).card - 1).

The absolute degree 2 ^ (genusPrimeDiscriminants hd).card is proved in CandidateGenusField/Degree. The relative formula here combines that theorem with the quadratic degree of the base through the tower law [M : ℚ] = [ℚ(√d) : ℚ] · [M : ℚ(√d)].

This is the relative-degree part of the genus-field construction. For negative d, isGenusField_candidateGenusField identifies the candidate with the maximal extension satisfying the required 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 definitions #

Main results #

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

A chosen square root of d inside its candidate genus field. Existence follows from the prime-discriminant factorization of fundamentalDiscriminant d; no particular sign is selected.

Instances For
    source
    @[simp]
    theorem TauCeti.Multiquadratic.candidateGenusFieldBaseRoot_sq {d : ℤ} (hd : Squarefree d) :
    candidateGenusFieldBaseRoot hd ^ 2 = (algebraMap ℚ ↥(candidateGenusField hd)) ↑d

    The chosen base root squares to d.

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

    The copy of ℚ(√d) inside candidateGenusField hd, generated by the chosen square root of d. It is quadratic exactly in the nonsquare case used for quadratic fields.

    Instances For
      source
      theorem TauCeti.Multiquadratic.candidateGenusFieldBase_def {d : ℤ} (hd : Squarefree d) :
      candidateGenusFieldBase hd = ℚ⟮candidateGenusFieldBaseRoot hd⟯

      candidateGenusFieldBase presented as the simple extension generated by its chosen root.

      source
      @[simp]
      theorem TauCeti.Multiquadratic.candidateGenusFieldBaseRoot_mem {d : ℤ} (hd : Squarefree d) :
      candidateGenusFieldBaseRoot hd ∈ candidateGenusFieldBase hd

      The chosen square root of d lies in the quadratic base.

      source
      @[simp]
      theorem TauCeti.Multiquadratic.candidateGenusFieldBase_le_iff {d : ℤ} (hd : Squarefree d) {F : IntermediateField ℚ ↥(candidateGenusField hd)} :
      candidateGenusFieldBase hd ≤ F ↔ candidateGenusFieldBaseRoot hd ∈ F

      Universal property of the quadratic base. It lies below an intermediate field F exactly when F contains the chosen square root of d.

      source
      theorem TauCeti.Multiquadratic.finrank_candidateGenusFieldBase {d : ℤ} (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) :
      Module.finrank ℚ ↥(candidateGenusFieldBase hd) = 2

      The embedded base ℚ(√d) is quadratic. If d is not a square in ℚ, the simple subfield generated by the chosen square root of d has degree two over ℚ.

      source
      theorem TauCeti.Multiquadratic.finrank_candidateGenusField_over_candidateGenusFieldBase {d : ℤ} (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) :
      Module.finrank ↥(candidateGenusFieldBase hd) ↥(candidateGenusField hd) = 2 ^ ((genusPrimeDiscriminants hd).card - 1)

      Relative degree of the candidate genus field over ℚ(√d). If the squarefree integer d is not a rational square, the prime-discriminant compositum has degree 2 ^ (t - 1) over its embedded quadratic base, where t = (genusPrimeDiscriminants hd).card.