An exponent-two Galois extension is multiquadratic

TauCeti/NumberTheory/Multiquadratic/Galois shows that adjoining square roots of a square-class independent family gives a Galois extension (TauCeti.Multiquadratic.isGalois) whose group has exponent two (TauCeti.Multiquadratic.aut_exponent_dvd_two), while TauCeti/NumberTheory/Multiquadratic/Degree computes its degree as 2ⁿ (TauCeti.Multiquadratic.finrank_adjoin_range). This file proves the converse, which is exponent-two Kummer theory: over a field where 2 ≠ 0, a finite Galois extension whose group has exponent two is generated by square roots of elements of the base field, and one can take the radicands square-class independent, so the degree is again 2ⁿ.

The argument is the Galois correspondence plus one linear-algebra fact about the group, TauCeti.exists_le_index_eq_two_notMem_of_exponent_dvd_two: a subgroup of an elementary abelian 2-group avoiding an element lies in an index-two subgroup avoiding that element. The fixed field of such a subgroup is quadratic over K, hence generated by a square root (TauCeti.IntermediateField.exists_sq_mem_range_adjoin_simple_eq_of_finrank_eq_two, where completing the square is what needs 2 ≠ 0). This gives TauCeti.Multiquadratic.exists_sq_mem_range_apply_eq_neg_of_notMem: a nonzero square root fixed by the original subgroup and negated by the chosen automorphism. If some σ ≠ 1 fixed every square root, this lemma with the trivial subgroup would give a nonzero x both fixed and negated by σ, so 2 * x = 0, a contradiction. Thus the square roots generate, and finite-dimensionality cuts the generating set down to a finite one.

Square-class independence follows by choosing an inclusion-minimal subset of the given square roots that generates the same field: a square subset product would express one of its members through the others, contradicting minimality. Feeding the independent family back into TauCeti.Multiquadratic.finrank_adjoin_range gives [L : K] = 2ⁿ.

In genus theory, this identifies an abelian extension of a quadratic field as a compositum of quadratic fields once its Galois group over the rational numbers has exponent dividing two. The square-class descent and degree theorems then apply to that extension.

Exponent-two Kummer theory is classical; see for instance S. Lang, Algebra, VI §8, or D. A. Cox, Primes of the Form x² + ny², §6.A, where the genus field is described exactly this way.

Main results

In the namespace TauCeti.Multiquadratic:

• exists_sq_mem_range_apply_eq_neg_of_notMem: separate an automorphism from a subgroup by a nonzero square root fixed by that subgroup and negated by the automorphism.
• adjoin_setOf_sq_mem_range_eq_top: the square roots of elements of K that lie in L generate L over K.
• exists_finset_sq_mem_range_adjoin_eq_top: a finite set of such square roots already generates.
• exists_root_adjoin_eq_adjoin: any finite family of square roots can be replaced by a square-class independent subfamily generating the same intermediate field.
• exists_root_adjoin_range_eq_top: the sharp form — L = K(√d₁, …, √dₙ) for a square-class independent family, and consequently [L : K] = 2ⁿ.

theorem TauCeti.Multiquadratic.exists_sq_mem_range_apply_eq_neg_of_notMem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [NeZero 2] (hexp : Monoid.exponent Gal(L/K) ∣ 2) {N : Subgroup Gal(L/K)} {σ : Gal(L/K)} (hσ : σ ∉ N) : ∃ (x : L) (a : K), x ≠ 0 ∧ x ^ 2 = (algebraMap K L) a ∧ (∀ τ ∈ N, τ x = x) ∧ σ x = -x

A subgroup of an exponent-two finite Galois group avoiding σ fixes a nonzero square root of an element of the base field that σ negates.

theorem TauCeti.Multiquadratic.adjoin_setOf_sq_mem_range_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [NeZero 2] (hexp : Monoid.exponent Gal(L/K) ∣ 2) : IntermediateField.adjoin K {x : L | ∃ (a : K), x ^ 2 = (algebraMap K L) a} = ⊤

An exponent-two Galois extension is generated by square roots. If 2 ≠ 0 in K and L / K is a finite Galois extension whose Galois group has exponent dividing two, then L is generated over K by the elements whose square lies in K.

theorem TauCeti.Multiquadratic.exists_finset_sq_mem_range_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [NeZero 2] (hexp : Monoid.exponent Gal(L/K) ∣ 2) : ∃ (s : Finset L), (∀ x ∈ s, ∃ (a : K), x ^ 2 = (algebraMap K L) a) ∧ IntermediateField.adjoin K ↑s = ⊤

Finitely many square roots already generate. The generating set of adjoin_setOf_sq_mem_range_eq_top can be taken finite, because L / K is finite: a primitive element already lies in the subfield generated by finitely many square roots.

theorem TauCeti.Multiquadratic.exists_root_adjoin_eq_adjoin {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [NeZero 2] (s : Finset L) (hssq : ∀ x ∈ s, ∃ (a : K), x ^ 2 = (algebraMap K L) a) : ∃ (n : ℕ) (d : Fin n → K) (root : Fin n → L), (∀ (i : Fin n), root i ∈ s) ∧ (∀ (i : Fin n), root i ^ 2 = (algebraMap K L) (d i)) ∧ (∀ (S : Finset (Fin n)), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)) ∧ IntermediateField.adjoin K (Set.range root) = IntermediateField.adjoin K ↑s ∧ Module.finrank K ↥(IntermediateField.adjoin K ↑s) = 2 ^ n

A finite set of square roots contains an independent generating family. If every member of s squares into K, one can select roots from s whose radicands are square-class independent and which generate the same intermediate field. Its degree is therefore a power of two.

theorem TauCeti.Multiquadratic.exists_root_adjoin_range_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [NeZero 2] (hexp : Monoid.exponent Gal(L/K) ∣ 2) : ∃ (n : ℕ) (d : Fin n → K) (root : Fin n → L), (∀ (i : Fin n), root i ^ 2 = (algebraMap K L) (d i)) ∧ (∀ (S : Finset (Fin n)), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)) ∧ IntermediateField.adjoin K (Set.range root) = ⊤ ∧ Module.finrank K L = 2 ^ n

The converse of the multiquadratic degree theorem. Let 2 ≠ 0 in K and let L / K be a finite Galois extension whose Galois group has exponent dividing two. Then L = K(√d₁, …, √dₙ) for radicands d₁, …, dₙ ∈ K that are square-class independent — no nonempty subset product is a square — and consequently [L : K] = 2ⁿ.