The relative degree [K_{n+1} : K_n] #
K_{n+1} is generated over K_n by square roots of the shifted roots β - a of f_n
(rootShift), so its relative degree is 2 to the power of 2^n minus the dimension of the
𝔽₂-space of multiplicative relations among them (relfinrank_succ_eq_pow). The relation space is
trivial exactly when c_{n+1} is not a square in K_n, which is Lemma 1.6 (degree_criterion);
Lemma 1.5 (kummer_extension_criterion) then says which rationals stay non-squares in K_n.
Part of the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials,
Arch. Math. 59 (1992), 239-244; see QuadraticIterates.ArchMath1992.
The relative degree [K_{n+1} : K_n] #
The shifted root β - a of f_n, as an element of K_n: these are the radicands whose
square roots generate K_{n+1} over K_n.
Equations
- QuadraticIterates.rootShift a n β = ⟨↑β - ↑a, ⋯⟩
Instances For
The relative degree [K_{n+1} : K_n] equals 2 ^ (2^n - d), where d is the 𝔽₂-dimension
of the multiquadratic relations among the shifted roots β - a of f_n.
The degree criterion and the Kummer extension criterion #
If -a is not a rational square, K_1 = ℚ(√(-a)) has degree 2 over ℚ.
Lemma 1.6: if f_n is irreducible over ℚ, then [K_{n+1} : K_n] = 2^{2^n} iff c_{n+1}
is not a square in K_n.
If Ω_n ≅ [C_2]^n and the c_i are 2-independent with square roots x i in K_n, then for
nonzero c : ℚ, the image of c in K_n is a square iff it is the square of some
z ∈ IntermediateField.adjoin ℚ (Set.range x).
Lemma 1.5: if Ω_n ≅ [C_2]^n and c_1, …, c_n are 2-independent, then a nonzero c ∈ ℚ is a
non-square in K_n iff c_1, …, c_n, c are 2-independent.