The circulant Gram matrix of a supplied normal basis

theorem MIPRE.SAT.instFactPrimeOfNatNat_mIPRE_3 : Fact (Nat.Prime 2)

noncomputable def MIPRE.SAT.shoupFrobeniusCycle (k : ℕ) (hk : 1 ≤ k) [NeZero k] : Multiplicative (Fin k) →* Gal((shoupBinField k hk).carrier/ZMod 2)

The cyclic Frobenius action with exactly the degree as its index modulus.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.SAT.shoupFrobeniusCycle_apply (k : ℕ) (hk : 1 ≤ k) [NeZero k] (i : Fin k) (a : (shoupBinField k hk).carrier) : ((shoupFrobeniusCycle k hk) (Multiplicative.ofAdd i)) a = a ^ 2 ^ ↑i

The finite cyclic action agrees with the Frobenius powers used in normality.

theorem MIPRE.SAT.shoupTraceGram_normal_circulant (k : ℕ) (hk : 1 ≤ k) [NeZero k] (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (hb : LowDegree.IsNormalBasis b) : shoupTraceGram k hk ⇑b = Matrix.circulant fun (i : Fin k) => shoupTraceGram k hk (⇑b) i 0

A normal basis's Gram matrix is the circulant determined by its first column.

noncomputable def MIPRE.SAT.shoupNormalGramElement (k : ℕ) (hk : 1 ≤ k) [NeZero k] (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) : AddMonoidAlgebra (ZMod 2) (Fin k)

The normal Gram matrix is a concretely identified group-algebra matrix.

Equations

• MIPRE.SAT.shoupNormalGramElement k hk b = MIPRE.LowDegree.BinaryLinear.finGroupOfVector fun (i : Fin k) => MIPRE.SAT.shoupTraceGram k hk (⇑b) i 0

theorem MIPRE.SAT.shoupNormalGramElement_matrix (k : ℕ) (hk : 1 ≤ k) [NeZero k] (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (hb : LowDegree.IsNormalBasis b) : LowDegree.BinaryLinear.groupMatrix (shoupNormalGramElement k hk b) = shoupTraceGram k hk ⇑b

theorem MIPRE.SAT.shoupNormalGram_selfDualize (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (b : Module.Basis (Fin k) (ZMod 2) (shoupBinField k hk).carrier) (hb : LowDegree.IsNormalBasis b) : (LowDegree.BinaryLinear.inverseRootMatrix (shoupTraceGram k hk ⇑b)).transpose * shoupTraceGram k hk ⇑b * LowDegree.BinaryLinear.inverseRootMatrix (shoupTraceGram k hk ⇑b) = 1

The doubled-index inverse square root gives the required Gram identity for any normal basis.