Tensor products of inner product spaces

Stream: Is there code for X?

[Oliver Nash]

We don't yet have tensor products of inner product spaces, right?

[Frédéric Dupuis]

I don't think so.

[Oliver Nash]

OK thanks!

[Heather Macbeth]

@Anatole Dedecker was working on this this summer (via Hilbert-Schmidt operators).

[Oliver Nash]

Oh cool!

[Anatole Dedecker]

Unfortunately I haven't made a ton of progress on that because I need #15451, which still depends (transitively) on 4 PRs, and I still have a hope to find a way to make everything cleaner (read "basis-free") using a carefully chosen filter, but I should probably give up on that.

The other problem I have is that I'm not sure what would be needed to make the Hilbert-Schmidt construction actually usable as a tensor product. Wikipedia does give a universal property for the Hilbert tensor product but it involves weakly Hilbert Schmidt bilinear maps (which means a whole lot of API to add) and I don't think it will be super useful in practice. Another option is proving that we have the universal property of the completion of the algebraic tensor product, but that means defining the inner product on it, at which point it would be simpler to just define the Hilbert tensor product as a completion. So I think the only remaining option is to rely on the characterization by Hilbert bases, which is extremely unsatisfying...

[Oliver Nash]

Thanks Anatole, I'm really glad that you've put so much thought into this even if you're still not completely satisfied.

[Oliver Nash]

In the meantime, there's a much more basic, purely algebraic fact that is missing:

import analysis.inner_product_space.basic
import linear_algebra.tensor_product

open_locale tensor_product

variables {𝕜 E F : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F]

instance : inner_product_space 𝕜 (E ⊗[𝕜] F) := sorry -- missing

[Oliver Nash]

Of course this will only be useful in finite dimensions but finite dimensions also matter!

[Anatole Dedecker]

Actually providing this instance and proving basic things about it will be almost all the work necessary to define the full tensor product in the completion way, because we now know how to put an inner product on the completion of an inner product space. So if you think this is useful anyway (which it is, because finite dimensions) then maybe the completion way is the right way

[Oliver Nash]

I'm not sure I follow you. Isn't the tensor product that uses the topology going to construct a different space?

[Anatole Dedecker]

Yes it is, but it will be the completion of this one. So the question is basically, do we want to define it as "the" completion (i.e docs#uniform_completion), or as Hilbert-Schmidt operators and prove it is "a" completion (i.e docs#abstract_completion)

[Oliver Nash]

Oh I see.

[Oliver Nash]

I suppose we could always do both: we'll need to define a model one way or another (and maybe this could be docs#uniform_completion) but whatever we do we should probably prove that this is a docs#abstract_completion.

[Anatole Dedecker]

My point being that if we define the instance you're asking for then it doesn't cost much more to define it as a completion because we have docs#uniform_space.completion.inner_product_space

[Oliver Nash]

Right.

[Anatole Dedecker]

But on the other hand I remember @Heather Macbeth was in favor of the more concrete definition (in the way we don't use completions for talking about Hilbert sums, we use docs#pi_Lp with p = 2)

[Oliver Nash]

Well it's usually a good idea to follow Heather's ideas :-)

[Eric Wieser]

I had a brief go at the titular task here in lean 3 before re-finding this thread. I only did it for real inner product spaces because we don't have the sesquilinear version of docs#BilinForm.tmul. I'm not certain whether the sorry holds without choosing a basis.

[Oliver Nash]

I made a project for a Lean event that Kevin organised last September and it contains a construction of the inner product space structure on a tensor product. I think it was @Jujian Zhang who did most of the work. The instance is here: https://github.com/ocfnash/lean-shannon-lovasz/blob/e63e535599ffb3c2a7e995e1621847693dd68fab/src/to_mathlib/analysis/inner_product_space/tensor_product.lean#L404

[Eric Wieser]

Nice, that makes me feel justified in my laziness of sticking to real inner product spaces, and in my hunch that I couldn't avoid finite dimensionality

[Oliver Nash]

To be clear: the result does not need a finite-dimensionality assumption, and the instance I linked does not assume finite dimensionality.

The proof in that repo does bootstrap up from an argument using bases with a finite-dimensionality assumption. I'd guess there is a basis-free argument but I'm not sure.

[Eric Wieser]

I opened #6020 to track this