Rational radicands reduce to squarefree integer radicands #
The multiquadratic degree theorem TauCeti.Multiquadratic.finrank_adjoin_range is field-generic:
its radicands are arbitrary elements d i of the base field. Over ℚ the roadmap works instead
with squarefree integers, because those are the radicands the genus theory names (the prime
discriminants -4, ±8, p* and their products). The passage between the two is a square-class
computation: a rational radicand may be replaced by the squarefree integer representing its square
class, and this changes neither the field generated nor the independence hypothesis.
This file carries out that reduction. Multiplying a radicand by a nonzero square multiplies its
root by a base scalar, so it leaves the generated field alone
(TauCeti.IntermediateField.adjoin_range_algebraMap_mul), and it leaves squareness of subset
products alone (isSquare_mul_sq_iff); every nonzero rational has a squarefree integer in its
square class (Rat.exists_squarefree_int_mul_sq). Combining these turns
ℚ(√d₁, …, √dₙ) for arbitrary nonzero rational dᵢ into ℚ(√a₁, …, √aₙ) for squarefree integers
aᵢ, and lets the degree theorem be fed an integral independence hypothesis.
The hindep hypothesis is stated over ℤ here — no nonempty subset product of the integer
representatives is a square integer — which is the form the integral criteria supply
(TauCeti.Multiquadratic.not_isSquare_prod_of_coprime_squarefree,
TauCeti.Multiquadratic.not_isSquare_prod_primes).
Main results #
TauCeti.Multiquadratic.isSquare_prod_iff_of_eq_mul_sq: a subset product of rational radicands is a square exactly when the corresponding subset product of their integer representatives is a square integer.TauCeti.Multiquadratic.finrank_adjoin_range_of_eq_mul_sq:[ℚ(√d₁, …, √dₙ) : ℚ] = 2^|ι|with the independence hypothesis read off the integer representatives.TauCeti.Multiquadratic.exists_squarefree_root_adjoin_eq: the reduction — a multiquadratic field overℚwith nonzero rational radicands is a multiquadratic field with squarefree integer radicands, generated by rescaled roots, together with the square-class witnesses relating the two.TauCeti.Multiquadratic.exists_squarefree_root_adjoin_range_eq_top: an exponent-two Galois extension ofℚis generated by square roots of a square-class independent family of squarefree integers.TauCeti.Multiquadratic.sq_sqrt_ratCast: the rational counterpart ofsq_sqrt_intCast, the square root of a nonnegative rational in the shape the degree theorem consumes.
A private worked example at the end of the file checks the reduction end to end:
[ℚ(√(8/9), √(3/4)) : ℚ] = 4, the radicands 8/9 and 3/4 having squarefree parts 2 and 3,
so that this is ℚ(√2, √3) in disguise.
Square-class transfer for subset products. If each rational radicand d i is an integer
representative a i times a nonzero square, then a subset product of the d i is a rational
square exactly when the corresponding subset product of the a i is an integer square. This is
what carries the square-class independence hypothesis between the rational and integral forms.
The a i are arbitrary integers here; squarefree representatives are one way to obtain such a
decomposition, via Rat.exists_squarefree_int_mul_sq.
The multiquadratic degree over ℚ, tested on integer representatives. Let d : ι → ℚ be
radicands, each written as an integer a i times the square of a nonzero rational c i, and let
root i be a square root of d i in a field L over ℚ. If no nonempty subset product of the
a i is a square integer, then [ℚ(rootᵢ : i) : ℚ] = 2^|ι|.
This is finrank_adjoin_range with its independence hypothesis moved to ℤ. The a i need not be
squarefree for the statement to hold — squarefreeness is only how one produces such a
decomposition, via Rat.exists_squarefree_int_mul_sq.
Rescaling a square root into the integral square class. If d = a * c ^ 2 with c ≠ 0
and x is a square root of d, then c⁻¹ * x is a square root of the integer a. This is the
root-level half of the square-class reduction: the rescaled root generates the same field
(TauCeti.IntermediateField.adjoin_range_algebraMap_mul) and satisfies an integral equation.
Rational radicands reduce to squarefree integer radicands. If the d i are nonzero
rationals with square roots root i in a field L over ℚ, then there are squarefree integers
a i and square roots root' i of them generating the same field:
ℚ(√d₁, …, √dₙ) = ℚ(√a₁, …, √aₙ). The new roots are the old ones rescaled by base scalars, so no
enlargement or shrinking of the field can occur.
The square-class witness comes out too: the nonzero rational c i with d i = a i * c i ^ 2, and
the defining equation root' i = (c i)⁻¹ * root i. A consumer therefore has everything needed to
push hypotheses across the reduction, for instance to feed isSquare_prod_iff_of_eq_mul_sq or
finrank_adjoin_range_of_eq_mul_sq with the squarefree representatives produced here.
The last conclusion is an equality of intermediate fields, so a property of the field itself — its
degree over ℚ, its Galois group, its subfields, the splitting behaviour of a prime in it —
transports along that equality from the squarefree integer radicands to the rational ones. It does
not transport the hypotheses: a theorem about squarefree integer radicands still has to be applied
to the particular a i produced here, with its own hypotheses (independence, coprimality, …)
established for them.
An exponent-two Galois extension of ℚ is generated by square roots of squarefree
integers. Let L / ℚ be a finite Galois extension whose Galois group has exponent dividing two.
Then there are square-class independent squarefree integers a₁, …, aₙ and chosen square roots in
L which generate all of L; in particular [L : ℚ] = 2ⁿ. Independence is stated integrally:
no nonempty subset product of the aᵢ is a square in ℤ.
The real square root of a nonnegative rational squares back to it, in the shape the degree
theorem consumes. This is the rational counterpart of sq_sqrt_intCast.