Kronecker product to the tensor product

This file contains the definition of tensor_toKronecker and kronecker_to_tensor, the linear equivalences between ⊗ₜ and ⊗ₖ.

noncomputable def TensorProduct.toKronecker {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : TensorProduct R (Matrix m m R) (Matrix n n R) →ₗ[R] Matrix (m × n) (m × n) R

Equations

• One or more equations did not get rendered due to their size.

theorem TensorProduct.toKronecker_apply {R : Type u_2} {m : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x : Matrix m m R) (y : Matrix n n R) : toKronecker (x ⊗ₜ[R] y) = Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y

noncomputable def Matrix.kroneckerToTensorProduct {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : Matrix (m × n) (m × n) R →ₗ[R] TensorProduct R (Matrix m m R) (Matrix n n R)

Equations

• One or more equations did not get rendered due to their size.

theorem TensorProduct.toKronecker_to_tensorProduct {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x : TensorProduct R (Matrix m m R) (Matrix n n R)) : Matrix.kroneckerToTensorProduct (toKronecker x) = x

theorem Matrix.kroneckerToTensorProduct_apply {R : Type u_2} {m : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x : Matrix m m R) (y : Matrix n n R) : kroneckerToTensorProduct (kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y) = x ⊗ₜ[R] y

theorem Matrix.kroneckerToTensorProduct_toKronecker {R : Type u_3} {m : Type u_2} {n : Type u_1} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x : Matrix (m × n) (m × n) R) : TensorProduct.toKronecker (kroneckerToTensorProduct x) = x

theorem TensorProduct.matrix_star {R : Type u_1} {m : Type u_2} {n : Type u_3} [Field R] [StarRing R] [Fintype m] [Fintype n] (x : Matrix m m R) (y : Matrix n n R) : star (x ⊗ₜ[R] y) = x.conjTranspose ⊗ₜ[R] y.conjTranspose

theorem TensorProduct.toKronecker_star {R : Type u_1} {m : Type u_2} {n : Type u_3} [Field R] [StarRing R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x : TensorProduct R (Matrix m m R) (Matrix n n R)) : star (toKronecker x) = toKronecker (star x)

theorem Matrix.kronecker_eq_sum_std_basis {R : Type u_3} {m : Type u_2} {n : Type u_1} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x : Matrix (m × n) (m × n) R) : x = ∑ i : m, ∑ j : m, ∑ k : n, ∑ l : n, x (i, k) (j, l) • kroneckerMap (fun (x1 x2 : R) => x1 * x2) (stdBasisMatrix i j 1) (stdBasisMatrix k l 1)

theorem TensorProduct.matrix_eq_sum_std_basis {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x : TensorProduct R (Matrix m m R) (Matrix n n R)) : x = ∑ i : m, ∑ j : m, ∑ k : n, ∑ l : n, toKronecker x (i, k) (j, l) • Matrix.stdBasisMatrix i j 1 ⊗ₜ[R] Matrix.stdBasisMatrix k l 1

theorem TensorProduct.toKronecker_hMul {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x y : TensorProduct R (Matrix m m R) (Matrix n n R)) : toKronecker (x * y) = toKronecker x * toKronecker y

theorem Matrix.kroneckerToTensorProduct_hMul {R : Type u_2} {m : Type u_1} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x y : Matrix m m R) (z w : Matrix n n R) : kroneckerToTensorProduct (kroneckerMap (fun (x1 x2 : R) => x1 * x2) x z * kroneckerMap (fun (x1 x2 : R) => x1 * x2) y w) = kroneckerToTensorProduct (kroneckerMap (fun (x1 x2 : R) => x1 * x2) x z) * kroneckerToTensorProduct (kroneckerMap (fun (x1 x2 : R) => x1 * x2) y w)

noncomputable def tensorToKronecker {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : TensorProduct R (Matrix m m R) (Matrix n n R) ≃ₐ[R] Matrix (m × n) (m × n) R

Equations

• tensorToKronecker = { toFun := ⇑TensorProduct.toKronecker, invFun := ⇑Matrix.kroneckerToTensorProduct, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem tensorToKronecker_symm_apply {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (a : Matrix (m × n) (m × n) R) : tensorToKronecker.symm a = Matrix.kroneckerToTensorProduct a

@[simp]

theorem tensorToKronecker_apply {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (a : TensorProduct R (Matrix m m R) (Matrix n n R)) : tensorToKronecker a = TensorProduct.toKronecker a

noncomputable def kroneckerToTensor {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : Matrix (m × n) (m × n) R ≃ₐ[R] TensorProduct R (Matrix m m R) (Matrix n n R)

Equations

• kroneckerToTensor = tensorToKronecker.symm

@[simp]

theorem kroneckerToTensor_symm_apply {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (a✝ : TensorProduct R (Matrix m m R) (Matrix n n R)) : kroneckerToTensor.symm a✝ = TensorProduct.toKronecker a✝

@[simp]

theorem kroneckerToTensor_apply {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (a✝ : Matrix (m × n) (m × n) R) : kroneckerToTensor a✝ = (↑↑tensorToKronecker).symm a✝

theorem Matrix.kroneckerToTensorProduct_star {R : Type u_1} {m : Type u_2} {n : Type u_3} [Field R] [StarRing R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x : Matrix (m × n) (m × n) R) : star (kroneckerToTensorProduct x) = kroneckerToTensorProduct (star x)

theorem kroneckerToTensor_toLinearMap_eq {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : kroneckerToTensor.toLinearMap = Matrix.kroneckerToTensorProduct

theorem tensorToKronecker_toLinearMap_eq {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : tensorToKronecker.toLinearMap = TensorProduct.toKronecker