English
The matrix of TensorProduct.comm is a permutation of the identity matrix reflecting the swap of factors.
Русский
Матрица TensorProduct.comm представляет переброску факторов и является перестановкой единичной матрицы.
LaTeX
$$toMatrix (bM \otimes bN) (bN \otimes bM) (TensorProduct.comm R M N) = (1 : Matrix (ι × κ) (ι × κ) R).submatrix Prod.swap id$$
Lean4
/-- `TensorProduct.comm` corresponds to a permutation of the identity matrix. -/
theorem toMatrix_comm :
toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM) (TensorProduct.comm R M N) =
(1 : Matrix (ι × κ) (ι × κ) R).submatrix Prod.swap _root_.id :=
by
ext ⟨i, j⟩ ⟨i', j'⟩
simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, comm_tmul,
Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ i', @eq_comm _ j',
smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, and_comm, submatrix_apply, Matrix.one_apply, Prod.swap_prod_mk,
id_eq, Prod.mk.injEq]
