Square-class descent in multiquadratic towers

For a sequence of chosen square roots root : ℕ → L over a base field K, the tower sqrtTower root n = K(root₀, …, rootₙ₋₁) is the intermediate field generated by the first n roots. This file proves square-class descent in characteristic not two: if an element y whose square is r : K lies in sqrtTower root n, then r is a square times a subset product of the corresponding radicands. The descent is proved for the roots indexed by an arbitrary finite set, and specialized to the tower and to a finite index type. The rational-real specialization only requires the nonnegativity hypotheses needed for Real.sqrt to supply the chosen roots.

This is the engine behind the degree computation [K(√d₀, …, √dₙ₋₁) : K] = 2ⁿ for square-class-independent radicands, and hence behind the structure theory of multiquadratic fields.

Main definitions and results

• TauCeti.Multiquadratic.sqrtTower: the tower K(root₀, …, rootₙ₋₁).
• TauCeti.Multiquadratic.sqrtTower_def: the defining adjoin restatement.
• TauCeti.Multiquadratic.mem_sqrtTower_iff: membership in the defining adjoin.
• TauCeti.Multiquadratic.sqrtTower_succ: the one-step recursion.
• TauCeti.Multiquadratic.sqrtTower_le_iff: the universal property of the tower.
• TauCeti.Multiquadratic.sqrtTower_eq_adjoin_fin_range: the bridge to a Fin n index.
• TauCeti.Multiquadratic.sqrtTower_root_mem: the listed roots lie in the tower.
• TauCeti.Multiquadratic.squareClass_of_sq_mem_finset: square-class descent for the roots indexed by a finite set.
• TauCeti.Multiquadratic.squareClass_of_sq_mem: square-class descent in the tower.
• TauCeti.Multiquadratic.squareClass_of_sq_mem_fintype: finite-index square-class descent.
• TauCeti.Multiquadratic.squareClass_of_sqrt_mem: rational-real square-class descent.

Provenance

This material is migrated from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture, where it was developed for one specific CM field. Here it is stated over an arbitrary base field of characteristic not two.

