The relative Galois group 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) an abelian Galois extension of K with group (ℤ/2)ⁿ, and
TauCeti.NumberTheory.Multiquadratic.Subfield.Lattice matches each intermediate field F of
M / K with the 𝔽₂-subspace U of ι → ℤ/2 consisting of the sign patterns of the
automorphisms that fix F. TauCeti.NumberTheory.Multiquadratic.RelativeDegree records the
relative degree [M : F] = 2 ^ dim U; this file records the relative group.
Two things happen. First, a relative automorphism restricts to a K-automorphism, and those are
involutions, so Gal(M/F) has exponent dividing two; commutativity comes for free, since Mathlib's
tower instances for IsAbelianGalois already make both halves of the tower abelian Galois once
TauCeti.Multiquadratic.isAbelianGalois supplies IsAbelianGalois K M. So Gal(M/F) is again
elementary abelian, exactly as Gal(M/K) is.
Second, the sign pattern identifies Gal(M/F) precisely: restriction of scalars embeds it into
Gal(M/K) ≃ (ℤ/2)ⁿ, its image is exactly the subspace U attached to F, and the resulting map
Gal(M/F) ≃* Multiplicative U
is an isomorphism. Nothing is proved bijective by hand for this: it is Mathlib's
IntermediateField.fixingSubgroupEquiv composed with the restriction of
TauCeti.Multiquadratic.galoisGroupEquiv to the fixing subgroup of F, whose image the subfield
dictionary already identifies with U. Cardinalities then come from
IsGalois.card_aut_eq_finrank together with the relative degrees of
TauCeti.NumberTheory.Multiquadratic.RelativeDegree: |Gal(M/F)| = 2 ^ dim U in general, and
|Gal(M/F)| = 2 ^ (n - 1) over a quadratic subfield, the reading the genus-field constructions
consume.
This is the group-theoretic half of the relative picture the genus-field constructions consume: the
genus field is multiquadratic over ℚ, and the group the genus theory identifies with Cl/Cl² is
its Galois group over the quadratic base ℚ(√d), a relative group of exactly this shape.
Main results #
TauCeti.Multiquadratic.aut_top_over_intermediateField_mul_self_eq_one: every relative automorphism is an involution.TauCeti.Multiquadratic.aut_top_over_intermediateField_exponent_dvd_two:Gal(M/F)has exponent dividing two.TauCeti.Multiquadratic.galoisGroupEquivIntermediateFieldSubmodule: the isomorphismGal(M/F) ≃* Multiplicative Ugiven by the sign pattern of the restricted automorphism.TauCeti.Multiquadratic.card_aut_top_over_intermediateField:|Gal(M/F)| = 2 ^ dim U.TauCeti.Multiquadratic.card_aut_top_over_intermediateField_of_finrank_eq_two: over a quadratic subfield,|Gal(M/F)| = 2 ^ (n - 1).
Provenance #
The multiquadratic Galois group and the subfield/subspace dictionary refined here are migrated,
with the rest of 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 relative reading
assembles that dictionary with Mathlib's Galois correspondence
(IntermediateField.fixingSubgroupEquiv) and its abelian-extension tower instances
(IsAbelianGalois.tower_top).
Relative automorphisms of a multiquadratic field are involutions. An F-automorphism of
M = K(rootᵢ : i) restricts to a K-automorphism, and those square to the identity
(TauCeti.Multiquadratic.aut_mul_self_eq_one).
The relative Galois group has exponent dividing two. As stated this needs no finiteness or
characteristic hypothesis, just as TauCeti.Multiquadratic.aut_exponent_dvd_two does not for
Gal(M/K). Under the extra hypotheses [Finite ι] and [NeZero (2 : K)] of
TauCeti.Multiquadratic.isAbelianGalois, Mathlib's IsAbelianGalois.tower_top supplies
commutativity as well, and then this says Gal(M/F) is elementary abelian, exactly as Gal(M/K)
is.
The sign pattern of a relative automorphism lies in the 𝔽₂-subspace attached to the base
field: by definition that subspace collects the sign patterns of the automorphisms fixing F.
The relative Galois group of a multiquadratic field is the subspace attached to its base.
Under square-class independence, restricting an F-automorphism of M = K(rootᵢ : i) to K and
reading its sign pattern is an isomorphism of Gal(M/F) onto the 𝔽₂-subspace U of ι → ℤ/2
that the subfield dictionary attaches to F. For F = ⊥ the subspace is everything and this is
TauCeti.Multiquadratic.galoisGroupEquiv.
No bijection is proved here: this is the composite of Mathlib's
IntermediateField.fixingSubgroupEquiv, which inverts restriction of scalars, with the restriction
of TauCeti.Multiquadratic.galoisGroupEquiv to the fixing subgroup of F, whose image is U by
TauCeti.Multiquadratic.intermediateFieldEquivSubmodule_apply_ofDual.
Instances For
The relative Galois equivalence sends an automorphism to the sign pattern of its restriction.
The inverse of the relative Galois equivalence realizes a sign pattern v in the subspace
attached to F as the F-automorphism sending each generator rootᵢ to (-1)^(vᵢ) · rootᵢ. This
is the relative reading of TauCeti.Multiquadratic.galoisGroupEquiv_symm_apply_gen.
The order of the relative Galois group of a multiquadratic field. Under square-class
independence, the relative Galois group Gal(M/F) of M = K(rootᵢ : i) over an intermediate field
F has order 2 ^ dim U, where U is the 𝔽₂-subspace of ι → ℤ/2 attached to F. This is the
cardinality reading of TauCeti.Multiquadratic.galoisGroupEquivIntermediateFieldSubmodule, taken
here from the relative degree TauCeti.Multiquadratic.finrank_top_over_intermediateField, and it
is to the relative group what TauCeti.Multiquadratic.card_aut_adjoin_range is to the absolute
one.
The relative Galois group over a quadratic subfield has order 2 ^ (n - 1). Under
square-class independence, over any quadratic subfield F of the degree-2ⁿ multiquadratic field
M = K(rootᵢ : i), the relative Galois group Gal(M/F) is elementary abelian of order
2 ^ (|ι| - 1): a quadratic subfield is a hyperplane, so its subspace is a line's worth short of
everything. This is the group the genus-field constructions read off over the quadratic base.