Tensor product of bounded operators

Stream: new members

[Magalame]

Sorry, this might be a bit trivial but is there already a theorem in mathlib about how (X →L[ℂ] X) ⊗ (Y →L[ℂ] Y) = X ⊗ Y →L[ℂ] X ⊗ Y, with X,Y hilbert spaces?

[Kevin Buzzard]

So this is some kind of completed tensor product? I don't even know if we have that (but we might: I am not an expert in the analysis part of the library). As for the linear algebra part, of course the two sides are not "equal" in a formal sense, but here's the map in one direction:

import data.polynomial.algebra_map

open_locale tensor_product

example {R X Y: Type*} [comm_ring R] [add_comm_group X] [add_comm_group Y] [module R X]
  [module R Y] (f : X →ₗ[R] X) (g : Y →ₗ[R] Y) : (X ⊗[R] Y) →ₗ[R] X ⊗[R] Y := tensor_product.map f g

[Magalame]

you're absolutely right I should have specified that X and Y are also finite dimensional

[Eric Wieser]

It's not true in the reverse direction, is it? What do you do with the map that sends u ⊗ v to v ⊗ u?

[Junyan Xu]

docs#hom_tensor_hom_equiv combined with docs#linear_map.to_continuous_linear_map seem to settle the original question.

@Eric Wieser Both sides have the same dimension, and it's easy to see the forward map is surjective; if p_ij is the map sending e_i to e_j and other basis vectors to 0, then p_ij ⊗ p_kl is the map sending e_i ⊗ e_k to e_j ⊗ e_l and other basis vectors to 0, and these maps span the hom space. If X = Y, the map u ⊗ v ↦ v ⊗ u is given by ∑ij p_ij ⊗ p_ji.

[Heather Macbeth]

@Magalame We don't have the tensor product of Hilbert spaces, although thanks to ongoing work of @Anatole Dedecker this may change fairly soon.

[Magalame]

@Junyan Xu thanks a lot for the hint! I'm still a bit unfamiliar with mathlib

[Magalame]

@Heather Macbeth great to hear! I'll be looking out for that :)
is there an ETA yet?