The subfield lattice of a multiquadratic field

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)ⁿ (TauCeti.NumberTheory.Multiquadratic.Galois.Group). The fundamental theorem of Galois theory turns the lattice of intermediate fields of M/K into the (order-reversed) lattice of subgroups of Gal(M/K); transporting along the isomorphism Gal(M/K) ≃ (ℤ/2)ⁿ lands in the subgroups of ι → ℤ/2, and an additive subgroup of an 𝔽₂-vector space is the same thing as an 𝔽₂-subspace. Composing these identifications gives an order-reversing bijection between the intermediate fields of M/K and the 𝔽₂-subspaces of ι → ℤ/2.

This is the lattice-of-subfields layer of the multiquadratic roadmap: the dictionary "subfields ↔ subspaces of 𝔽₂ⁿ" that organises, for instance, the quadratic subfields and the genus-field constructions.

Main results

• TauCeti.Multiquadratic.intermediateFieldEquivSubmodule: for square-class independent radicands, the order-reversing bijection IntermediateField K M ≃o (Submodule (ZMod 2) (ι → ℤ/2))ᵒᵈ.
• TauCeti.Multiquadratic.card_intermediateField_adjoin_range: its cardinality reading — the number of intermediate fields of M/K is the number of 𝔽₂-subspaces of ι → ℤ/2.

Provenance

The Galois-group identification this builds on 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 subfield/subspace dictionary itself assembles Mathlib's Galois correspondence (IsGalois.intermediateFieldEquivSubgroup) with the subgroup ↔ subspace order isomorphisms for 𝔽₂-vector spaces (Subgroup.toAddSubgroup', AddSubgroup.toZModSubmodule).

noncomputable def TauCeti.Multiquadratic.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)) : IntermediateField K ↥(IntermediateField.adjoin K (Set.range root)) ≃o (Submodule (ZMod 2) (ι → ZMod 2))ᵒᵈ

The subfield lattice of a multiquadratic field is the 𝔽₂-subspace lattice of (ℤ/2)ⁿ. If no nonempty subset product of the radicands d i is a square in K (and 2 ≠ 0), then the intermediate fields of M = K(rootᵢ : i) over K correspond, order-reversingly, to the 𝔽₂-subspaces of ι → ℤ/2: a larger subfield is fixed by a smaller group, hence matches a smaller subspace.

The bijection is the composite of Mathlib's Galois correspondence IsGalois.intermediateFieldEquivSubgroup (intermediate fields ↔ subgroups of the Galois group, dualised), the Galois-group isomorphism galoisGroupEquiv (Gal(M/K) ≃ Multiplicative (ι → ℤ/2)), and the identification of subgroups of an 𝔽₂-vector space with its subspaces.

@[simp]

theorem TauCeti.Multiquadratic.intermediateFieldEquivSubmodule_apply_ofDual {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))) : OrderDual.ofDual ((intermediateFieldEquivSubmodule hroot hindep) F) = (AddSubgroup.toZModSubmodule 2) (Subgroup.toAddSubgroup' ((galoisGroupEquiv hroot hindep).mapSubgroup F.fixingSubgroup))

The subspace attached to an intermediate field is the image of its fixing subgroup under the sign-pattern Galois-group equivalence.

theorem TauCeti.Multiquadratic.mem_intermediateFieldEquivSubmodule_apply_ofDual_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))) (v : ι → ZMod 2) : v ∈ OrderDual.ofDual ((intermediateFieldEquivSubmodule hroot hindep) F) ↔ ∃ σ ∈ F.fixingSubgroup, signPattern root σ = v

A sign vector belongs to the subspace attached to an intermediate field exactly when it is the sign pattern of an automorphism fixing that field.

@[simp]

theorem TauCeti.Multiquadratic.mem_intermediateFieldEquivSubmodule_symm_apply_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)) (U : Submodule (ZMod 2) (ι → ZMod 2)) (x : ↥(IntermediateField.adjoin K (Set.range root))) : x ∈ (intermediateFieldEquivSubmodule hroot hindep).symm (OrderDual.toDual U) ↔ ∀ (σ : Gal(↥(IntermediateField.adjoin K (Set.range root))/K)), signPattern root σ ∈ U → σ x = x

The intermediate field attached to a subspace is the fixed field of the automorphisms whose sign patterns lie in that subspace.

theorem TauCeti.Multiquadratic.card_intermediateField_adjoin_range {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)) : Nat.card (IntermediateField K ↥(IntermediateField.adjoin K (Set.range root))) = Nat.card (Submodule (ZMod 2) (ι → ZMod 2))

The number of subfields of a multiquadratic field. Under square-class independence, the intermediate fields of M = K(rootᵢ : i) over K are in bijection with the 𝔽₂-subspaces of ι → ℤ/2, so there are exactly as many of them. (For |ι| = n this count is the number of subspaces of 𝔽₂ⁿ, the Galois number Gₙ.)