The Galois group of a multiquadratic field is (ℤ/2)ⁿ

Over a field K in which 2 ≠ 0, a multiquadratic field M = K(rootᵢ : i) (with rootᵢ ^ 2 = dᵢ ∈ K) is Galois (TauCeti.NumberTheory.Multiquadratic.Galois.Basic). Each automorphism sends every generator to ± rootᵢ, so it is determined by a sign pattern ι → ℤ/2; this assignment is an injective group homomorphism. When the radicands are square-class independent the degree is 2ⁿ (TauCeti.NumberTheory.Multiquadratic.Degree), so counting forces the homomorphism to be an isomorphism: Gal(M/K) ≃ (ℤ/2)ⁿ.

Main results

• TauCeti.Multiquadratic.signHom: the injective sign-pattern homomorphism Gal(M/K) →* (ℤ/2)ⁿ.
• TauCeti.Multiquadratic.galoisGroupEquiv: for square-class independent radicands, the explicit isomorphism Gal(M/K) ≃* Multiplicative (ι → ℤ/2).
• TauCeti.Multiquadratic.aut_nontrivial: under square-class independence over a nonempty index type, Gal(M/K) is nontrivial.
• TauCeti.Multiquadratic.card_aut_adjoin_range: the cardinality reading |Gal(M/K)| = 2^|ι| of that isomorphism.
• TauCeti.Multiquadratic.nonempty_mulEquiv_gal_definingPolynomial: the same group read as the Galois group Polynomial.Gal of the defining polynomial ∏ᵢ (X² - dᵢ).

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 the sign-change automorphisms of one concrete multiquadratic field were analysed; here the construction is carried out for an arbitrary such tower.

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

The sign pattern of an automorphism: 0 where it fixes a generator and 1 otherwise. When gen root i ≠ -gen root i, the 1 case says that the automorphism negates the generator.

Equations

• TauCeti.Multiquadratic.signPattern root σ i = if σ (TauCeti.Multiquadratic.gen root i) = TauCeti.Multiquadratic.gen root i then 0 else 1

theorem TauCeti.Multiquadratic.aut_gen_eq_signPattern {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) = (-1) ^ (signPattern root σ i).val * gen root i

An automorphism acts on each generator by the corresponding sign.

theorem TauCeti.Multiquadratic.signPattern_eq_ite_of_zsmul_gen {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)) (σ : Gal(↥(IntermediateField.adjoin K (Set.range root))/K)) {i : ι} {ε : ℤ} (hε : ε = 1 ∨ ε = -1) (hd : d i ≠ 0) (hσ : σ (gen root i) = ε • gen root i) : signPattern root σ i = if ε = 1 then 0 else 1

Read the sign pattern off a generator-wise sign. If σ (gen root i) = ε • gen root i with ε = ±1 (in ℤ) and d i ≠ 0, then signPattern root σ i is 0 when ε = 1 and 1 when ε = -1. This bridges a generator-wise sign — for instance a Frobenius acting on √dᵢ by a Legendre symbol (NumberField.isArithFrobAt_apply_sqrt) — to the (ℤ/2)ⁿ identification, so it composes with TauCeti.Multiquadratic.galoisGroupEquiv_apply.

theorem TauCeti.Multiquadratic.signPattern_injective {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)) : Function.Injective (signPattern root)

Two automorphisms with the same sign pattern are equal.

theorem TauCeti.Multiquadratic.signPattern_eq_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {root : ι → L} (σ : Gal(↥(IntermediateField.adjoin K (Set.range root))/K)) (i : ι) (h : σ (gen root i) = gen root i) : signPattern root σ i = 0

The sign is 0 exactly where the automorphism fixes the generator.

@[simp]

theorem TauCeti.Multiquadratic.signPattern_eq_zero_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {root : ι → L} (σ : Gal(↥(IntermediateField.adjoin K (Set.range root))/K)) (i : ι) : signPattern root σ i = 0 ↔ σ (gen root i) = gen root i

The sign is 0 iff the automorphism fixes the generator.

theorem TauCeti.Multiquadratic.signPattern_eq_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {root : ι → L} (σ : Gal(↥(IntermediateField.adjoin K (Set.range root))/K)) (i : ι) (hne : gen root i ≠ -gen root i) (h : σ (gen root i) = -gen root i) : signPattern root σ i = 1

The sign is 1 where the automorphism negates a generator that differs from its negation.

@[simp]

