Multiquadratic field extensions #
The degree of a multiquadratic extension L(√c₁, …, √cₘ)/L over a field of characteristic ≠ 2
is 2 ^ (m - dim V), where V ≤ 𝔽₂^m is the space of square relations between the radicands,
realized as the kernel of a linear map to Lˣ/(Lˣ)²; descent of squares along such extensions.
Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.
Adjoining a single square root x (with x² ∈ L) to a field L gives degree at most 2.
Adjoining a finite set of square roots (each squaring into L) gives degree at most
2 ^ |s|.
Relative degree is monotone in the top field: [B : A] ≤ [C : A] for A ≤ B ≤ C with C/A
finite-dimensional.
The group Lˣ/(Lˣ)² of nonzero square classes of the field L, written additively so that
it becomes a ZMod 2-module.
Equations
- SquareClasses L = Additive (Lˣ ⧸ (powMonoidHom 2).range)
Instances For
The class of a nonzero field element in Lˣ/(Lˣ)² (junk value 0 at r = 0).
Equations
- sqClass r = if hr : r = 0 then 0 else Additive.ofMul ↑(Units.mk0 r hr)
Instances For
The 𝔽₂-relation submodule of a finite family of radicands r : ι → L: the kernel of
ε ↦ ∑ ε i • [r i] in Lˣ/(Lˣ)². For nonzero radicands, ε is a relation iff
∏_{i : ε i = 1} r i is a square in L (see mem_rootRelations).
Equations
- rootRelations r = (Fintype.linearCombination (ZMod 2) fun (i : ι) => sqClass (r i)).ker
Instances For
Extension by zero from (the coercion of) a finite set s, as a ZMod 2-linear map.
Equations
Instances For
The 𝔽₂-relation submodule of a multiquadratic extension: the extension by zero of the
relation submodule of the family c|_s (see mem_multiquadraticRelations).
Equations
- multiquadraticRelations s c = Submodule.map (extendByZeroLM s) (rootRelations fun (x : ↑↑s) => c ↑x)
Instances For
ε ∈ multiquadraticRelations s c iff ε is supported on s and
∏_{x ∈ s, ε x = 1} c x is a square in L.
One-step square descent: over L(x) with x² = c and x ∉ L, the image of d ∈ L is a
square iff d or d · c is a square in L.
For an intermediate field K of E/L and e : L, the image of e in K is a square
iff some element of K squares to the image of e in E.
If w is a square root of algebraMap e lying outside an intermediate field K, then e
is not a square in K.
An element of the simple extension F(y) with y² ∈ F is exactly an F-linear combination
u + v · y.
Iterated square descent: some element of L(s) squares to d iff d * ∏_{y ∈ t} c y is a
square in L for some subset t ⊆ s.
The relation space of an ι-indexed family has 𝔽₂-dimension at most |ι|.
multiquadraticRelations s c has 𝔽₂-dimension at most |s|.
multiquadraticRelations s c is finite-dimensional over 𝔽₂.
Intersecting V (insert y s') with the hyperplane ε y = 0 recovers V s' (equal
𝔽₂-dimension).
Some relation of V (insert y s') has y-coordinate 1 iff c y is a square in
L(s').
Adjoining y raises dim V by 1 when c y is a square in L(s'), and leaves it
unchanged otherwise.
Degree of a multiquadratic extension: [L(s) : L] = 2 ^ (|s| - dim V), where V is the
𝔽₂-space of square relations among the radicands.
If a multiquadratic family s generates a field of maximal degree 2 ^ |s| and w is a
new square root whose radicand is not a square in L(s), then adjoining w doubles the degree.
Family form of multiquadratic_degree_insert_of_maximal: a maximal multiquadratic family
x of size n (square roots of v) gains a new square root w whose radicand is not a square
in L(range x), doubling the degree.
The dimension of the relation space is invariant under reindexing the family by a bijection.
multiquadraticRelations s c has the same 𝔽₂-dimension as the relation space of the
restricted family c|_s.
Family form of multiquadratic_degree: for an injective family x : ι → E of square roots
of nonzero radicands r : ι → L, the degree of L(x i : i) over L is
2 ^ (|ι| - dim rootRelations r).
If every g ∈ G acts on the radicands through a field automorphism, the relation space is
invariant under the coordinate action.
For a finite 2-group acting pretransitively with automorphism-compatible radicands, a
nonzero relation space contains the all-ones vector.
Such a subfield has exponent 2: every F-automorphism of it is an involution.
A subfield of E generated by square roots of elements of F is Galois over F.