noncomputable def TauCeti.Multiquadratic.sqrtTower {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (root : ℕ → L) (n : ℕ) : IntermediateField K L

Iterated multiquadratic tower K(root₀, …, rootₙ₋₁) ⊆ L.

Equations

• TauCeti.Multiquadratic.sqrtTower root n = IntermediateField.adjoin K (root '' Set.Iio n)

theorem TauCeti.Multiquadratic.sqrtTower_def {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (root : ℕ → L) (n : ℕ) : sqrtTower root n = IntermediateField.adjoin K (root '' Set.Iio n)

The defining adjoin presentation of sqrtTower.

theorem TauCeti.Multiquadratic.mem_sqrtTower_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (root : ℕ → L) (n : ℕ) (x : L) : x ∈ sqrtTower root n ↔ x ∈ IntermediateField.adjoin K (root '' Set.Iio n)

Membership in sqrtTower in terms of the defining adjoin.

@[simp]

theorem TauCeti.Multiquadratic.sqrtTower_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (root : ℕ → L) : sqrtTower root 0 = ⊥

The zeroth multiquadratic tower is the base field.

@[simp]

theorem TauCeti.Multiquadratic.sqrtTower_succ {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (root : ℕ → L) (n : ℕ) : sqrtTower root (n + 1) = sqrtTower root n ⊔ K⟮root n⟯

Adjoining the next square root gives the successor stage of sqrtTower.

@[simp]

theorem TauCeti.Multiquadratic.sqrtTower_le_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (root : ℕ → L) (n : ℕ) (F : IntermediateField K L) : sqrtTower root n ≤ F ↔ ∀ j < n, root j ∈ F

The universal property of sqrtTower: it is the smallest intermediate field containing the first n chosen roots.

theorem TauCeti.Multiquadratic.sqrtTower_eq_adjoin_fin_range {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (root : ℕ → L) (n : ℕ) : sqrtTower root n = IntermediateField.adjoin K (Set.range fun (j : Fin n) => root ↑j)

The first n roots may equivalently be indexed by Fin n.

theorem TauCeti.Multiquadratic.sqrtTower_le_iff_fin {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (root : ℕ → L) (n : ℕ) (F : IntermediateField K L) : sqrtTower root n ≤ F ↔ ∀ (j : Fin n), root ↑j ∈ F

The universal property of sqrtTower using the finite index type Fin n.

theorem TauCeti.Multiquadratic.sqrtTower_root_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (root : ℕ → L) {j n : ℕ} (hj : j < n) : root j ∈ sqrtTower root n

A chosen root indexed before n lies in sqrtTower root n.

theorem TauCeti.Multiquadratic.sqrtTower_sq_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {root : ℕ → L} {j : ℕ} {a : K} (hroot : root j ^ 2 = (algebraMap K L) a) (n : ℕ) : root j ^ 2 ∈ sqrtTower root n

The square of a listed root lies in sqrtTower root n as soon as it is in the base field.

theorem TauCeti.Multiquadratic.squareClass_of_sq_mem_finset {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} (d : ι → K) (root : ι → L) (S : Finset ι) (hroot : ∀ i ∈ S, root i ^ 2 = (algebraMap K L) (d i)) [NeZero 2] {r : K} {y : L} (hy : y ^ 2 = (algebraMap K L) r) (hmem : y ∈ IntermediateField.adjoin K (root '' ↑S)) : ∃ T ⊆ S, ∃ (s : K), r = s ^ 2 * ∏ i ∈ T, d i

Square-class descent over a finite set of indices. In characteristic not two, if y² = r over K and y ∈ K(root i | i ∈ S), where root i is a chosen square root of d i, then r is a square times a subset product of the d i with i ∈ S.

theorem TauCeti.Multiquadratic.squareClass_of_sq_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (d : ℕ → K) (root : ℕ → L) {n : ℕ} (hroot : ∀ j < n, root j ^ 2 = (algebraMap K L) (d j)) [NeZero 2] {r : K} {y : L} (hy : y ^ 2 = (algebraMap K L) r) (hmem : y ∈ sqrtTower root n) : ∃ (T : Finset ℕ) (s : K), ↑T ⊆ Set.Iio n ∧ r = s ^ 2 * ∏ j ∈ T, d j

Square-class descent. In characteristic not two, if y² = r over K and y ∈ K(root₀, …, rootₙ₋₁), where root j is a chosen square root of d j, then r is a square times a subset product of the d j with j < n.

theorem TauCeti.Multiquadratic.squareClass_of_sq_mem_fintype {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} [Finite ι] (d : ι → K) (root : ι → L) (hroot : ∀ (j : ι), root j ^ 2 = (algebraMap K L) (d j)) [NeZero 2] {r : K} {y : L} (hy : y ^ 2 = (algebraMap K L) r) (hmem : y ∈ IntermediateField.adjoin K (Set.range root)) : ∃ (T : Finset ι) (s : K), r = s ^ 2 * ∏ j ∈ T, d j

Finite-index square-class descent. If y² = r over K and y ∈ K(root i | i : ι) for a finite index type ι, where root i is a chosen square root of d i, then r is a square times a subset product of the d i.

theorem TauCeti.Multiquadratic.squareClass_of_sqrt_mem (c : ℕ → ℚ) {n : ℕ} (hc : ∀ j < n, 0 ≤ c j) {r : ℚ} (hr : 0 ≤ r) (hmem : √↑r ∈ sqrtTower (fun (j : ℕ) => √↑(c j)) n) : ∃ (T : Finset ℕ) (s : ℚ), ↑T ⊆ Set.Iio n ∧ r = s ^ 2 * ∏ j ∈ T, c j

Square-class descent for real rational square roots. If r is a nonnegative rational with √r ∈ ℚ(√c₀, …, √cₙ₋₁) and every c j with j < n is nonnegative, then r is a rational square times a subset product of the c j.

theorem TauCeti.Multiquadratic.sq_sqrt_intCast {n : ℤ} (hn : 0 ≤ n) : √↑n ^ 2 = (algebraMap ℚ ℝ) ↑n

The real square root of a nonnegative integer squares back to its rational value, in the form (√n)² = algebraMap ℚ ℝ n. This supplies the hroot hypothesis of the degree theorem for the real square roots of integer radicands; sq_sqrt_natCast is its natural-number counterpart.