Zulip Chat Archive

Stream: maths

Topic: Tensor product of matrices


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Jul 09 2020 at 23:59):

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

view this post on Zulip Alex J. Best (Jul 10 2020 at 00:00):

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

view this post on Zulip Bassem Safieldeen (Jul 10 2020 at 00:01):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bassem Safieldeen (Jul 10 2020 at 00:06):

Will give it a try. Thank you.

view this post on Zulip 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 (|ψ⟩⟨ψ| ⊗ₜ[] |ψ⟩⟨ψ|)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 10 2020 at 00:55):

says

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

view this post on Zulip Scott Morrison (Jul 10 2020 at 01:18):

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

view this post on Zulip 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!

view this post on Zulip Alex J. Best (Jul 10 2020 at 01:24):

Oh amazing, thanks Scott!


Last updated: May 09 2021 at 11:09 UTC