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). That bijection records which subfields exist; this file records their degrees.

Galois theory reads the degree of an intermediate field as the index of its fixing subgroup (IntermediateField.finrank_eq_fixingSubgroup_index), and the fixing subgroup is exactly the subgroup of (ℤ/2)ⁿ carried by U. Counting gives the clean reciprocal relation

[F : K] · |U| = 2ⁿ,

equivalently [F : K] = 2 ^ (n - dim U): a larger subfield matches a smaller subspace, and the two codimensions add up to n. The headline consequence is the identification of the quadratic subfields: F has degree 2 over K exactly when its subspace U is a hyperplane, dim U + 1 = n.

Main results

• TauCeti.Multiquadratic.finrank_mul_card_intermediateFieldEquivSubmodule: [F : K] · |U| = 2ⁿ, the degree of an intermediate field times the cardinality of its subspace.
• TauCeti.Multiquadratic.finrank_mul_two_pow_finrank_intermediateFieldEquivSubmodule: the same relation read through the dimension of U, [F : K] · 2 ^ dim U = 2ⁿ.
• TauCeti.Multiquadratic.finrank_intermediateField_eq_two_pow: the explicit-power form [F : K] = 2 ^ (n - dim U).
• TauCeti.Multiquadratic.finrank_intermediateField_eq_two_iff: F is a quadratic subfield of M exactly when its subspace is a hyperplane, dim U + 1 = n.

Provenance

The subfield/subspace dictionary this refines is 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 degree reading assembles Mathlib's Galois index formula (IntermediateField.finrank_eq_fixingSubgroup_index) with the subgroup-cardinality bookkeeping (Subgroup.index_mul_card, Subgroup.card_mapSubgroup).

theorem TauCeti.Multiquadratic.finrank_mul_card_intermediateFieldEquivSubmodule {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 * Nat.card ↥(OrderDual.ofDual ((intermediateFieldEquivSubmodule hroot hindep) F)) = 2 ^ Nat.card ι

The degree of an intermediate field times the size of its subspace is 2ⁿ. Under square-class independence, an intermediate field F of M = K(rootᵢ : i) and its subspace U = (intermediateFieldEquivSubmodule F).ofDual of ι → ℤ/2 satisfy [F : K] · |U| = 2 ^ |ι|. The Galois correspondence is order-reversing, so a larger subfield matches a smaller subspace and the two sizes multiply to the full degree.

theorem TauCeti.Multiquadratic.finrank_mul_two_pow_finrank_intermediateFieldEquivSubmodule {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 * 2 ^ Module.finrank (ZMod 2) ↥(OrderDual.ofDual ((intermediateFieldEquivSubmodule hroot hindep) F)) = 2 ^ Nat.card ι

The degree of an intermediate field through the dimension of its subspace. The reciprocal relation [F : K] · |U| = 2ⁿ read with |U| = 2 ^ dim U: [F : K] · 2 ^ dim U = 2 ^ |ι|.

theorem TauCeti.Multiquadratic.finrank_intermediateField_eq_two_pow {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 = 2 ^ (Nat.card ι - Module.finrank (ZMod 2) ↥(OrderDual.ofDual ((intermediateFieldEquivSubmodule hroot hindep) F)))

The degree of an intermediate field is 2 to the codimension of its subspace. Under square-class independence, an intermediate field F of M = K(rootᵢ : i) has [F : K] = 2 ^ (|ι| - dim U), where U is the 𝔽₂-subspace attached to F. This is the explicit-power form of the reciprocal relation [F : K] · |U| = 2ⁿ.

theorem TauCeti.Multiquadratic.finrank_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 K ↥F = 2 ↔ Module.finrank (ZMod 2) ↥(OrderDual.ofDual ((intermediateFieldEquivSubmodule hroot hindep) F)) + 1 = Nat.card ι

The quadratic subfields are the hyperplanes. Under square-class independence, an intermediate field F of M = K(rootᵢ : i) has degree 2 over K exactly when its subspace U of ι → ℤ/2 is a hyperplane, i.e. dim U + 1 = |ι|. This is the lattice reading of "the quadratic subfields of a multiquadratic field".