## Stream: maths

### Topic: Tensor product of matrices

#### Bassem Safieldeen (Jul 09 2020 at 23:32):

I am trying to do stuff with matrices and tensor products, and I am facing two slightly unrelated problems.

The first is that Lean complains when I try to define the matrix ![![1/2, 0], ![0, 1/2]] (please see code below). The problem goes away if I replace the 1/2's with 1's.

The second is that the tensor product  (|ψ⟩⟨ψ| ⊗ₜ[ℂ] |ψ⟩⟨ψ|) doesn't seem to return a matrix whose entries I can access. Lean says that |ψ⟩⟨ψ| ⊗ₜ[ℂ] |ψ⟩⟨ψ| is a tensor product type. How do I convert it to a matrix to access the entries?

Any help is appreciated.

import data.real.basic
import data.complex.basic
import data.matrix.basic
import data.matrix.notation
import linear_algebra.tensor_product

open tensor_product

/-
1) definition 'rho' is noncomputable, it depends on 'complex.field'
-/
def rho : matrix (fin 2) (fin 2) ℂ :=
![![1/2, 0], ![0, 1/2]]

def psi : matrix (fin 2) (fin 1) ℂ :=
![![1], ![0]]

notation |ψ⟩ := psi
notation |ψ⟩⟨ψ| := psi.mul psi.transpose

/-
2) function expected at
|ψ⟩.mul |ψ⟩.transpose ⊗ₜ[ℂ] |ψ⟩.mul |ψ⟩.transpose
term has type
quot setoid.r
-/

/-
don't know how to synthesize placeholder
context:
⊢ Sort ?
-/
#eval (|ψ⟩⟨ψ| ⊗ₜ[ℂ] |ψ⟩⟨ψ|) 0 0


#### Alex J. Best (Jul 09 2020 at 23:45):

The first error is just lean telling you it can't compute with the definition you made, probably this doesn't matter at all to you, you can put noncomputable theory after your imports to tell lean not to bother you about this. Alternatively you can put noncomputable def instead every time this happens.

#### Alex J. Best (Jul 09 2020 at 23:47):

The reason it happens for 1/2 and not 1 is that 1/2 is 1 divided by 2, so it involves division in the field which lean can't compute for an arbitrary field.

#### Bassem Safieldeen (Jul 09 2020 at 23:58):

The problem persists if I use 0.5 and (0.5 : ℂ) :)

Why is 1 ok and 0.5 not? Both are equally valid complex numbers that have the right to be in my matrix of complex numbers.

#### Alex J. Best (Jul 09 2020 at 23:58):

0.5 is defined to be 1/2 in lean, or rather 5/10 which is the same!

#### Alex J. Best (Jul 09 2020 at 23:59):

They're fine complex numbers in lean, they just aren't computable, which like I said is a distinction that likely doesn't matter to you.

#### Alex J. Best (Jul 09 2020 at 23:59):

Many files begin with noncomputable theory its not a bad thing at all.

#### Alex J. Best (Jul 10 2020 at 00:00):

If you put that then lean will happily accept your definition.

#### Bassem Safieldeen (Jul 10 2020 at 00:01):

Yes, I have tried that. But accessing the matrix throws an error, still.

#### Alex J. Best (Jul 10 2020 at 00:01):

For 2 I guess you want that matrix n n R ⊗ matrix m m R is equivalent to matrix (n × m) (n × m) R which I don't think we have in mathlib, but wouldn't be too hard to define, really this would be a choice of such an isomorphism.

#### Alex J. Best (Jul 10 2020 at 00:03):

We do have def matrix_equiv_tensor : matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R) so you can use that to obtain a matrix n n (matrix m m R) whose entries you can access quite easily.

#### Bassem Safieldeen (Jul 10 2020 at 00:06):

Will give it a try. Thank you.

#### Alex J. Best (Jul 10 2020 at 00:09):

I tried it and hit a problem I'm unsure how to fix

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
inferred
ring.to_add_comm_group (matrix (fin 2) (fin 2) ℂ)


these typeclass problems are above my pay-grade lol

import data.real.basic
import data.complex.basic
import data.matrix.basic
import data.matrix.notation
import linear_algebra.tensor_product
import ring_theory.matrix_algebra

open tensor_product
noncomputable theory
/-
1) definition 'rho' is noncomputable, it depends on 'complex.field'
-/
def rho : matrix (fin 2) (fin 2) ℂ :=
![![1/2, 0], ![0, 1/2]]

def psi : matrix (fin 2) (fin 1) ℂ :=
![![1], ![0]]

notation |ψ⟩ := psi
notation |ψ⟩⟨ψ| := psi.mul psi.transpose

/-
2) function expected at
|ψ⟩.mul |ψ⟩.transpose ⊗ₜ[ℂ] |ψ⟩.mul |ψ⟩.transpose
term has type
quot setoid.r
-/

/-
don't know how to synthesize placeholder
context:
⊢ Sort ?
-/
#check (|ψ⟩⟨ψ| ⊗ₜ[ℂ] |ψ⟩⟨ψ|)
#check (matrix_equiv_tensor ℂ (matrix (fin 2) (fin 2) ℂ) (fin 2)).symm (|ψ⟩⟨ψ| ⊗ₜ[ℂ] |ψ⟩⟨ψ|)


#### Alex J. Best (Jul 10 2020 at 00:51):

Oh I think the problem is that matrix_equiv_tensor wants everything to be a commutative ring, rather than just a ring, so you might still have to define your own equivalence between the tensor product of matrix algebras and one big matrix algebra to access entries like that.

#### Scott Morrison (Jul 10 2020 at 00:54):

Yeah, I think I discovered the same problem:

import data.complex.basic
import data.matrix.basic
import ring_theory.matrix_algebra

open tensor_product
open_locale tensor_product

noncomputable theory

@[derive [fintype, decidable_eq]]
def n := fin 2

def foo : (matrix n n ℂ) ⊗ (matrix n n ℂ) ≃ₐ[ℂ] matrix n n (matrix n n ℂ) :=
(matrix_equiv_tensor ℂ (matrix n n ℂ) n).symm


#### Scott Morrison (Jul 10 2020 at 00:55):

says

failed to synthesize type class instance for
⊢ algebra ℂ (matrix n n (matrix n n ℂ))


#### Scott Morrison (Jul 10 2020 at 01:18):

The commutativity requirement on the algebra in matrix_equiv_tensor has been dropped in #3351.

#### Scott Morrison (Jul 10 2020 at 01:19):

And @Alex J. Best's suggestion of #check (matrix_equiv_tensor ℂ (matrix (fin 2) (fin 2) ℂ) (fin 2)).symm (|ψ⟩⟨ψ| ⊗ₜ[ℂ] |ψ⟩⟨ψ|) now works as a result!

#### Alex J. Best (Jul 10 2020 at 01:24):

Oh amazing, thanks Scott!

Last updated: May 09 2021 at 11:09 UTC