Documentation

Mathlib.RingTheory.MatrixAlgebra

Algebra isomorphisms between tensor products and matrices #

Main definitions #

noncomputable def kroneckerTMulLinearEquiv (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (M : Type u_8) (N : Type u_9) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] :
TensorProduct R (Matrix l m M) (Matrix n p N) ≃ₗ[R] Matrix (l × n) (m × p) (TensorProduct R M N)

Matrix.kroneckerTMul as a linear equivalence, when the two arguments are tensored.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem kroneckerTMulLinearEquiv_tmul (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (M : Type u_8) (N : Type u_9) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (a : Matrix l m M) (b : Matrix n p N) :
(kroneckerTMulLinearEquiv l m n p R M N) (a ⊗ₜ[R] b) = Matrix.kroneckerMap (fun (x1 : M) (x2 : N) => x1 ⊗ₜ[R] x2) a b
@[simp]
theorem kroneckerTMulAlgEquiv_symm_single_tmul (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (M : Type u_8) (N : Type u_9) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ia : l) (ja : m) (ib : n) (jb : p) (a : M) (b : N) :
(kroneckerTMulLinearEquiv l m n p R M N).symm (Matrix.single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) = Matrix.single ia ja a ⊗ₜ[R] Matrix.single ib jb b
@[deprecated kroneckerTMulAlgEquiv_symm_single_tmul (since := "2025-05-05")]
theorem kroneckerTMulAlgEquiv_symm_stdBasisMatrix_tmul (l : Type u_1) (m : Type u_2) (n : Type u_3) (p : Type u_4) (R : Type u_5) (M : Type u_8) (N : Type u_9) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Fintype l] [Fintype m] [Fintype n] [Fintype p] [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ia : l) (ja : m) (ib : n) (jb : p) (a : M) (b : N) :
(kroneckerTMulLinearEquiv l m n p R M N).symm (Matrix.single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) = Matrix.single ia ja a ⊗ₜ[R] Matrix.single ib jb b

Alias of kroneckerTMulAlgEquiv_symm_single_tmul.

@[simp]
theorem kroneckerTMulLinearEquiv_one (m : Type u_2) (n : Type u_3) (R : Type u_5) {A : Type u_6} {B : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] :
(kroneckerTMulLinearEquiv m m n n R A B) 1 = 1
@[simp]
theorem kroneckerTMulLinearEquiv_mul (m : Type u_2) (n : Type u_3) (R : Type u_5) {A : Type u_6} {B : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (x y : TensorProduct R (Matrix m m A) (Matrix n n B)) :
(kroneckerTMulLinearEquiv m m n n R A B) (x * y) = (kroneckerTMulLinearEquiv m m n n R A B) x * (kroneckerTMulLinearEquiv m m n n R A B) y

Note this can't be stated for rectangular matrices because there is no HMul (TensorProduct R _ _) (TensorProduct R _ _) (TensorProduct R _ _) instance.

noncomputable def MatrixEquivTensor.toFunBilinear (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] :
A →ₗ[R] Matrix n n R →ₗ[R] Matrix n n A

(Implementation detail). The function underlying (A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A, as an R-bilinear map.

Equations
@[simp]
theorem MatrixEquivTensor.toFunBilinear_apply (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (m : Matrix n n R) :
((toFunBilinear n R A) a) m = a m.map (algebraMap R A)
noncomputable def MatrixEquivTensor.toFunLinear (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] :
TensorProduct R A (Matrix n n R) →ₗ[R] Matrix n n A

(Implementation detail). The function underlying (A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A, as an R-linear map.

Equations
noncomputable def MatrixEquivTensor.toFunAlgHom (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] :
TensorProduct R A (Matrix n n R) →ₐ[R] Matrix n n A

The function (A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A, as an algebra homomorphism.

Equations
@[simp]
theorem MatrixEquivTensor.toFunAlgHom_apply (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (a : A) (m : Matrix n n R) :
(toFunAlgHom n R A) (a ⊗ₜ[R] m) = a m.map (algebraMap R A)
noncomputable def MatrixEquivTensor.invFun (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M : Matrix n n A) :
TensorProduct R A (Matrix n n R)

(Implementation detail.)

The bare function Matrix n n A → A ⊗[R] Matrix n n R. (We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)

Equations
@[simp]
theorem MatrixEquivTensor.invFun_zero (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] :
invFun n R A 0 = 0
@[simp]
theorem MatrixEquivTensor.invFun_add (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M N : Matrix n n A) :
invFun n R A (M + N) = invFun n R A M + invFun n R A N
@[simp]
theorem MatrixEquivTensor.invFun_smul (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (a : A) (M : Matrix n n A) :
invFun n R A (a M) = a ⊗ₜ[R] 1 * invFun n R A M
@[simp]
theorem MatrixEquivTensor.invFun_algebraMap (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M : Matrix n n R) :
invFun n R A (M.map (algebraMap R A)) = 1 ⊗ₜ[R] M
theorem MatrixEquivTensor.right_inv (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M : Matrix n n A) :
(toFunAlgHom n R A) (invFun n R A M) = M
theorem MatrixEquivTensor.left_inv (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M : TensorProduct R A (Matrix n n R)) :
invFun n R A ((toFunAlgHom n R A) M) = M
noncomputable def MatrixEquivTensor.equiv (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] :
TensorProduct R A (Matrix n n R) Matrix n n A

(Implementation detail)

The equivalence, ignoring the algebra structure, (A ⊗[R] Matrix n n R) ≃ Matrix n n A.

Equations
noncomputable def matrixEquivTensor (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] :
Matrix n n A ≃ₐ[R] TensorProduct R A (Matrix n n R)

The R-algebra isomorphism Matrix n n A ≃ₐ[R] (A ⊗[R] Matrix n n R).

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem matrixEquivTensor_apply (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (M : Matrix n n A) :
(matrixEquivTensor n R A) M = p : n × n, M p.1 p.2 ⊗ₜ[R] Matrix.single p.1 p.2 1
@[simp]
theorem matrixEquivTensor_apply_single (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (i j : n) (x : A) :
@[deprecated matrixEquivTensor_apply_single (since := "2025-05-05")]
theorem matrixEquivTensor_apply_stdBasisMatrix (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (i j : n) (x : A) :

Alias of matrixEquivTensor_apply_single.

@[simp]
theorem matrixEquivTensor_apply_symm (n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (a : A) (M : Matrix n n R) :
(matrixEquivTensor n R A).symm (a ⊗ₜ[R] M) = a M.map (algebraMap R A)
noncomputable def Matrix.kroneckerTMulAlgEquiv (m : Type u_2) (n : Type u_3) (R : Type u_5) (A : Type u_6) (B : Type u_7) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] :
TensorProduct R (Matrix m m A) (Matrix n n B) ≃ₐ[R] Matrix (m × n) (m × n) (TensorProduct R A B)

Matrix.kroneckerTMul as an algebra equivalence, when the two arguments are tensored.

Equations
@[simp]
theorem Matrix.kroneckerTMulAlgEquiv_apply {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} {B : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (x : TensorProduct R (Matrix m m A) (Matrix n n B)) :
(kroneckerTMulAlgEquiv m n R A B) x = (kroneckerTMulLinearEquiv m m n n R A B) x
@[simp]
theorem Matrix.kroneckerTMulAlgEquiv_symm_apply {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} {B : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (x : Matrix (m × n) (m × n) (TensorProduct R A B)) :
(kroneckerTMulAlgEquiv m n R A B).symm x = (kroneckerTMulLinearEquiv m m n n R A B).symm x