Products of Kronecker products with matrix units

A Kronecker product Matrix.single i j 1 ⊗ₖ X is the block matrix carrying X in the block from j to i and zero elsewhere. Such block matrices multiply along chains: the product of single (a t) (b t) 1 ⊗ₖ X t over a chain in which each block starts where the next one ends is the single block of the product of the X t.

Main results

• Matrix.single_one_kronecker_mul_single_one_kronecker: two block matrices multiply blockwise.
• Matrix.list_prod_ofFn_single_kronecker: the product of the block matrices along a chain.

theorem Matrix.single_one_kronecker_mul_single_one_kronecker {R : Type u_1} {l : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq l] {l' : Type u_4} {l'' : Type u_5} {m' : Type u_6} {m'' : Type u_7} [DecidableEq l'] [DecidableEq l''] [Fintype l'] [Fintype m'] (i : l) (j : l') (k : l'') (X : Matrix m m' R) (Y : Matrix m' m'' R) : kroneckerMap (fun (x1 x2 : R) => x1 * x2) (single i j 1) X * kroneckerMap (fun (x1 x2 : R) => x1 * x2) (single j k 1) Y = kroneckerMap (fun (x1 x2 : R) => x1 * x2) (single i k 1) (X * Y)

Two block matrices multiply blockwise when the first block ends where the second starts. Unlike Matrix.mul_kronecker_mul, this needs no commutativity: the entries of a matrix unit are central.

theorem Matrix.list_prod_ofFn_single_kronecker {R : Type u_1} {l : Type u_2} {m : Type u_3} [Semiring R] [Fintype l] [DecidableEq l] [Fintype m] [DecidableEq m] {n : ℕ} (a b : Fin (n + 1) → l) (X : Fin (n + 1) → Matrix m m R) (h : ∀ (i : Fin n), b i.castSucc = a i.succ) : (List.ofFn fun (t : Fin (n + 1)) => kroneckerMap (fun (x1 x2 : R) => x1 * x2) (single (a t) (b t) 1) (X t)).prod = kroneckerMap (fun (x1 x2 : R) => x1 * x2) (single (a 0) (b (Fin.last n)) 1) (List.ofFn X).prod

A product of block matrices along a chain. If each block X t sits in the block from b t to a t, and each starts where the next one ends, then the product is the block of the product of the X t, from the start b (Fin.last n) of the last block to the end a 0 of the first.