The iterates of X² + a, their splitting fields and Galois groups

The iterates f_n of f = X² + a, the splitting field K_n of f_n over ℚ taken inside AlgebraicClosure ℚ, the Galois group Ω_n = Gal(f_n/ℚ) and the iterated wreath product [C₂]ⁿ; the integer sequences c_n and b_n and the rescaled polynomial normPoly a; 2-independence of families of rationals. The main results here are Odoni's embedding Ω_n ↪ [C₂]ⁿ (odoni_embedding), the Kummer tower K_n ⊆ K_{n+1} with [K_{n+1} : K_n] ≤ 2^{2^n} (kummer_degree_bound), and Lemma 1.4 (embed_equiv).

Part of the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; see QuadraticIterates.ArchMath1992.

Notation

fℚ[a, n] is scoped notation for the iterate f_n viewed in ℚ[X].

noncomputable def QuadraticIterates.iteratedPoly {R : Type u_1} [CommSemiring R] (a : R) : ℕ → Polynomial R

The iterates f_n of f = X² + a over a commutative (semi)ring R: f_0 = X, f_{n+1} = f_n² + a. Over ℤ (R := ℤ) this is the sequence of the paper.

Equations

• QuadraticIterates.iteratedPoly a 0 = Polynomial.X
• QuadraticIterates.iteratedPoly a n.succ = QuadraticIterates.iteratedPoly a n ^ 2 + Polynomial.C a

@[simp]

theorem QuadraticIterates.iteratedPoly_zero {R : Type u_1} [CommSemiring R] (a : R) : iteratedPoly a 0 = Polynomial.X

theorem QuadraticIterates.iteratedPoly_succ {R : Type u_1} [CommSemiring R] (a : R) (n : ℕ) : iteratedPoly a (n + 1) = iteratedPoly a n ^ 2 + Polynomial.C a

theorem QuadraticIterates.map_iteratedPoly {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (φ : R →+* S) (a : R) (n : ℕ) : Polynomial.map φ (iteratedPoly a n) = iteratedPoly (φ a) n

Iterating commutes with any ring homomorphism: the image of f_n under φ is the n-th iterate over the codomain with parameter φ a.

theorem QuadraticIterates.iteratedPoly_succ_comp {R : Type u_1} [CommSemiring R] (a : R) (n : ℕ) : iteratedPoly a (n + 1) = (iteratedPoly a n).comp (Polynomial.X ^ 2 + Polynomial.C a)

f_{n+1} = f_n ∘ (X² + a): the iterate can also grow on the right.

theorem QuadraticIterates.iteratedPoly_add {R : Type u_1} [CommSemiring R] (a : R) (m n : ℕ) : iteratedPoly a (m + n) = (iteratedPoly a m).comp (iteratedPoly a n)

Iterates compose additively: f_{m+n} = f_m ∘ f_n.

def QuadraticIterates.«termFℚ[_,_]» : Lean.ParserDescr

fℚ[a, n] denotes the n-th iterate f_n = iteratedPoly a n, viewed in ℚ[X].

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev QuadraticIterates.splittingField (a : ℤ) (n : ℕ) : IntermediateField ℚ (AlgebraicClosure ℚ)

The splitting field K_n of f_n over ℚ, as the intermediate field of AlgebraicClosure ℚ generated by the roots of f_n.

Equations

• QuadraticIterates.splittingField a n = IntermediateField.adjoin ℚ ((Polynomial.map (Int.castRingHom ℚ) (QuadraticIterates.iteratedPoly a n)).rootSet (AlgebraicClosure ℚ))

instance QuadraticIterates.splittingField.instIsSplittingField (a : ℤ) (n : ℕ) : Polynomial.IsSplittingField ℚ (↥(splittingField a n)) (Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a n))

instance QuadraticIterates.splittingField.instFiniteDimensional (a : ℤ) (n : ℕ) : FiniteDimensional ℚ ↥(splittingField a n)

instance QuadraticIterates.splittingField.instIsGalois (a : ℤ) (n : ℕ) : IsGalois ℚ ↥(splittingField a n)

@[reducible, inline]

noncomputable abbrev QuadraticIterates.GaloisGroup (a : ℤ) (n : ℕ) : Type

The Galois group Ω_n = Gal(f_n/ℚ) of the n-th iterate, via Mathlib's Polynomial.Gal.

Equations

