Matrices commuting with the Kronecker powers of orthogonal matrices

Let M be a matrix with rows and columns indexed by κ → ι which commutes with the Kronecker power A.kroneckerPower κ of every matrix A with Aᵀ * A = 1. The signed permutation matrices are orthogonal, and testing M against their Kronecker powers constrains its entries:

• relabelling every index by a permutation of ι does not change an entry of M;
• when 2 ≠ 0 and there are no zero divisors, an entry of M vanishes as soon as some label occurs an odd number of times among the row index and an even number of times among the column index, or the reverse: the diagonal sign matrix negating that label acts on the row and on the column with opposite signs.

These are the first steps of the description of the commutant of the orthogonal group on a tensor power by Brauer diagrams.

Main results

• Matrix.apply_comp_mul_prod_of_forall_commute_kroneckerPower: invariance under a signed permutation.
• Matrix.apply_comp_comp_of_commute_kroneckerPower: invariance under relabelling.
• Matrix.apply_eq_zero_of_commute_kroneckerPower: the parity constraint on the entries.

theorem Matrix.apply_comp_mul_prod_of_forall_commute_kroneckerPower {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {M : Matrix (κ → ι) (κ → ι) R} (hM : ∀ (A : Matrix ι ι R), A.transpose * A = 1 → Commute M (kroneckerPower κ A)) (σ : Equiv.Perm ι) {d : ι → R} (hd : ∀ (i : ι), d i * d i = 1) (v u : κ → ι) : M (⇑σ ∘ v) (⇑σ ∘ u) * ∏ i : κ, d (u i) = (∏ i : κ, d (v i)) * M v u

A matrix commuting with the Kronecker powers of all orthogonal matrices is invariant under the signed permutation matrix sending e_j to d j • e_(σ j).

theorem Matrix.apply_comp_comp_of_commute_kroneckerPower {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {M : Matrix (κ → ι) (κ → ι) R} (hM : ∀ (A : Matrix ι ι R), A.transpose * A = 1 → Commute M (kroneckerPower κ A)) (σ : Equiv.Perm ι) (v u : κ → ι) : M (⇑σ ∘ v) (⇑σ ∘ u) = M v u

A matrix commuting with the Kronecker powers of all orthogonal matrices is invariant under relabelling by a permutation.

theorem Matrix.apply_eq_zero_of_commute_kroneckerPower {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {M : Matrix (κ → ι) (κ → ι) R} [NoZeroDivisors R] (hM : ∀ (A : Matrix ι ι R), A.transpose * A = 1 → Commute M (kroneckerPower κ A)) (h2 : 2 ≠ 0) {v u : κ → ι} (a : ι) (h : ¬(Even {i : κ | v i = a}.card ↔ Even {i : κ | u i = a}.card)) : M v u = 0

The parity constraint. An entry of a matrix commuting with the Kronecker powers of all orthogonal matrices vanishes when a label a occurs an even number of times in the row index and an odd number of times in the column index, or the reverse: the diagonal sign matrix negating a acts on the row and on the column with opposite signs.