Relative degrees in the multiquadratic subfield lattice

For square roots root i of radicands d i over a field K with 2 ≠ 0, square-class independence makes M = K(rootᵢ : i) Galois with group (ℤ/2)ⁿ, and the order-reversing bijection TauCeti.Multiquadratic.intermediateFieldEquivSubmodule matches each intermediate field F of M / K with an 𝔽₂-subspace U of ι → ℤ/2 (TauCeti.NumberTheory.Multiquadratic.Subfield.Lattice). TauCeti.NumberTheory.Multiquadratic.Subfield.Degree records the absolute degree [F : K] = 2 ^ (n - dim U); this file records the complementary relative degree of the whole multiquadratic field over F.

The tower law [M : K] = [F : K] · [M : F] turns the absolute reading [F : K] · 2 ^ dim U = 2ⁿ into the relative one: cancelling [F : K] leaves

[M : F] = 2 ^ dim U.

So the two codimensions are genuinely complementary — [F : K] grows with the codimension of U, [M : F] grows with its dimension, and their product is the full degree 2ⁿ. The headline reading is the dual of the "quadratic subfields are the hyperplanes" characterisation: M is quadratic over F exactly when U is a line, dim U = 1. In particular, over any quadratic subfield of a degree-2ⁿ multiquadratic field, the multiquadratic field itself has degree 2 ^ (n - 1), the relative degree the genus-field constructions consume.

Main results

• TauCeti.Multiquadratic.finiteDimensional_top_over_intermediateField: M is finite-dimensional over any intermediate field F, the instance the relative degrees are read against.
• TauCeti.Multiquadratic.finrank_intermediateField_mul_finrank_top: the tower identity [F : K] · [M : F] = 2ⁿ.
• TauCeti.Multiquadratic.finrank_top_over_intermediateField: [M : F] = 2 ^ dim U, the relative degree of M over an intermediate field F through the dimension of its subspace U.
• TauCeti.Multiquadratic.finrank_top_over_intermediateField_eq_two_iff: M is quadratic over F exactly when U is a line, dim U = 1.
• TauCeti.Multiquadratic.finrank_top_over_intermediateField_of_finrank_eq_two: over a quadratic subfield, [M : F] = 2 ^ (n - 1).
• TauCeti.Multiquadratic.finrank_top_over_adjoin_range_ne: M is quadratic over the compositum of all but one of its roots.

Provenance

The subfield/subspace dictionary and the absolute-degree reading this refines are migrated, with the rest of the multiquadratic Layer 0, from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture. The relative-degree reading assembles that absolute reading with Mathlib's tower law (Module.finrank_mul_finrank).

theorem TauCeti.Multiquadratic.finiteDimensional_top_over_intermediateField {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {d : ι → K} {root : ι → L} [Finite ι] (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) (F : IntermediateField K ↥(IntermediateField.adjoin K (Set.range root))) : FiniteDimensional ↥F ↥(IntermediateField.adjoin K (Set.range root))

A multiquadratic field is finite-dimensional over any intermediate field.

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

The tower identity [F : K] · [M : F] = 2ⁿ. Under square-class independence, an intermediate field F of M = K(rootᵢ : i) and the whole multiquadratic field multiply their degrees to the full degree 2 ^ |ι|: the absolute degree [F : K] times the relative degree [M : F].

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

The relative degree of a multiquadratic field over an intermediate field. Under square-class independence, the whole multiquadratic field M = K(rootᵢ : i) has degree 2 ^ dim U over an intermediate field F, where U is the 𝔽₂-subspace of ι → ℤ/2 attached to F. This is the reciprocal partner of TauCeti.Multiquadratic.finrank_intermediateField_eq_two_pow: [F : K] reads the codimension of U, [M : F] reads its dimension, and their product is the full degree.

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

M is quadratic over F exactly when its subspace is a line. Under square-class independence, the multiquadratic field M = K(rootᵢ : i) has degree 2 over an intermediate field F exactly when the 𝔽₂-subspace U of ι → ℤ/2 attached to F is a line, dim U = 1. This is the dual of "the quadratic subfields are the hyperplanes" (TauCeti.Multiquadratic.finrank_intermediateField_eq_two_iff).

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

The relative degree over a quadratic subfield is 2 ^ (n - 1). Under square-class independence, over any quadratic subfield F of the degree-2ⁿ multiquadratic field M = K(rootᵢ : i), the multiquadratic field itself has degree 2 ^ (|ι| - 1). This is the relative degree that the genus-field constructions read off over the quadratic base.

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

A multiquadratic field is quadratic over the compositum of all but one of its roots. If the square-class independent roots root i generate the whole field L over K, then omitting the root indexed by i leaves a subfield of index two: the absolute degrees are 2 ^ |ι| and 2 ^ (|ι| - 1), so the tower law gives relative degree 2. This is the transverse degree the genus-field constructions read off at the prime belonging to the omitted root.