• QuadraticIterates.GaloisGroup a n = (Polynomial.map (Int.castRingHom ℚ) (QuadraticIterates.iteratedPoly a n)).Gal

@[reducible, inline]

abbrev QuadraticIterates.WreathPower (n : ℕ) : Type

The n-fold iterated regular wreath product [C_2]^n of C_2 = Multiplicative (ZMod 2), via Mathlib's IteratedWreathProduct.

Equations

• QuadraticIterates.WreathPower n = IteratedWreathProduct (Multiplicative (ZMod 2)) n

The sequences c and b over ℤ

theorem QuadraticIterates.evenPoly_X_sq_add_C {R : Type u_1} [CommSemiring R] (a : R) : EvenPoly (Polynomial.X ^ 2 + Polynomial.C a)

X² + a is an even polynomial.

theorem QuadraticIterates.evenPoly_C_mul_X_sq_add_C {R : Type u_1} [CommSemiring R] (b c : R) : EvenPoly (Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c)

b·X² + c is an even polynomial.

noncomputable def QuadraticIterates.cSeq (a : ℤ) : ℕ → ℤ

The integer sequence c_n (indexed from 1): c_1 = -a, c_{n+1} = c_n² + a; the value at index 0 is 0. It is the γ-sequence of X² + a with ε = -1.

Equations

• QuadraticIterates.cSeq a = QuadraticIterates.gammaSeq (Polynomial.X ^ 2 + Polynomial.C a) (-1)

theorem QuadraticIterates.cSeq_eq_gammaSeq (a : ℤ) (n : ℕ) : cSeq a n = gammaSeq (Polynomial.X ^ 2 + Polynomial.C a) (-1) n

c_n = γ_n(X² + a, ε = -1) (definitional).

@[simp]

theorem QuadraticIterates.cSeq_zero (a : ℤ) : cSeq a 0 = 0

@[simp]

theorem QuadraticIterates.cSeq_one (a : ℤ) : cSeq a 1 = -a

theorem QuadraticIterates.cSeq_succ (a : ℤ) {n : ℕ} (hn : 1 ≤ n) : cSeq a (n + 1) = cSeq a n ^ 2 + a

The recursion c_{n+1} = c_n² + a, valid for n ≥ 1.

theorem QuadraticIterates.cSeq_two (a : ℤ) : cSeq a 2 = a ^ 2 + a

theorem QuadraticIterates.cSeq_gcd (a : ℤ) (m n : ℕ) : (cSeq a m).gcd (cSeq a n) = (cSeq a (m.gcd n)).natAbs

Strong divisibility for the c-sequence: gcd (c_m) (c_n) = |c_{gcd m n}|.

theorem QuadraticIterates.cSeq_associated_gcd (a : ℤ) (m n : ℕ) : Associated (gcd (cSeq a m) (cSeq a n)) (cSeq a (m.gcd n))

Strong divisibility of the c-sequence in the Associated-of-gcd form consumed by the moebiusFactorR API.

theorem QuadraticIterates.cSeq_succ_eq_neg_one_pow_mul_eval (a : ℤ) (k : ℕ) : cSeq a (k + 1) = (-1) ^ 2 ^ k * Polynomial.eval a (iteratedPoly a k)

c_{k+1} = (-1)^{2^k} · f_k(a); in particular c_{k+1} = f_k(a) for k ≥ 1.

noncomputable def QuadraticIterates.bSeq (a : ℤ) (n : ℕ) : ℤ

The Möbius factors b_n = ∏_{d ∣ n} c_d^{μ(n/d)} ∈ ℤ of the c-sequence: the specialization of the general β-sequence to X² + a, ε = -1 (an integer by strong divisibility, see intCast_bSeq).

Equations

• QuadraticIterates.bSeq a n = QuadraticIterates.betaSeq (Polynomial.X ^ 2 + Polynomial.C a) (-1) n

theorem QuadraticIterates.bSeq_eq_moebiusFactorR (a : ℤ) (n : ℕ) : bSeq a n = moebiusFactorR (cSeq a) n

@[simp]

theorem QuadraticIterates.bSeq_one (a : ℤ) : bSeq a 1 = -a

noncomputable def QuadraticIterates.normPoly (a : ℤ) : Polynomial ℤ

