A self-dual normal basis exists in characteristic two and odd degree #
This is the existence half of blueprint lem:self-dual-basis: over a finite field of
characteristic two, an extension of odd degree admits a basis that is simultaneously normal
(a Frobenius orbit) and self-dual for the trace form.
The argument is the short one. Fix the normal element α Mathlib's normal basis theorem
supplies and let c ∈ F[G], G = Gal(K/F), be its Gram element, with c_g = tr(α · gα).
Writing ofAlg a for the element with normal-basis coordinates a, the Gram element
transforms as
gramPair (ofAlg a) (ofAlg a) = a · τa · c,
where τ is the involution induced by g ↦ g⁻¹ (gramPair_ofAlg). Nondegeneracy of the
trace form makes c a unit (isUnit_gram), and c is τ-fixed, hence so is c⁻¹. Since
|G| = [K : F] is odd and the characteristic is two, squaring is bijective on F[G]
(mul_self_bijective'), so exists_mul_involute_eq of
MIPRE.Foundations.LowDegree.SelfDualize produces a with a · τa = c⁻¹. Then
β = ofAlg a has Gram element 1, i.e. its Frobenius orbit is orthonormal.
What is not here is the poly(k) algorithm that produces such a basis; the blueprint's
lem:self-dual-basis still waits on that half.
Squaring on a group algebra, multiplicatively #
In a finite abelian group of odd order, squaring is injective.
The coefficient of a square, at a squared index.
Squaring is bijective on F[G], multiplicatively.
The Gram element of a Frobenius orbit #
The normal element Mathlib's normal basis theorem supplies.
Equations
- MIPRE.LowDegree.normalElt F K = (IsGalois.normalBasis F K) 1
Instances For
The involution of the group algebra induced by g ↦ g⁻¹.
Equations
- MIPRE.LowDegree.galStar F K = (MonoidAlgebra.domCongr F F (MulEquiv.inv Gal(K/F))).toRingEquiv
Instances For
The Gram element of a pair: its coefficient at g is tr(x · g y). For x = y the
Gram matrix of the Frobenius orbit of x is the circulant this determines.
Equations
- MIPRE.LowDegree.gramPair F K x y = MonoidAlgebra.ofCoeff (Finsupp.equivFunOnFinite.symm fun (g : Gal(K/F)) => (Algebra.trace F K) (x * g y))
Instances For
The element of K with normal-basis coordinates a.
Equations
- MIPRE.LowDegree.ofAlg F K a = (IsGalois.normalBasis F K).repr.symm a.coeff
Instances For
The trace is invariant under the Galois action.
The trace pairing of two members of one Frobenius orbit depends only on their ratio.
The Gram element transforms by a ↦ a · τa · c. This is the identity the whole
self-dualization rests on: the Gram matrix of the orbit of ofAlg a is the circulant of
a · τ a · c, where c is the Gram element of the normal element itself.
The Gram element is a unit #
The Gram element of an orbit is fixed by the involution: the Gram matrix is symmetric.
The Gram element of a normal element is a unit: the Gram matrix of a basis under the nondegenerate trace form is invertible.
A self-dual normal element, and the basis #
A self-dual normal element. In characteristic two and odd degree there is a β whose
Frobenius orbit is orthonormal for the trace form. This is exists_mul_involute_eq applied to
the inverse of the Gram element, which is fixed by the involution because the Gram element is
and inverses are unique.
The Frobenius orbit of a self-dual normal element is orthonormal: the diagonal.
The Frobenius orbit of a self-dual normal element is orthonormal: off the diagonal.
A self-dual normal basis exists when the characteristic is two and the degree is odd
(the existence half of blueprint lem:self-dual-basis).
A self-dual normal basis of 𝔽_{2^k} over 𝔽₂ exists for every odd k --- the
existence half of blueprint lem:self-dual-basis, on Mathlib's normal basis theorem and the
self-dualization of lem:group-algebra-selfdualization.