A multiquadratic field is Galois

For square roots root i of radicands d i ∈ K, the multiquadratic field M = K(rootᵢ : i) is the splitting field of ∏ᵢ (X² - dᵢ), hence normal; when 2 ≠ 0 in K each generator is separable, so M / K is Galois. Along the way we record the basic structure shared by the later group-theoretic analysis: every K-automorphism sends each generator to another element with the same square, so it is an involution and the automorphism group is abelian.

The explicit identification of the group with (ℤ/2)ⁿ is a separate, later step (TauCeti.NumberTheory.Multiquadratic.Galois.Group).

Main results

• TauCeti.Multiquadratic.isSplittingField: M is the splitting field of ∏ᵢ (X² - dᵢ).
• TauCeti.Multiquadratic.finiteDimensional_adjoin_range: M is finite-dimensional over K.
• TauCeti.Multiquadratic.isGalois: M / K is Galois (when 2 ≠ 0 in K).
• TauCeti.Multiquadratic.isGalois_of_adjoin_eq_top: a field generated by these roots is Galois.
• TauCeti.Multiquadratic.aut_mul_self_eq_one: every σ : M ≃ₐ[K] M satisfies σ * σ = 1.
• TauCeti.Multiquadratic.aut_pow_two_eq_one_of_adjoin_eq_top: the same involution result for a field generated by square roots.
• TauCeti.Multiquadratic.aut_commute: the automorphism group is commutative.
• TauCeti.Multiquadratic.isAbelianGalois: M / K is abelian Galois.

Provenance

Generalised from kim-em/erdos-unit-distance, the formalization of L. Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture, where these facts were established for one concrete CM field.

noncomputable def TauCeti.Multiquadratic.definingPolynomial {K : Type u_1} [Field K] {ι : Type u_3} [Finite ι] (d : ι → K) : Polynomial K

The defining polynomial of the multiquadratic field: ∏ᵢ (X² - dᵢ).

Equations

• TauCeti.Multiquadratic.definingPolynomial d = ∏ i : ι, (Polynomial.X ^ 2 - Polynomial.C (d i))

@[simp]

theorem TauCeti.Multiquadratic.definingPolynomial_def {K : Type u_1} [Field K] {ι : Type u_3} {d : ι → K} [Finite ι] : definingPolynomial d = ∏ i : ι, (Polynomial.X ^ 2 - Polynomial.C (d i))

The defining polynomial is the product of the quadratic factors X² - dᵢ.

noncomputable def TauCeti.Multiquadratic.gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} (root : ι → L) (i : ι) : ↥(IntermediateField.adjoin K (Set.range root))

The i-th generator, as an element of the multiquadratic field M.

Equations

• TauCeti.Multiquadratic.gen root i = ⟨root i, ⋯⟩

@[simp]

theorem TauCeti.Multiquadratic.coe_gen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {root : ι → L} (i : ι) : ↑(gen root i) = root i

Coercing the i-th generator of K(rootᵢ : i) back to L gives root i.

theorem TauCeti.Multiquadratic.adjoin_gen_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {root : ι → L} : IntermediateField.adjoin K (Set.range (gen root)) = ⊤

The generators generate M as its own top field.

@[simp]

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

The generator squares to its radicand (in M).

theorem TauCeti.Multiquadratic.aut_gen_eq_self_or_eq_neg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {d : ι → K} {root : ι → L} (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) (σ : Gal(↥(IntermediateField.adjoin K (Set.range root))/K)) (i : ι) : σ (gen root i) = gen root i ∨ σ (gen root i) = -gen root i

Every automorphism sends a generator to itself or to its negation.

theorem TauCeti.Multiquadratic.gen_ne_neg {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)) (i : ι) (hd : d i ≠ 0) : gen root i ≠ -gen root i

A generator is not equal to its own negation when the radicand is nonzero, since 2 ≠ 0 in L.

theorem TauCeti.Multiquadratic.isSplittingField {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)) : Polynomial.IsSplittingField K (↥(IntermediateField.adjoin K (Set.range root))) (definingPolynomial d)

M = K(rootᵢ : i) is the splitting field of ∏ᵢ (X² - dᵢ) over K.

theorem TauCeti.Multiquadratic.finiteDimensional_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 ι] (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) : FiniteDimensional K ↥(IntermediateField.adjoin K (Set.range root))

A multiquadratic field is finite-dimensional over K: it is the splitting field of ∏ᵢ (X² - dᵢ), a polynomial over K.

theorem TauCeti.Multiquadratic.isGalois {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)) : IsGalois K ↥(IntermediateField.adjoin K (Set.range root))

A multiquadratic field over a field in which 2 ≠ 0 is Galois: it is the splitting field of ∏ᵢ (X² - dᵢ) (hence normal), and each generator satisfies a separable quadratic.

theorem TauCeti.Multiquadratic.isGalois_of_adjoin_eq_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)) (htop : IntermediateField.adjoin K (Set.range root) = ⊤) : IsGalois K L

A field generated over K by finitely many square roots is Galois over K.

@[simp]

theorem TauCeti.Multiquadratic.aut_mul_self_eq_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {d : ι → K} {root : ι → L} (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) (σ : Gal(↥(IntermediateField.adjoin K (Set.range root))/K)) : σ * σ = 1

Every K-automorphism of the multiquadratic field K(rootᵢ : i) is an involution: fixing K forces the image of each generator to have the same square as the generator, so applying the automorphism twice fixes the generators.

theorem TauCeti.Multiquadratic.aut_pow_two_eq_one_of_adjoin_eq_top {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {d : ι → K} {root : ι → L} (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) (htop : IntermediateField.adjoin K (Set.range root) = ⊤) (σ : Gal(L/K)) : σ ^ 2 = 1

Every automorphism of a field generated by square roots has square equal to one.

theorem TauCeti.Multiquadratic.aut_commute {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {d : ι → K} {root : ι → L} (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) (a b : Gal(↥(IntermediateField.adjoin K (Set.range root))/K)) : Commute a b

The automorphism group of a multiquadratic field is commutative: every element has order dividing two, so any two commute.

theorem TauCeti.Multiquadratic.isAbelianGalois {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)) : IsAbelianGalois K ↥(IntermediateField.adjoin K (Set.range root))

A finite multiquadratic extension in characteristic different from two is abelian Galois.