English
The matrix of TensorProduct.map f g with respect to bases bM,bN,bM',bN' equals the Kronecker product of the matrices of f and g.
Русский
Матрица отображения TensorProduct.map f g относительно баз имеет вид тензорной (кронекеровской) матрицы из матриц f и g.
LaTeX
$$$toMatrix (bM \otimes bN) (bM' \otimes bN') (TensorProduct.map f g) = toMatrix bM bM' f \otimes_κ toMatrix bN bN' g$$$
Lean4
/-- The linear map built from `TensorProduct.map` corresponds to the matrix built from
`Matrix.kronecker`. -/
theorem toMatrix_map (f : M →ₗ[R] M') (g : N →ₗ[R] N') :
toMatrix (bM.tensorProduct bN) (bM'.tensorProduct bN') (TensorProduct.map f g) =
toMatrix bM bM' f ⊗ₖ toMatrix bN bN' g :=
by
ext ⟨i, j⟩ ⟨i', j'⟩
simp_rw [Matrix.kroneckerMap_apply, toMatrix_apply, Basis.tensorProduct_apply, TensorProduct.map_tmul,
Basis.tensorProduct_repr_tmul_apply]
exact mul_comm _ _
