Tensor product of matrices

Stream: maths

[Bassem Safieldeen]

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]

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]

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]

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]

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

[Alex J. Best]

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]

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

[Alex J. Best]

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

[Bassem Safieldeen]

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

[Alex J. Best]

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]

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]

Will give it a try. Thank you.

[Alex J. Best]

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]

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]

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]

says

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

[Scott Morrison]

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

[Scott Morrison]

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]

Oh amazing, thanks Scott!