# Zulip Chat Archive

## 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
matrix.add_comm_group
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