Galois groups from prime-discriminant radicands

The genus-field layer of the multiquadratic roadmap uses prime discriminants D but adjoins square roots of the associated squarefree radicands primeDiscriminantRadicand D: -1, 2, -2, or an odd prime discriminant itself. The field-generic Galois-group theorem TauCeti.Multiquadratic.galoisGroupEquiv already identifies the Galois group of a square-class-independent multiquadratic field with (ℤ/2)ⁿ. This file packages the prime-discriminant instance, using TauCeti.Multiquadratic.not_isSquare_prod_primeDiscriminantRadicands for the independence hypothesis.

Main results

• TauCeti.Multiquadratic.galoisGroupEquivPrimeDiscriminantRadicands: for an injective family of prime discriminants not containing all three even prime discriminants, the Galois group of the field generated by roots of their radicands is Multiplicative (ι → ZMod 2).
• TauCeti.Multiquadratic.card_aut_adjoin_roots_primeDiscriminantRadicands: the corresponding cardinality statement.

noncomputable def TauCeti.Multiquadratic.galoisGroupEquivPrimeDiscriminantRadicands {ι : Type u_1} [Finite ι] {L : Type u_2} [Field L] [Algebra ℚ L] (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ¬((∃ (i : ι), D i = -4) ∧ (∃ (i : ι), D i = 8) ∧ ∃ (i : ι), D i = -8)) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) : Gal(↥(IntermediateField.adjoin ℚ (Set.range root))/ℚ) ≃* Multiplicative (ι → ZMod 2)

The Galois group from prime-discriminant radicands is (ℤ/2)ⁿ. For an injective family of prime discriminants D : ι → ℤ which does not contain all three even prime discriminants -4, 8, and -8, and chosen roots of their squarefree radicands, the Galois group of the generated multiquadratic field is Multiplicative (ι → ZMod 2). This is the prime-discriminant instance of the field-generic galoisGroupEquiv.

@[simp]

theorem TauCeti.Multiquadratic.galoisGroupEquivPrimeDiscriminantRadicands_apply {ι : Type u_1} [Finite ι] {L : Type u_2} [Field L] [Algebra ℚ L] (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ¬((∃ (i : ι), D i = -4) ∧ (∃ (i : ι), D i = 8) ∧ ∃ (i : ι), D i = -8)) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) (σ : Gal(↥(IntermediateField.adjoin ℚ (Set.range root))/ℚ)) : (galoisGroupEquivPrimeDiscriminantRadicands D hD hinj heven root hroot) σ = Multiplicative.ofAdd (signPattern root σ)

The prime-discriminant Galois equivalence sends an automorphism to its sign pattern on the chosen radicand roots.

@[simp]

theorem TauCeti.Multiquadratic.galoisGroupEquivPrimeDiscriminantRadicands_symm_apply_gen {ι : Type u_1} [Finite ι] {L : Type u_2} [Field L] [Algebra ℚ L] (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ¬((∃ (i : ι), D i = -4) ∧ (∃ (i : ι), D i = 8) ∧ ∃ (i : ι), D i = -8)) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) (ε : ι → ZMod 2) (i : ι) : ((galoisGroupEquivPrimeDiscriminantRadicands D hD hinj heven root hroot).symm (Multiplicative.ofAdd ε)) (gen root i) = (-1) ^ (ε i).val * gen root i

The inverse prime-discriminant Galois equivalence realizes a sign pattern by sending each chosen generator to (-1)^(ε i) times that generator.

theorem TauCeti.Multiquadratic.card_aut_adjoin_roots_primeDiscriminantRadicands {ι : Type u_1} [Finite ι] {L : Type u_2} [Field L] [Algebra ℚ L] (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ¬((∃ (i : ι), D i = -4) ∧ (∃ (i : ι), D i = 8) ∧ ∃ (i : ι), D i = -8)) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) : Nat.card Gal(↥(IntermediateField.adjoin ℚ (Set.range root))/ℚ) = 2 ^ Nat.card ι

Cardinality of the Galois group from prime-discriminant radicands. Under the same prime-discriminant hypotheses, |Gal(ℚ(rootᵢ : i)/ℚ)| = 2^|ι|.