The faithful cyclic Frobenius representation

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

noncomputable def MIPRE.SAT.shoupFrobeniusAction (k : ℕ) (hk : 1 ≤ k) [NeZero k] : AddMonoidAlgebra (ZMod 2) (Fin k) →ₐ[ZMod 2] Module.End (ZMod 2) (shoupBinField k hk).carrier

A group-algebra coefficient vector acts as the corresponding linearized polynomial.

Equations

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

theorem MIPRE.SAT.shoupFrobeniusAction_eq_sum (k : ℕ) (hk : 1 ≤ k) [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) : (shoupFrobeniusAction k hk) z = ∑ i : Fin k, z.coeff i • ((shoupFrobeniusCycle k hk) (Multiplicative.ofAdd i)).toLinearMap

theorem MIPRE.SAT.shoupFrobeniusAction_apply (k : ℕ) (hk : 1 ≤ k) [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (a : (shoupBinField k hk).carrier) : ((shoupFrobeniusAction k hk) z) a = ∑ i : Fin k, z.coeff i • a ^ 2 ^ ↑i

theorem MIPRE.SAT.shoupFrobeniusCycle_injective (k : ℕ) (hk : 1 ≤ k) [NeZero k] : Function.Injective fun (i : Fin k) => (shoupFrobeniusCycle k hk) (Multiplicative.ofAdd i)

theorem MIPRE.SAT.shoupFrobeniusAction_injective (k : ℕ) (hk : 1 ≤ k) [NeZero k] : Function.Injective ⇑(shoupFrobeniusAction k hk)

Faithfulness follows from independence of the distinct Frobenius automorphisms.

theorem MIPRE.SAT.shoupFrobeniusAction_exists_basis_image (k : ℕ) (hk : 1 ≤ k) [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (hz : z ≠ 0) : ∃ (j : Fin k), ((shoupFrobeniusAction k hk) z) ((shoupPowerBasis k hk) j) ≠ 0

A nonzero cyclic operator has a nonzero image among the polynomial-basis vectors.