tensor product of matrix

Stream: Is there code for X?

[Edison Xie]

Do we have

def matrix_eqv (K : Type u) [Field K] (m n : ℕ): (Matrix (Fin m) (Fin m) K) ⊗[K] (Matrix (Fin n) (Fin n) K) ≃ₐ[K]
    Matrix (Fin m × Fin n) (Fin m × Fin n) K := sorry

this in mathlib4? If not I'm going to PR this :)

[Eric Wieser]

That should certainly not be limited to Fin!

[Ruben Van de Velde]

And should be camelCase

[Eric Wieser]

Previous thread here: #Is there code for X? > Kronecker / TensorProduct equivalence @ 💬

[Junyan Xu]

You can combine matrixEquivTensor with Matrix.compAlgEquiv

[Edison Xie]

I have it for field I’m wondering if I could generalise if to CommRing

[Junyan Xu]

Both of the above works for a Semiring that is an Algebra over a CommSemiring.

[Edison Xie]

Got it!

[Junyan Xu]

import Mathlib.RingTheory.PolynomialAlgebra
-- #find_home finds this, but maybe we should add some import to an earlier file instead

open TensorProduct
noncomputable def matrix_eqv (K : Type u) [CommSemiring K] (m n)
    [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.comm ..).trans <| (matrixEquivTensor ..).symm.trans <|
    Matrix.compAlgEquiv ..

[Eric Wieser]

Here's the big one:

noncomputable def matrix_eqv (K A B : Type*) [CommSemiring K] [Semiring A] [Algebra K A] [Semiring B] [Algebra K B] (m n)
    [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] :
    Matrix m m A ⊗[K] Matrix n n B ≃ₐ[K] Matrix (m × n) (m × n) (A ⊗[K] B) :=
  Algebra.TensorProduct.congr (matrixEquivTensor _ _ _) (matrixEquivTensor _ _ _)
    |>.trans <| (Algebra.TensorProduct.tensorTensorTensorComm K _ _ _ _)
    |>.trans <|
      .trans (Algebra.TensorProduct.congr .refl <|
        Algebra.TensorProduct.comm K _ _
          |>.trans <| (matrixEquivTensor _ _ _).symm
          |>.trans <| Matrix.compAlgEquiv _ _ K K
      ) <| (matrixEquivTensor ..).symm

[Eric Wieser]

I'll Pr the above

[Edison Xie]

Thanks :folded_hands:

[Eric Wieser]

#21148, but the characterizing lemma is missing still

[Eric Wieser]

@Alex Meiburg ^

[Alex Meiburg]

Oh wow that is perfect timing haha. Just so happens that tomorrow I and a few others are going on a retreat where we're going to try to prove a theorem that involves, among other things, a whole bunch of working with tensor products. (We were just going to sorry the relevant things out)

Edit: just kidding, I didn't read carefully enough. I thought this was about Kronecker product pi types

[Alex Meiburg]

Less exciting. But still good to have!

[Eric Wieser]

I added the characterizing lemmas, cleanup is a problem for another time

[Eric Wieser]

I split off #21204 from #21148, but everything should now be cleaned up