The rescaling |a|·X² + sign a of X² + a. Substituting x ↦ |a|·x turns the recursion c_{n+1} = c_n² + a into the γ-recursion of normPoly a, whose sequence is therefore |c_n| / |a| (abs_cSeq_eq_gammaSeq_mul_abs) — in particular positive, which is what Lemma 2.2 needs and X² + a itself does not provide.

Equations

• QuadraticIterates.normPoly a = Polynomial.C |a| * Polynomial.X ^ 2 + Polynomial.C a.sign

@[simp]

theorem QuadraticIterates.eval_normPoly (a x : ℤ) : Polynomial.eval x (normPoly a) = |a| * x ^ 2 + a.sign

theorem QuadraticIterates.evenPoly_normPoly (a : ℤ) : EvenPoly (normPoly a)

2-independence of families of rationals

def QuadraticIterates.TwoIndependent {n : ℕ} (v : Fin n → ℚ) : Prop

Nonzero rationals a_1, …, a_n are 2-independent if their classes in ℚ*/(ℚ*)² are 𝔽₂-linearly independent: no nonempty subfamily has product a square in ℚ.

Equations

• QuadraticIterates.TwoIndependent v = ((∀ (i : Fin n), v i ≠ 0) ∧ ∀ (S : Finset (Fin n)), S.Nonempty → ¬IsSquare (∏ i ∈ S, v i))

theorem QuadraticIterates.TwoIndependent.sqrt_injective {n : ℕ} {v : Fin n → ℚ} (hv : TwoIndependent v) {K : Type u_1} [Field K] [Algebra ℚ K] {x : Fin n → K} (hx : ∀ (i : Fin n), x i ^ 2 = (algebraMap ℚ K) (v i)) : Function.Injective x

Square roots of 2-independent rationals in a ℚ-algebra are pairwise distinct.

theorem QuadraticIterates.TwoIndependent.of_snoc {n : ℕ} {v : Fin n → ℚ} {c : ℚ} (h : TwoIndependent (Fin.snoc v c)) : TwoIndependent v

2-independence of Fin.snoc v c restricts to the initial family v.

theorem QuadraticIterates.twoIndependent_iff_linearIndependent {n : ℕ} (v : Fin n → ℚ) : TwoIndependent v ↔ LinearIndependent (ZMod 2) fun (i : Fin n) => sqClass (v i)

A family of rationals is 2-independent iff the family of its classes in ℚˣ/(ℚˣ)² is 𝔽₂-linearly independent.

Degrees, roots and the Galois group of the iterates over ℚ

theorem QuadraticIterates.natDegree_iteratedPoly (a : ℤ) (n : ℕ) : (iteratedPoly a n).natDegree = 2 ^ n

theorem QuadraticIterates.map_iteratedPoly_succ_eq_sq_add (a : ℤ) (k : ℕ) : Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a (k + 1)) = Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a k) ^ 2 + Polynomial.C ↑a

theorem QuadraticIterates.map_iteratedPoly_one (a : ℤ) : Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a 1) = Polynomial.X ^ 2 + Polynomial.C ↑a

theorem QuadraticIterates.map_iteratedPoly_succ (a : ℤ) (k : ℕ) : Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a (k + 1)) = (Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a k)).comp (Polynomial.X ^ 2 + Polynomial.C ↑a)

theorem QuadraticIterates.monic_iteratedPoly (a : ℤ) (n : ℕ) : (iteratedPoly a n).Monic

theorem QuadraticIterates.ncard_rootSet_iteratedPoly_le (a : ℤ) (n : ℕ) : ((Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a n)).rootSet (AlgebraicClosure ℚ)).ncard ≤ 2 ^ n

theorem QuadraticIterates.mem_rootSet_iteratedPoly_succ (a : ℤ) (n : ℕ) (β : AlgebraicClosure ℚ) : β ∈ (Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a (n + 1))).rootSet (AlgebraicClosure ℚ) ↔ β ^ 2 + ↑a ∈ (Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a n)).rootSet (AlgebraicClosure ℚ)

theorem QuadraticIterates.pow_two_pow_apply_root (a : ℤ) (ϕ : Gal(AlgebraicClosure ℚ/ℚ)) {m : ℕ} {γ : AlgebraicClosure ℚ} (hγ : γ ∈ (Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a m)).rootSet (AlgebraicClosure ℚ)) : (ϕ ^ 2 ^ m) γ = γ

Any ℚ-automorphism of its algebraic closure raised to the power 2 ^ m fixes every root of f_m.

