TensorProduct of Matrix Algebra

Stream: Is there code for X?

[Edison Xie]

import Mathlib.Tactic

variable (K : Type) [Field K]

open BigOperators TensorProduct

def matrix_eqv (n m : ℕ): (Matrix (Fin m) (Fin m) K) ⊗[K] (Matrix (Fin n) (Fin n) K) ≃ₐ[K]
    Matrix (Fin $ n*m) (Fin $ n*m) K := sorry

Hi everyone, is there a code for this? (An algebra isomorphism between MnK ⊗ MmK and MmnK, I get that the equivalence may be coming from kronecker product but I feel like there should be some direct proof in mathlib already? Thanks a lot for any help!!

[Eric Wieser]

I'm pretty sure this was asked quite recently; though certainly you should not expect the result to be about Fin m

[Eric Wieser]

The version I'd expect is

import Mathlib.Tactic

variable (K : Type) [Field K]

open BigOperators TensorProduct

def matrix_eqv (n m : Type*) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] :
    (Matrix m m K) ⊗[K] (Matrix n n K) ≃ₐ[K] Matrix (n × m) (n × m) K := sorry

[Eric Wieser]

Ah, here's the thread I'm thinking of

[Edison Xie]

Eric Wieser said:

I'm pretty sure this was asked quite recently; though certainly you should not expect the result to be about Fin m

Thx for the tips but I 'm wondering if there's an algebra isomorphism as below :

def matrix_eqv' (n m : ℕ): (Matrix (Fin n × Fin m) (Fin n × Fin m) K) ≃ₐ[K] Matrix (Fin (n * m)) (Fin (n * m)) K :=  sorry

[Edison Xie]

I know there is an equivalence between Fin n × Fin m and Fin (n * m) by finProdFinEquiv but can I somehow apply this to get the isomorphism?

[Edison Xie]

Ah okay I found Matrix.reindexAlgEquiv to solve that but my previous problem remains even after reading the question page you gave me :((

[Eric Wieser]

Sorry if I was unclear; my point above was that you should first try to solve my sorry, and only once you have that one recover yours as a special case

[Eric Wieser]

Indeed, the other thread isn't as relevant as I thought it might be

[Eric Wieser]

A good start to the first sorry is AlgEquiv.ofAlgHom (Algebra.TensorProduct.lift _ _ _) _ _ _

[Eric Wieser]

Here's one direction:

noncomputable def matrixEquivForward (n m : Type*) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] :
    Matrix m m K ⊗[K] Matrix n n K →ₐ[K] Matrix (m × n) (m × n) K :=
  Algebra.TensorProduct.algHomOfLinearMapTensorProduct
    (TensorProduct.lift Matrix.kroneckerBilinear)
    (fun _ _ _ _ => Matrix.mul_kronecker_mul _ _ _ _)
    (Matrix.one_kronecker_one (α := K))

open scoped Kronecker in
theorem matrixEquivForward_tmul (n m : Type*) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (M : Matrix m m K) (N : Matrix n n K) : matrixEquivForward K n m (N ⊗ₜ M) = N ⊗ₖ M := rfl

[Eric Wieser]

I assume the reverse you want is something like

noncomputable def matrixEquivRev (n m : Type*) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] :
    Matrix (m × n) (m × n) K →ₐ[K] Matrix m m K ⊗[K] Matrix n n K :=
  AlgHom.ofLinearMap
    (Basis.constr (S := K) (Matrix.stdBasis K _ _) fun p =>
      Matrix.stdBasisMatrix p.1.1 p.2.1 1 ⊗ₜ Matrix.stdBasisMatrix p.1.2 p.2.2 1)
    sorry
    sorry

[Edison Xie]

Eric Wieser said:

I assume the reverse you want is something like

noncomputable def matrixEquivRev (n m : Type*) [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] :
    Matrix (m × n) (m × n) K →ₐ[K] Matrix m m K ⊗[K] Matrix n n K :=
  AlgHom.ofLinearMap
    (Basis.constr (S := K) (Matrix.stdBasis K _ _) fun p =>
      Matrix.stdBasisMatrix p.1.1 p.2.1 1 ⊗ₜ Matrix.stdBasisMatrix p.1.2 p.2.2 1)
    sorry
    sorry

thanks this is exactly what I'm looking for :)