Self-dualization in characteristic two #

The step that turns a normal basis into a self-dual normal basis (blueprint lem:self-dual-basis, ledger nodes 1.1.6.1.7 and 1.1.6.1.8).

Written in the group algebra, where the whole step is two short lemmas. If α is a normal element of K / F with Galois group G, the Gram matrix of its orbit is circulant, i.e. it is the element c ∈ F[G] with c g = tr(α · g α); it is a unit, and it is fixed by the involution τ induced by g ↦ g⁻¹. Replacing α by a • α replaces c by a · τ a · c, so a self-dual normal basis is exactly a solution a of a · τ a = c⁻¹.

exists_mul_involute_eq — that equation is solvable in any commutative ring on which squaring is bijective: take the square root of the right-hand side, which is unique and therefore fixed by τ because the right-hand side is.
sq_bijective — and squaring is bijective on F[G] when F is a finite field of characteristic two and G is a finite abelian group of odd order, because squaring is then the composite of the Frobenius of F on coefficients with the doubling bijection of G on indices.

Between them they replace the circulant Gram manipulation the campaign's two nodes carry. Nothing here is about fields yet: MIPRE/Foundations/LowDegree/SelfDual.lean has the definitions IsSelfDualBasis and IsNormalBasis, and assembling these lemmas into a basis is the remaining work of issue #105.

The equation `a · τ a = u` #

source

theorem MIPRE.LowDegree.exists_mul_involute_eq {R : Type u_1} [CommRing R] (τ : R ≃+* R) (hinj : ∀ (x y : R), x * x = y * y → x = y) (hsurj : ∀ (y : R), ∃ (x : R), x * x = y) {u : R} (hu : τ u = u) :

∃ (a : R), a * τ a = u

Self-dualization, abstractly. In a commutative ring on which squaring is bijective, every element fixed by a ring involution is of the form a · τ a. The square root of u is unique, and τ of it is another square root, so it is fixed by τ as well.

Squaring on a group algebra of odd order in characteristic two #

source

theorem MIPRE.LowDegree.add_self_injective {G : Type u_1} [AddCommGroup G] [Fintype G] (hG : Odd (Fintype.card G)) :

Function.Injective fun (g : G) => g + g

In a finite abelian group of odd order, doubling is injective.

source

theorem MIPRE.LowDegree.add_self_bijective {G : Type u_1} [AddCommGroup G] [Fintype G] (hG : Odd (Fintype.card G)) :

Function.Bijective fun (g : G) => g + g

In a finite abelian group of odd order, doubling is bijective.

source

theorem MIPRE.LowDegree.two_eq_zero {G : Type u_1} [AddCommGroup G] {F : Type u_2} [Field F] (hF : CharP F 2) :

2 = 0

source

theorem MIPRE.LowDegree.add_mul_self_char_two {R : Type u_3} [CommRing R] (h2 : 2 = 0) (x y : R) :

(x + y) * (x + y) = x * x + y * y

In characteristic two, squaring is additive.

source

theorem MIPRE.LowDegree.coeff_mul_self {G : Type u_1} [AddCommGroup G] [Fintype G] {F : Type u_2} [Field F] [DecidableEq G] (hF : CharP F 2) (hG : Odd (Fintype.card G)) (z : AddMonoidAlgebra F G) (g : G) :

(z * z).coeff (g + g) = z.coeff g * z.coeff g

The coefficient of a square, at a doubled index: squaring F[G] is the Frobenius of F on coefficients composed with doubling on indices.

source

theorem MIPRE.LowDegree.mul_self_bijective {G : Type u_1} [AddCommGroup G] [Fintype G] {F : Type u_2} [Field F] [Fintype F] [DecidableEq G] (hF : CharP F 2) (hG : Odd (Fintype.card G)) :

Function.Bijective fun (x : AddMonoidAlgebra F G) => x * x

Squaring is bijective on F[G] when F has characteristic two and G is a finite abelian group of odd order.

source

theorem MIPRE.LowDegree.exists_mul_involute_eq_of_charTwo {G : Type u_1} [AddCommGroup G] [Fintype G] {F : Type u_2} [Field F] [Fintype F] [DecidableEq G] (hF : CharP F 2) (hG : Odd (Fintype.card G)) (τ : AddMonoidAlgebra F G ≃+* AddMonoidAlgebra F G) {u : AddMonoidAlgebra F G} (hu : τ u = u) :

∃ (a : AddMonoidAlgebra F G), a * τ a = u

Self-dualization in the group algebra: if F has characteristic two and G is a finite abelian group of odd order, every element of F[G] fixed by a ring involution τ is of the form a · τ a.

An explicit square root over the binary field #

source

noncomputable def MIPRE.LowDegree.binarySquareRoot {G : Type u_1} [AddCommGroup G] [Fintype G] (z : AddMonoidAlgebra (ZMod 2) G) :

AddMonoidAlgebra (ZMod 2) G

Square root in a binary group algebra: the coefficient at g is read from g + g. For an odd-order group this is a permutation of the coefficient vector. In particular, this step needs neither factorization nor exponentiation in the group of units.

Equations