theorem QuadraticIterates.isPGroup_galoisGroup (a : ℤ) (n : ℕ) : IsPGroup 2 (GaloisGroup a n)

Ω_n = Gal(f_n/ℚ) is a 2-group.

theorem QuadraticIterates.odoni_embedding (a : ℤ) (n : ℕ) : ∃ (φ : GaloisGroup a n →* WreathPower n), Function.Injective ⇑φ

Odoni's embedding theorem: Ω_n embeds into [C_2]^n.

theorem QuadraticIterates.exists_sq_eq_sub (a : ℤ) (α : AlgebraicClosure ℚ) : ∃ (β : AlgebraicClosure ℚ), β ^ 2 = α - ↑a

Every element of the algebraic closure of ℚ has a square root after subtracting a; the square roots of the α - a for α a root of f_n generate K_{n+1} over K_n.

theorem QuadraticIterates.splittingField_le_succ (a : ℤ) (n : ℕ) : splittingField a n ≤ splittingField a (n + 1)

theorem QuadraticIterates.splittingField_mono (a : ℤ) {m n : ℕ} (hmn : m ≤ n) : splittingField a m ≤ splittingField a n

@[simp]

theorem QuadraticIterates.splittingField_zero_eq_bot (a : ℤ) : splittingField a 0 = ⊥

K_0 = ℚ: the only root of f_0 = X is 0.

The Kummer tower K_n ⊆ K_{n+1}

theorem QuadraticIterates.relfinrank_succ_eq_finrank_adjoin (a : ℤ) (n : ℕ) (g : AlgebraicClosure ℚ → AlgebraicClosure ℚ) (hg : ∀ (α : AlgebraicClosure ℚ), g α ^ 2 = α - ↑a) : (splittingField a n).relfinrank (splittingField a (n + 1)) = Module.finrank ↥(splittingField a n) ↥(IntermediateField.adjoin (↥(splittingField a n)) (g '' (Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a n)).rootSet (AlgebraicClosure ℚ)))

K_{n+1} = K_n(√(α - a) : α root of f_n): the relative degree [K_{n+1} : K_n] is the degree of the multiquadratic extension of K_n generated by a choice of square roots of the α - a.

theorem QuadraticIterates.relfinrank_succ_le (a : ℤ) (n : ℕ) : (splittingField a n).relfinrank (splittingField a (n + 1)) ≤ 2 ^ 2 ^ n

theorem QuadraticIterates.kummer_degree_bound (a : ℤ) (n : ℕ) : splittingField a n ≤ splittingField a (n + 1) ∧ (splittingField a (n + 1) = splittingField a n ⊔ IntermediateField.adjoin ℚ ((Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a (n + 1))).rootSet (AlgebraicClosure ℚ)) ∧ ∀ β ∈ (Polynomial.map (Int.castRingHom ℚ) (iteratedPoly a (n + 1))).rootSet (AlgebraicClosure ℚ), β ^ 2 ∈ splittingField a n) ∧ (splittingField a n).relfinrank (splittingField a (n + 1)) ≤ 2 ^ 2 ^ n

Facts 1.0 (Kummer tower): K_n ⊆ K_{n+1}, the extension K_{n+1} is generated over K_n by roots of f_{n+1} whose squares lie in K_n, and [K_{n+1} : K_n] ≤ 2^{2^n}.

theorem QuadraticIterates.card_wreathPower (n : ℕ) : Nat.card (WreathPower n) = 2 ^ (2 ^ n - 1)

theorem QuadraticIterates.card_galoisGroup_eq_finrank (a : ℤ) (n : ℕ) : Nat.card (GaloisGroup a n) = Module.finrank ℚ ↥(splittingField a n)

theorem QuadraticIterates.embed_equiv (a : ℤ) (n : ℕ) : (∃ (φ : GaloisGroup a n →* WreathPower n), Function.Injective ⇑φ) ∧ (Nonempty (GaloisGroup a (n + 1) ≃* WreathPower (n + 1)) ↔ Nonempty (GaloisGroup a n ≃* WreathPower n) ∧ (splittingField a n).relfinrank (splittingField a (n + 1)) = 2 ^ 2 ^ n)

Lemma 1.4: Ω_n embeds into [C_2]^n, and Ω_{n+1} ≅ [C_2]^{n+1} iff Ω_n ≅ [C_2]^n and [K_{n+1} : K_n] = 2^{2^n}.