Matrix type issue

Stream: maths

[Anirudh Suresh]

import Mathlib
open scoped Matrix

def tensor_product_2 {m n o p : ℕ} (A : Matrix (Fin m) (Fin n) ℂ)
  (B : Matrix (Fin o) (Fin p) ℂ) : Matrix (Fin (m * o)) (Fin (n * p)) ℂ :=
(Matrix.kroneckerMap (fun (a:ℂ) (b:ℂ) => a*b) A B).reindex finProdFinEquiv finProdFinEquiv

infixl:80 " ⊗ " => tensor_product_2
set_option diagnostics true

theorem t1 (q1 q2: Matrix (Fin 2) (Fin 1) ℂ) : !![1, 0, 0, 0; 0, 0, 1, 0; 0, 1, 0, 0; 0, 0, 0, 1] * (q1)⊗(q2) = (q2)⊗(q1):=by {

}

}

This matrix multiplication is not working because Fin(22) is not seen the same as Fin (4) by Lean 4. Is there a way to fix this other than defining an instance for this multiplication every time? Is there a way that my tensor product sees Fin (22) as Fin (4) by default?

[Matt Diamond]

(FYI your post is a bit garbled because you wrote 2 * 2 without spaces, so Zulip is interpreting this as italics and it looks like you're saying 22 instead of 2 * 2)

[Eric Wieser]

(or #backticks)

[Aaron Liu]

The actual problem is that you have a Matrix (Fin 4) (Fin 4) ℂ and are trying to multiply a Matrix (Fin (2 * 2)) (Fin (1 * 1)) ℂ, which just doesn't work.

[Aaron Liu]

Fin (2 * 2) vs Fin 4 is actually not an issue.

[Aaron Liu]

Try using docs#Matrix.addMonoidHomMulLeft instead?

[Aaron Liu]

Actually, it looks like we have a docs#Matrix.instHMulOfFintypeOfMulOfAddCommMonoid, so I'm not sure what the problem is.

[Eric Wieser]

The problem is that the instance resolution doesn't unfold * here

[Eric Wieser]

Or at least, the reason why that instance doesn't apply. I don't think this should necesarily be expected to work

[Aaron Liu]

The problem is your explicit matrix is a matrix of ℕ

[Aaron Liu]

You need a type annotation to make it a matrix of ℂ

[Aaron Liu]

Then the instance just works

[Anirudh Suresh]

this makes sense but does lean consider Fin(2 times 2) the same as Fin 4 because when I end up doing the following, I get an error in the case of i but not in the case of j as Lean sees j to be of type Fin (1 times 1)

import Mathlib
open scoped Matrix

def tensor_product_2 {m n o p : ℕ} (A : Matrix (Fin m) (Fin n) ℂ)
  (B : Matrix (Fin o) (Fin p) ℂ) : Matrix (Fin (m * o)) (Fin (n * p)) ℂ :=
(Matrix.kroneckerMap (fun (a:ℂ) (b:ℂ) => a*b) A B).reindex finProdFinEquiv finProdFinEquiv

infixl:80 " ⊗ " => tensor_product_2

theorem t1 (q1 q2: Matrix (Fin 2) (Fin 1) ℂ) : (!![1, 0, 0, 0; 0, 0, 1, 0; 0, 1, 0, 0; 0, 0, 0, 1]: Matrix (Fin 4) (Fin 4) ℂ) * (q1)⊗(q2) = (q2)⊗(q1):=by {
  unfold tensor_product_2
  ext i j
  obtain ⟨i1, i2, hi⟩ := finProdFinEquiv.symm i
  obtain ⟨j1, j2, hj⟩ := finProdFinEquiv.symm j
}

[Matt Diamond]

one option is to write ext (i : Fin (2 * 2)) j instead of ext i j

[Matt Diamond]

also you probably want to write it like obtain ⟨⟨i1, i1h⟩, ⟨i2, i2h⟩⟩ := finProdFinEquiv.symm i to correctly destructure the Fin n values

[Eric Wieser]

Destructing feels like the wrong approach here

[Matt Diamond]

that's fair... I was just explaining what to do if he wanted to destructure them, since it seemed like that was the intention of his code... but yes, it might not be useful

[Eric Wieser]

This works:

theorem t1 (q1 q2: Matrix (Fin 2) (Fin 1) ℂ) :
    !![1, 0, 0, 0; 0, 0, 1, 0; 0, 1, 0, 0; 0, 0, 0, (1 : ℂ)].reindex
      (Fin.castOrderIso <| by rfl).toEquiv (Fin.castOrderIso <| by rfl).toEquiv * (q1 ⊗ q2) = q2 ⊗ q1 := by
  unfold tensor_product_2
  ext i j
  obtain ⟨i1, i2, hi⟩ := finProdFinEquiv.symm i
  obtain ⟨j1, j2, hj⟩ := finProdFinEquiv.symm j

[Eric Wieser]

Of couse if you resign to using reindex, then you probably aren't getting anything from tensor_product_2 any more:

open scoped Kronecker

theorem t1 (q1 q2: Matrix (Fin 2) (Fin 1) ℂ) :
    !![1, 0, 0, 0; 0, 0, 1, 0; 0, 1, 0, 0; 0, 0, 0, (1 : ℂ)].reindex
      finProdFinEquiv.symm finProdFinEquiv.symm * (q1 ⊗ₖ q2) = (q2 ⊗ₖ q1) :=

[Anirudh Suresh]

Eric Wieser said:

Of couse if you resign to using reindex, then you probably aren't getting anything from tensor_product_2 any more:

open scoped Kronecker

theorem t1 (q1 q2: Matrix (Fin 2) (Fin 1) ℂ) :
    !![1, 0, 0, 0; 0, 0, 1, 0; 0, 1, 0, 0; 0, 0, 0, (1 : ℂ)].reindex
      finProdFinEquiv.symm finProdFinEquiv.symm * (q1 ⊗ₖ q2) = (q2 ⊗ₖ q1) :=

What exactly is the reason why reindexing is done in the definition of the theorem? Is it not possible to prove the theorem otherwise? Moreover, it is important for me to use tensor_product_2 because of how I want to use matrices and kronecker products.

[Eric Wieser]

For the example you quoted it's of course not possible to state without reindex; for the previous one I did it because it helps ext to do the right thing automatically. You're right that it should be just as possible to prove without doing so.

[Eric Wieser]

Another way you can modify your original non-working proof is with obtain ⟨i1, i2⟩ := finProdFinEquiv (m := 2) (n := 2).symm i

[Eric Wieser]

Though Matt's suggestion above is a little cleaner than that

[Eric Wieser]

Maybe this is helpful?

theorem t1 (q1 q2: Matrix (Fin 2) (Fin 1) ℂ) :
    (!![1, 0, 0, 0; 0, 0, 1, 0; 0, 1, 0, 0; 0, 0, 0, 1]: Matrix (Fin 4) (Fin 4) ℂ) * (q1)⊗(q2) = (q2)⊗(q1) := by
  ext (i : Fin (2 * 2)) j
  revert i j
  simp_rw [finProdFinEquiv.surjective.forall]
  rintro ⟨i1, i2⟩ ⟨j1, j2⟩

[Anirudh Suresh]

Yes this seems to work. Does this make it harder to proceed with the proof as compared to using the reindex?

[Eric Wieser]

I don't know for sure

[Anirudh Suresh]

import Mathlib
open scoped Matrix

def tensor_product_2 {m n o p : ℕ} (A : Matrix (Fin m) (Fin n) ℂ)
  (B : Matrix (Fin o) (Fin p) ℂ) : Matrix (Fin (m * o)) (Fin (n * p)) ℂ :=
(Matrix.kroneckerMap (fun (a:ℂ) (b:ℂ) => a*b) A B).reindex finProdFinEquiv finProdFinEquiv

infixl:80 " ⊗ " => tensor_product_2

theorem t1 (q1 q2: Matrix (Fin 2) (Fin 1) ℂ) :
    (!![1, 0, 0, 0; 0, 0, 1, 0; 0, 1, 0, 0; 0, 0, 0, 1]: Matrix (Fin 4) (Fin 4) ℂ) * (q1)⊗(q2) = (q2)⊗(q1) := by
    {
      ext (i : Fin (2 * 2)) j
      revert i j
      simp_rw [finProdFinEquiv.surjective.forall]
      rintro ⟨i1, i2⟩ ⟨j1, j2⟩
      unfold tensor_product_2
      simp [Matrix.mul_apply]

    }

Another issue I am facing is that when I simplify the definitions, I get a sum over Fin 4. Is it possible to split this summation as the sum of four terms or is there a better way to go about proving this?

[Aaron Liu]

That should be a simproc

[Aaron Liu]

I don't know if it exists or not

[Aaron Liu]

A quick search turns up nothing

[Aaron Liu]

See #mathlib4 > potential simp_procs @ 💬

[Bhavik Mehta]

docs#Fin.sum_univ_four