Quadratic subfields of a multiquadratic field from subset products

For square roots root i of radicands d i ∈ K over a field K, the subset-product root ∏_{i ∈ S} root i squares into K: its square is the subset product ∏_{i ∈ S} d i of the radicands. Each subset therefore names a simple subfield K(∏_{i ∈ S} root i) of the multiquadratic field M = K(rootᵢ : i). Under square-class independence the nonempty ones are genuinely quadratic (TauCeti.IntermediateField.finrank_adjoin_simple_eq_two_of_not_isSquare, which asks nothing of the characteristic), and when 2 ≠ 0 they are pairwise distinct: the assignment S ↦ K(∏_{i ∈ S} root i) is injective on all finite subsets of the index type, the empty subset going to K. This gives a concrete, arithmetic family of quadratic subfields that the genus-field constructions consume, complementing the abstract subfield/subspace dictionary of TauCeti.NumberTheory.Multiquadratic.Subfield.Lattice and TauCeti.NumberTheory.Multiquadratic.Subfield.Degree (where a quadratic subfield is characterised as a hyperplane of 𝔽₂ⁿ).

The engine for distinctness is the standalone same-square-class criterion for simple quadratic extensions, TauCeti.IntermediateField.isSquare_mul_of_adjoin_simple_eq: two square roots generate the same simple extension only when their radicands lie in the same square class.

Main results

• TauCeti.Multiquadratic.prod_root_sq: (∏_{i ∈ S} root i)² = ∏_{i ∈ S} d i.
• TauCeti.Multiquadratic.prod_root_mem_adjoin: the subset-product root lies in M.
• TauCeti.Multiquadratic.adjoin_prod_root_injective: distinct subsets give distinct subset-product subfields.
• TauCeti.Multiquadratic.not_isSquare_prod_of_notMem_adjoin_erase: if no root lies in the field generated by the others, no nonempty subset product of radicands is a square.

Provenance

The one-step quadratic normal form this rests on (TauCeti.IntermediateField.mem_sup_adjoin_sq, IntermediateField.finrank_sup_adjoin_simple_eq_mul_two) is migrated, with the rest of the basic multiquadratic theory, from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture. The subset-product description of the quadratic subfields is assembled here from that normal form.

theorem TauCeti.Multiquadratic.prod_root_sq {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] [Algebra K L] {ι : Type u_3} {d : ι → K} {root : ι → L} (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) (S : Finset ι) : (∏ i ∈ S, root i) ^ 2 = (algebraMap K L) (∏ i ∈ S, d i)

The square of a subset-product root. The product ∏_{i ∈ S} root i of the chosen roots over a finite subset S squares to the subset product ∏_{i ∈ S} d i of the radicands.

theorem TauCeti.Multiquadratic.prod_root_mem_adjoin {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {root : ι → L} (S : Finset ι) : ∏ i ∈ S, root i ∈ IntermediateField.adjoin K (Set.range root)

A subset-product root lies in the multiquadratic field. Each ∏_{i ∈ S} root i is a product of generators of M = K(rootᵢ : i), hence a member of M.

theorem TauCeti.Multiquadratic.adjoin_prod_root_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {d : ι → K} {root : ι → L} [NeZero 2] (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) (hindep : ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)) : Function.Injective fun (S : Finset ι) => K⟮∏ i ∈ S, root i⟯

Distinct subsets give distinct subset-product subfields. Under square-class independence the map S ↦ K(∏_{i ∈ S} root i) from the finite subsets of the index type to the intermediate fields of L / K is injective; the empty subset goes to K itself.

theorem TauCeti.Multiquadratic.not_isSquare_prod_of_notMem_adjoin_erase {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {d : ι → K} {root : ι → L} [DecidableEq L] {t : Finset L} (hd : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) (hroot_inj : Function.Injective root) (hroot_mem : ∀ (i : ι), root i ∈ t) (hnotmem : ∀ x ∈ t, x ∉ IntermediateField.adjoin K ↑(t.erase x)) (S : Finset ι) : S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)

Minimality forces square-class independence. Let t be a finite set of square roots such that no member of t lies in the field generated by the others, enumerated injectively by root, with radicands d (no root is zero, since zero lies in every field). Then no nonempty subset product of the radicands is a square: the corresponding product of roots is ± c for a root of that square c, so it would put one of the roots into the field spanned by the others.