mathlib3 documentation

monlib / linear_algebra.kronecker_to_tensor

Kronecker product to the tensor product #

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

def tensor_product.to_kronecker {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] :

tensor_product R (matrix m m R) (matrix n n R) →ₗ[R] matrix (m × n) (m × n) R

Equations

tensor_product.to_kronecker = {to_fun := λ (x : tensor_product R (matrix m m R) (matrix n n R)) (ij kl : m × n), ⇑((matrix_equiv_tensor R (matrix m m R) n).symm) x ij.snd kl.snd ij.fst kl.fst, map_add' := _, map_smul' := _}

theorem tensor_product.to_kronecker_apply {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x : matrix m m R) (y : matrix n n R) :

⇑tensor_product.to_kronecker (x ⊗ₜ[R] y) = matrix.kronecker_map has_mul.mul x y

def matrix.kronecker_to_tensor_product {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] :

matrix (m × n) (m × n) R →ₗ[R] tensor_product R (matrix m m R) (matrix n n R)

Equations

matrix.kronecker_to_tensor_product = {to_fun := λ (x : matrix (m × n) (m × n) R), ⇑(matrix_equiv_tensor R (matrix m m R) n) (λ (i j : n) (k l : m), x (k, i) (l, j)), map_add' := _, map_smul' := _}

theorem tensor_product.to_kronecker_to_tensor_product {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x : tensor_product R (matrix m m R) (matrix n n R)) :

⇑matrix.kronecker_to_tensor_product (⇑tensor_product.to_kronecker x) = x

theorem matrix.kronecker_to_tensor_product_apply {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x : matrix m m R) (y : matrix n n R) :

⇑matrix.kronecker_to_tensor_product (matrix.kronecker_map has_mul.mul x y) = x ⊗ₜ[R] y

theorem matrix.kronecker_to_tensor_product_to_kronecker {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x : matrix (m × n) (m × n) R) :

⇑tensor_product.to_kronecker (⇑matrix.kronecker_to_tensor_product x) = x

theorem tensor_product.matrix_star {R : Type u_1} {m : Type u_2} {n : Type u_3} [field R] [star_ring R] [fintype m] [fintype n] (x : matrix m m R) (y : matrix n n R) :

has_star.star (x ⊗ₜ[R] y) = x.conj_transpose ⊗ₜ[R] y.conj_transpose

theorem tensor_product.to_kronecker_star {R : Type u_1} {m : Type u_2} {n : Type u_3} [is_R_or_C R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x : matrix m m R) (y : matrix n n R) :

has_star.star (⇑tensor_product.to_kronecker (x ⊗ₜ[R] y)) = ⇑tensor_product.to_kronecker (has_star.star (x ⊗ₜ[R] y))

theorem matrix.kronecker_to_tensor_product_star {R : Type u_1} {m : Type u_2} {n : Type u_3} [is_R_or_C R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x : matrix m m R) (y : matrix n n R) :

has_star.star (⇑matrix.kronecker_to_tensor_product (matrix.kronecker_map has_mul.mul x y)) = ⇑matrix.kronecker_to_tensor_product (has_star.star (matrix.kronecker_map has_mul.mul x y))

theorem matrix.kronecker_eq_sum_std_basis {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x : matrix (m × n) (m × n) R) :

x = finset.univ.sum (λ (i : m), finset.univ.sum (λ (j : m), finset.univ.sum (λ (k : n), finset.univ.sum (λ (l : n), x (i, k) (j, l) • matrix.kronecker_map has_mul.mul (matrix.std_basis_matrix i j 1) (matrix.std_basis_matrix k l 1)))))

theorem tensor_product.matrix_eq_sum_std_basis {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x : tensor_product R (matrix m m R) (matrix n n R)) :

x = finset.univ.sum (λ (i : m), finset.univ.sum (λ (j : m), finset.univ.sum (λ (k : n), finset.univ.sum (λ (l : n), ⇑tensor_product.to_kronecker x (i, k) (j, l) • matrix.std_basis_matrix i j 1 ⊗ₜ[R] matrix.std_basis_matrix k l 1))))

theorem tensor_product.to_kronecker_mul {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x y : tensor_product R (matrix m m R) (matrix n n R)) :

⇑tensor_product.to_kronecker (x * y) = (⇑tensor_product.to_kronecker x).mul (⇑tensor_product.to_kronecker y)

theorem matrix.kronecker_to_tensor_product_mul {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (x y : matrix m m R) (z w : matrix n n R) :

⇑matrix.kronecker_to_tensor_product ((matrix.kronecker_map has_mul.mul x z).mul (matrix.kronecker_map has_mul.mul y w)) = ⇑matrix.kronecker_to_tensor_product (matrix.kronecker_map has_mul.mul x z) * ⇑matrix.kronecker_to_tensor_product (matrix.kronecker_map has_mul.mul y w)

@[simp]

theorem tensor_to_kronecker_symm_apply {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (ᾰ : matrix (m × n) (m × n) R) :

⇑(tensor_to_kronecker.symm) ᾰ = ⇑matrix.kronecker_to_tensor_product ᾰ

def tensor_to_kronecker {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] :

tensor_product R (matrix m m R) (matrix n n R) ≃ₐ[R] matrix (m × n) (m × n) R

Equations

tensor_to_kronecker = {to_fun := ⇑tensor_product.to_kronecker, inv_fun := ⇑matrix.kronecker_to_tensor_product, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

@[simp]

theorem tensor_to_kronecker_apply {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] (ᾰ : tensor_product R (matrix m m R) (matrix n n R)) :

⇑tensor_to_kronecker ᾰ = ⇑tensor_product.to_kronecker ᾰ

def kronecker_to_tensor {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] :

matrix (m × n) (m × n) R ≃ₐ[R] tensor_product R (matrix m m R) (matrix n n R)

Equations

kronecker_to_tensor = tensor_to_kronecker.symm

theorem kronecker_to_tensor_to_linear_map_eq {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] :

kronecker_to_tensor.to_linear_map = matrix.kronecker_to_tensor_product

theorem tensor_to_kronecker_to_linear_map_eq {R : Type u_1} {m : Type u_2} {n : Type u_3} [comm_semiring R] [fintype m] [fintype n] [decidable_eq m] [decidable_eq n] :

tensor_to_kronecker.to_linear_map = tensor_product.to_kronecker