Kronecker / TensorProduct equivalence

Stream: Is there code for X?

[Alex Meiburg]

I'm looking for a linear equivalence like
(Matrix B B R ⊗[R] Matrix D D R) ≃ₗ[R] Matrix (B × B) (D × D) R
or
(Matrix B B R ⊗[R] Matrix D D R) ≃ₗ[R] Matrix (B × D) (B × D) R
but I'm admittedly having a hard time understanding some statements like Matrix.toLin_kronecker and friends.

Actually, is it possible that I don't want tensor products here at all?
My end goal is that I want to say "here's one linear map A from matrices of shape W to matrices of shape X, here's another linear map B from matrices Y to matrices Z, here's their product which maps matrices of shape (W ⊗ Y) to (X ⊗ Z), where ⊗ is the kronecker product.

[Alex Meiburg]

I was able to write this definition:

noncomputable def MatrixMap_prod (M₁ : Matrix A A R →ₗ[R] Matrix B B R) (M₂ : Matrix C C R →ₗ[R] Matrix D D R)
    : Matrix (A × C) (A × C) R →ₗ[R] Matrix (B × D) (B × D) R
    :=
  let h₁ := (LinearMap.toMatrix (Basis.tensorProduct (Matrix.stdBasis R A A) (Matrix.stdBasis R C C))
      (Basis.tensorProduct (Matrix.stdBasis R B B) (Matrix.stdBasis R D D)))
    (TensorProduct.map M₁ M₂);
  let r₁ := Equiv.prodProdProdComm B B D D;
  let r₂ := Equiv.prodProdProdComm A A C C;
  let h₂ := Matrix.reindex r₁ r₂ h₁;
  Matrix.toLin (Matrix.stdBasis R (A × C) (A × C)) (Matrix.stdBasis R (B × D) (B × D)) h₂

which is, honestly, quite a mess. h₁ can equivalently be written

let h₁ := ((LinearMap.toMatrix (Matrix.stdBasis R A A) (Matrix.stdBasis R B B)) M₁) ⊗ₖ ((LinearMap.toMatrix (Matrix.stdBasis R C C) (Matrix.stdBasis R D D)) M₂)

(the equality of these is is precisely TensorProduct.toMatrix_map), but that's not really any cleaner or better.

[Eric Wieser]

What's the equation that you want the result to satisfy? MatrixMap_prod M₁ M₂ M (b₁, d₁) (b₂, d₂) = _?

[Alex Meiburg]

I think these are the (equivalent) properties that I want

/-- A `MatrixMap` is a linear map between squares matrices of size A to size B, over R. -/
abbrev MatrixMap (A B R : Type*) [Semiring R] := Matrix A A R →ₗ[R] Matrix B B R

variable {A B R : Type*} [Fintype A] [Fintype B] [CommSemiring R] [DecidableEq A] [DecidableEq B]

noncomputable def MatrixMap_Prod (M₁ : MatrixMap A B R) (M₂ : MatrixMap C D R) : MatrixMap (A × C) (B × D) R :=
  let h₁ := (LinearMap.toMatrix (Basis.tensorProduct (Matrix.stdBasis R A A) (Matrix.stdBasis R C C))
      (Basis.tensorProduct (Matrix.stdBasis R B B) (Matrix.stdBasis R D D)))
    (TensorProduct.map M₁ M₂);
  let r₁ := Equiv.prodProdProdComm B B D D;
  let r₂ := Equiv.prodProdProdComm A A C C;
  let h₂ := Matrix.reindex r₁ r₂ h₁;
  Matrix.toLin (Matrix.stdBasis R (A × C) (A × C)) (Matrix.stdBasis R (B × D) (B × D)) h₂

open BigOperators
theorem MatrixMap_Prod_def (M₁ : MatrixMap A B R) (M₂ : MatrixMap C D R) (M : Matrix (A × C) (A × C) R) :
    MatrixMap_Prod M₁ M₂ M (b₁, d₁) (b₂, d₂) =
  ∑ a₁, ∑ a₂, ∑ c₁, ∑ c₂, (M₁ (Matrix.stdBasisMatrix a₁ a₂ 1) b₁ b₂) * (M₂ (Matrix.stdBasisMatrix c₁ c₂ 1) d₁ d₂) * (M (a₁, c₁) (a₂, c₂)) := by
  sorry

open Kronecker
theorem MatrixMap_Prod_kron (M₁ : MatrixMap A B R) (M₂ : MatrixMap C D R) (MA : Matrix A A R) (MC : Matrix C C R) :
    MatrixMap_Prod M₁ M₂ (MA ⊗ₖ MC) = (M₁ MA) ⊗ₖ (M₂ MC) := by
  sorry

the MatrixMap_Prod_def could be used as an alternate definition. The real defining property that I want is MatrixMap_Prod_kron, which fully defines the map by linear combination, but not in a way that immediately yields an actual definition. But given MatrixMap_Prod_kron, I'm hoping there's some way to state the original thing in a cleaner way (maybe without needing to mention Matrix.stdBasisMatrix and Matrix.stdBasis, which feel hacky here.)