The candidate genus field of an imaginary quadratic field is totally complex

For squarefree d < 0, the embedded base ℚ(√d) inside candidateGenusField hd contains a square root of the negative rational d, so it is totally complex — a special case of NumberField.isTotallyComplex_of_sq_ratCast_of_neg. The candidate genus field, being an extension of the base, is then totally complex too (isTotallyComplex_of_algebra).

A totally complex base has no real infinite places, so the candidate genus field is unramified at every infinite place over its base (IsUnramifiedAtInfinitePlaces). This settles the archimedean half of the genus-field identification in the imaginary case.

Main results

• TauCeti.Multiquadratic.isTotallyComplex_candidateGenusFieldBase: the base ℚ(√d) is totally complex for d < 0.
• TauCeti.Multiquadratic.isTotallyComplex_candidateGenusField: so is the candidate genus field.
• TauCeti.Multiquadratic.isUnramifiedAtInfinitePlaces_candidateGenusField: for d < 0 the candidate genus field is unramified at all infinite places over its base.

theorem TauCeti.Multiquadratic.isTotallyComplex_candidateGenusFieldBase {d : ℤ} (hd : Squarefree d) (hneg : d < 0) : NumberField.IsTotallyComplex ↥(candidateGenusFieldBase hd)

The quadratic base ℚ(√d) inside the candidate genus field is totally complex for squarefree d < 0: it is generated by a square root of the negative rational d.

theorem TauCeti.Multiquadratic.isTotallyComplex_candidateGenusField {d : ℤ} (hd : Squarefree d) (hneg : d < 0) : NumberField.IsTotallyComplex ↥(candidateGenusField hd)

The candidate genus field of an imaginary quadratic field is totally complex. For squarefree d < 0 it is an extension of the totally complex base ℚ(√d).

theorem TauCeti.Multiquadratic.isUnramifiedAtInfinitePlaces_candidateGenusField {d : ℤ} (hd : Squarefree d) (hneg : d < 0) : IsUnramifiedAtInfinitePlaces ↥(candidateGenusFieldBase hd) ↥(candidateGenusField hd)

The candidate genus field is unramified at the infinite places over its base, for squarefree d < 0. The base ℚ(√d) is totally complex, so no infinite place of it is real and hence none ramifies. This is the archimedean half of the genus-field identification in the imaginary case.