Primitive components of a finite ring with bijective squaring

This supplies the algebraic justification for splitting the binary cyclic group algebra by its fixed vectors. The computations need only multiplication and linear algebra; the finite permutation argument below is a correctness proof, not an enumeration performed by the algorithm.

theorem MIPRE.LowDegree.exists_pow_succ_eq_self_of_square_bijective {R : Type u_1} [CommRing R] [Finite R] (hsq : Function.Bijective fun (x : R) => x * x) (x : R) : ∃ (n : ℕ), 0 < n ∧ x ^ (n + 1) = x

Bijective squaring on a finite ring makes every element periodic under squaring.

def MIPRE.LowDegree.PrimitiveBinaryComponent {R : Type u_1} [CommRing R] (e : R) : Prop

A primitive nonzero idempotent sees every idempotent as either zero or itself.

Equations

• MIPRE.LowDegree.PrimitiveBinaryComponent e = (e ≠ 0 ∧ e * e = e ∧ ∀ (u : R), u * u = u → e * u = 0 ∨ e * u = e)

theorem MIPRE.LowDegree.PrimitiveBinaryComponent.exists_mul_eq {R : Type u_1} [CommRing R] [Finite R] (hsq : Function.Bijective fun (x : R) => x * x) {e : R} (he : PrimitiveBinaryComponent e) (x : R) (hx : x ≠ 0) (hex : e * x = x) : ∃ (y : R), x * y = e

Every nonzero element supported on a primitive component has an inverse in that component.