Documentation

TauCeti.NumberTheory.Multiquadratic.CandidateGenusField.Real.FixedField

The real candidate genus field as a fixed field #

The candidate genus field is an abelian Galois subfield of ℂ. Complex conjugation preserves it: each chosen generator has rational square, so its conjugate is that generator or its negative. This gives an automorphism candidateGenusFieldConj hd of the candidate field.

The automorphism negates exactly the roots belonging to negative prime discriminants. Its fixed field is the maximal totally real subfield candidateGenusFieldReal hd. This description is the field-theoretic input for comparing the ordinary genus field of a real quadratic field with the ordinary elementary-2 class-group quotient.

The fixed-field description 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 #

Main results #

source
noncomputable def TauCeti.Multiquadratic.candidateGenusFieldConj {d : ℤ} (hd : Squarefree d) :
Gal(↥(candidateGenusField hd)/ℚ)

Complex conjugation on the candidate genus field. The compositum of the chosen square roots of prime-discriminant radicands is stable under complex conjugation, because the conjugate of each root is either that root or its negative.

Instances For
    source
    @[simp]
    theorem TauCeti.Multiquadratic.coe_candidateGenusFieldConj_apply {d : ℤ} (hd : Squarefree d) (x : ↥(candidateGenusField hd)) :
    ↑((candidateGenusFieldConj hd) x) = star ↑x

    The restriction of complex conjugation has the expected value in the ambient field ℂ.

    source
    @[simp]
    theorem TauCeti.Multiquadratic.candidateGenusFieldConj_apply_gen {d : ℤ} (hd : Squarefree d) (P : ↥(genusPrimeDiscriminants hd)) :
    (candidateGenusFieldConj hd) (candidateGenusFieldGen hd P) = if ↑P < 0 then -candidateGenusFieldGen hd P else candidateGenusFieldGen hd P

    Complex conjugation negates exactly the negative prime-discriminant generators.

    source
    theorem TauCeti.Multiquadratic.candidateGenusFieldSignPattern_conj_apply {d : ℤ} (hd : Squarefree d) (P : ↥(genusPrimeDiscriminants hd)) :
    candidateGenusFieldSignPattern hd (candidateGenusFieldConj hd) P = if ↑P < 0 then 1 else 0

    The sign pattern of complex conjugation is supported exactly on the negative prime discriminants. This is the coordinate form used by the relative Galois-group quotient.

    This is not a simp lemma because its left-hand side already reduces through the coordinate and generator-action simp lemmas.

    source
    theorem TauCeti.Multiquadratic.candidateGenusFieldConj_apply_eq_self_iff {d : ℤ} (hd : Squarefree d) (x : ↥(candidateGenusField hd)) :
    (candidateGenusFieldConj hd) x = x ↔ x ∈ candidateGenusFieldReal hd

    An element of the candidate genus field is fixed by complex conjugation exactly when it lies in the maximal totally real subfield.

    source
    theorem TauCeti.Multiquadratic.mem_map_candidateGenusFieldReal_iff {d : ℤ} (hd : Squarefree d) (x : ℂ) :
    x ∈ IntermediateField.map (candidateGenusField hd).val (candidateGenusFieldReal hd) ↔ x ∈ candidateGenusField hd ∧ star x = x

    The real candidate, viewed in ℂ, is the set of real elements of the candidate. A complex number lies in the image of candidateGenusFieldReal hd exactly when it lies in the candidate genus field and is fixed by complex conjugation.

    source
    theorem TauCeti.Multiquadratic.fixedField_zpowers_candidateGenusFieldConj {d : ℤ} (hd : Squarefree d) :
    IntermediateField.fixedField (Subgroup.zpowers (candidateGenusFieldConj hd)) = candidateGenusFieldReal hd

    The maximal totally real subfield is the fixed field of complex conjugation. Equivalently, the ordinary real candidate is obtained from the full prime-discriminant compositum by fixing the cyclic subgroup generated by the automorphism that negates its negative-radicand roots.

    source
    theorem TauCeti.Multiquadratic.fixingSubgroup_candidateGenusFieldReal {d : ℤ} (hd : Squarefree d) :
    (candidateGenusFieldReal hd).fixingSubgroup = Subgroup.zpowers (candidateGenusFieldConj hd)

    The subgroup fixing the real candidate is generated by complex conjugation. This is the kernel subgroup in the Galois correspondence, including the totally real case where conjugation is the identity and the subgroup is trivial.