Binary cyclic group algebras as circulant matrices

def MIPRE.LowDegree.BinaryLinear.groupMatrix {G : Type u_1} [AddCommGroup G] (z : AddMonoidAlgebra (ZMod 2) G) : Matrix G G (ZMod 2)

The regular representation of a finite binary group algebra is circulant.

Equations

• MIPRE.LowDegree.BinaryLinear.groupMatrix z = Matrix.circulant ⇑z.coeff

theorem MIPRE.LowDegree.BinaryLinear.groupMatrix_mul {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (z w : AddMonoidAlgebra (ZMod 2) G) : groupMatrix (z * w) = groupMatrix z * groupMatrix w

def MIPRE.LowDegree.BinaryLinear.groupMatrixHom {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] : AddMonoidAlgebra (ZMod 2) G →+* Matrix G G (ZMod 2)

The identity and product laws allow algebraic square roots to be used as matrices.

Equations

• MIPRE.LowDegree.BinaryLinear.groupMatrixHom = { toFun := MIPRE.LowDegree.BinaryLinear.groupMatrix, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem MIPRE.LowDegree.BinaryLinear.groupMatrix_injective {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] : Function.Injective groupMatrix

theorem MIPRE.LowDegree.BinaryLinear.groupMatrix_binarySquareRoot {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (hG : Odd (Fintype.card G)) (z : AddMonoidAlgebra (ZMod 2) G) : groupMatrix (binarySquareRoot z) * groupMatrix (binarySquareRoot z) = groupMatrix z

The explicit group-algebra square root gives an exact matrix square root.

noncomputable def MIPRE.LowDegree.BinaryLinear.finGroupOfVector {k : ℕ} [NeZero k] (v : Fin k → ZMod 2) : AddMonoidAlgebra (ZMod 2) (Fin k)

Coefficient vectors are encoded with the same ordering as binary matrices.

Equations

• MIPRE.LowDegree.BinaryLinear.finGroupOfVector v = AddMonoidAlgebra.ofCoeff (Finsupp.onFinset Finset.univ v ⋯)

@[simp]

theorem MIPRE.LowDegree.BinaryLinear.coeff_finGroupOfVector {k : ℕ} [NeZero k] (v : Fin k → ZMod 2) (i : Fin k) : (finGroupOfVector v).coeff i = v i

theorem MIPRE.LowDegree.BinaryLinear.inverseMatrix_groupMatrix {k : ℕ} [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (hz : Function.Surjective (groupMatrix z).mulVec) : ∃ (u : AddMonoidAlgebra (ZMod 2) (Fin k)), z * u = 1 ∧ inverseMatrix (groupMatrix z) = groupMatrix u

The computed inverse of a nonsingular circulant is again circulant.

def MIPRE.LowDegree.BinaryLinear.inverseRootMatrix {k : ℕ} [NeZero k] (A : Matrix (Fin k) (Fin k) (ZMod 2)) : Matrix (Fin k) (Fin k) (ZMod 2)

The inverse circulant's square root is read from doubled indices of its first column.

Equations

• MIPRE.LowDegree.BinaryLinear.inverseRootMatrix A = Matrix.circulant fun (i : Fin k) => MIPRE.LowDegree.BinaryLinear.inverseMatrix A (i + i) 0

theorem MIPRE.LowDegree.BinaryLinear.inverseRootMatrix_square {k : ℕ} [NeZero k] (hk : Odd k) (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (hz : Function.Surjective (groupMatrix z).mulVec) : inverseRootMatrix (groupMatrix z) * inverseRootMatrix (groupMatrix z) = inverseMatrix (groupMatrix z)

theorem MIPRE.LowDegree.BinaryLinear.inverseMatrix_isSymm {k : ℕ} (A : Matrix (Fin k) (Fin k) (ZMod 2)) (hA : Function.Surjective A.mulVec) (hs : A.IsSymm) : (inverseMatrix A).IsSymm

Transposition preserves the unique inverse of a symmetric matrix.

theorem MIPRE.LowDegree.BinaryLinear.inverseRootMatrix_isSymm {k : ℕ} [NeZero k] (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (hz : Function.Surjective (groupMatrix z).mulVec) (hs : (groupMatrix z).IsSymm) : (inverseRootMatrix (groupMatrix z)).IsSymm

theorem MIPRE.LowDegree.BinaryLinear.inverseRootMatrix_gram {k : ℕ} [NeZero k] (hk : Odd k) (z : AddMonoidAlgebra (ZMod 2) (Fin k)) (hz : Function.Surjective (groupMatrix z).mulVec) (hs : (groupMatrix z).IsSymm) : (inverseRootMatrix (groupMatrix z)).transpose * groupMatrix z * inverseRootMatrix (groupMatrix z) = 1

The explicit doubled-index square root self-dualizes every nonsingular symmetric circulant.