The degree of a multiquadratic field

For square roots root j of radicands d j over a field K (characteristic not two), the multiquadratic field K(root₀, …, rootₙ₋₁) has degree 2ⁿ over K when the radicands are square-class independent: no nonempty subset product ∏_{j ∈ S} d j is a square. Each tower step adjoins a root of the degree-two polynomial X² - d j, doubling the degree, and square-class descent shows the new root is genuinely outside the previous stage.

Main results

• TauCeti.Multiquadratic.finrank_sqrtTower: [K(root₀,…,rootₙ₋₁) : K] = 2ⁿ.
• TauCeti.Multiquadratic.finrank_adjoin_range: the same over a finite index type, [K(rootᵢ : i) : K] = 2^|ι| — the multiquadratic degree target.
• TauCeti.Multiquadratic.finrank_adjoin_range_ne: omitting one root from the generating family gives [K(rootⱼ : j ≠ i) : K] = 2^(|ι| - 1).

Provenance

The tower-degree induction is migrated and generalised from the declaration sqrtTower_finrank in ErdosUnitDistance/MultiquadraticField.lean in kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture.

theorem TauCeti.Multiquadratic.finrank_sqrtTower {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {d : ℕ → K} {root : ℕ → L} (hroot : ∀ (j : ℕ), root j ^ 2 = (algebraMap K L) (d j)) [NeZero 2] (n : ℕ) : (∀ (S : Finset ℕ), S.Nonempty → ↑S ⊆ Set.Iio n → ¬IsSquare (∏ j ∈ S, d j)) → Module.finrank K ↥(sqrtTower root n) = 2 ^ n

Degree of a multiquadratic tower. If no nonempty subset product of the radicands d j (j < n) is a square in K, then [K(root₀, …, rootₙ₋₁) : K] = 2ⁿ.

theorem TauCeti.Multiquadratic.finrank_adjoin_range {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} [Finite ι] {d : ι → K} {root : ι → L} (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) [NeZero 2] (hindep : ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)) : Module.finrank K ↥(IntermediateField.adjoin K (Set.range root)) = 2 ^ Nat.card ι

Degree of a multiquadratic field over a finite index. If no nonempty subset product of the radicands d i is a square in K, then [K(rootᵢ : i) : K] = 2^|ι|.

theorem TauCeti.Multiquadratic.finrank_adjoin_range_ne {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} [Finite ι] {d : ι → K} {root : ι → L} (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) [NeZero 2] (hindep : ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)) (i : ι) : Module.finrank K ↥(IntermediateField.adjoin K (Set.range fun (j : { j : ι // j ≠ i }) => root ↑j)) = 2 ^ (Nat.card ι - 1)

Degree of the compositum of all but one of the roots. If no nonempty subset product of the radicands d i is a square in K, then omitting the root indexed by i from the generating family lowers the degree by one power of two: [K(rootⱼ : j ≠ i) : K] = 2^(|ι| - 1).