theorem TauCeti.Multiquadratic.signPattern_eq_one_iff {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 : ι) (hne : gen root i ≠ -gen root i) : signPattern root σ i = 1 ↔ σ (gen root i) = -gen root i

The sign is 1 iff the automorphism negates a generator that differs from its negation.

@[simp]

theorem TauCeti.Multiquadratic.signPattern_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {ι : Type u_3} {root : ι → L} : signPattern root 1 = 0

The identity automorphism has the zero sign pattern.

theorem TauCeti.Multiquadratic.signPattern_mul_apply {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 : ι) : signPattern root (σ * τ) i = signPattern root σ i + signPattern root τ i

Pointwise composition rule for sign patterns.

@[simp]

theorem TauCeti.Multiquadratic.signPattern_mul {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)) : signPattern root (σ * τ) = signPattern root σ + signPattern root τ

The sign pattern is additive: it is a group homomorphism to ι → ℤ/2.

noncomputable def TauCeti.Multiquadratic.signHom {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) →* Multiplicative (ι → ZMod 2)

The Galois group of M / K maps to the sign patterns (ℤ/2)ⁱ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Multiquadratic.signHom_apply {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)) : (signHom root hroot) σ = Multiplicative.ofAdd (signPattern root σ)

Evaluation rule for signHom: it is the multiplicative form of signPattern.

theorem TauCeti.Multiquadratic.signHom_injective {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)) : Function.Injective ⇑(signHom root hroot)

The sign-pattern homomorphism is injective.

noncomputable def TauCeti.Multiquadratic.galoisGroupEquiv {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)) : Gal(↥(IntermediateField.adjoin K (Set.range root))/K) ≃* Multiplicative (ι → ZMod 2)

For square-class independent radicands, the Galois group of a multiquadratic field is (ℤ/2)ⁿ.

Equations

• TauCeti.Multiquadratic.galoisGroupEquiv hroot hindep = MulEquiv.ofBijective (TauCeti.Multiquadratic.signHom root hroot) ⋯

theorem TauCeti.Multiquadratic.aut_nontrivial {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] [Nonempty ι] (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap K L) (d i)) (hindep : ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)) : Nontrivial Gal(↥(IntermediateField.adjoin K (Set.range root))/K)

A multiquadratic field over a nonempty family of independent radicands has a nontrivial Galois group.

@[simp]

theorem TauCeti.Multiquadratic.galoisGroupEquiv_apply {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)) (σ : Gal(↥(IntermediateField.adjoin K (Set.range root))/K)) : (galoisGroupEquiv hroot hindep) σ = Multiplicative.ofAdd (signPattern root σ)

The Galois-group equivalence sends an automorphism to its multiplicative sign pattern.

@[simp]

theorem TauCeti.Multiquadratic.galoisGroupEquiv_symm_apply_gen {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)) (ε : ι → ZMod 2) (i : ι) : ((galoisGroupEquiv hroot hindep).symm (Multiplicative.ofAdd ε)) (gen root i) = (-1) ^ (ε i).val * gen root i

The inverse of galoisGroupEquiv realizes a sign pattern ε as the automorphism sending each generator rootᵢ to (-1)^(εᵢ) · rootᵢ.

theorem TauCeti.Multiquadratic.card_aut_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 Gal(↥(IntermediateField.adjoin K (Set.range root))/K) = 2 ^ Nat.card ι

Cardinality of the Galois group of a multiquadratic field. If no nonempty subset product of the radicands d i is a square in K (and 2 ≠ 0 in K), then the multiquadratic field M = K(rootᵢ : i) has |Gal(M/K)| = 2^|ι|. This is the cardinality reading of the explicit isomorphism galoisGroupEquiv.

theorem TauCeti.Multiquadratic.nonempty_mulEquiv_gal_definingPolynomial {K : Type u_1} [Field K] {ι : Type u_3} {d : ι → K} [Finite ι] [NeZero 2] (hindep : ∀ (S : Finset ι), S.Nonempty → ¬IsSquare (∏ i ∈ S, d i)) : Nonempty ((definingPolynomial d).Gal ≃* Multiplicative (ι → ZMod 2))

For square-class independent radicands, ∏ᵢ (X² - dᵢ) has Galois group (ℤ/2)ⁿ. The splitting field of the defining polynomial contains a square root of every radicand, and it is the multiquadratic field they generate, so galoisGroupEquiv applies to it. The isomorphism depends on the choice of those square roots, which is why only its existence is stated.