Basis of a PiTensorProduct

Stream: mathlib4

[Alex Meiburg]

I'm trying to convert between a PiTensorProduct.map and a Matrix on an appropriate basis. There is https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/TensorProduct/Basis.html#Basis.tensorProduct and indeed all of https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/TensorProduct/Matrix.html to make this workable for normal TensorProducts, but I can't find anything corresponding for PiTensorProducts...

[Kevin Buzzard]

Can you post a #mwe ?

[Alex Meiburg]

Best mwe I can come up with:

import Mathlib.LinearAlgebra.PiTensorProduct
import Mathlib.LinearAlgebra.TensorProduct.Matrix

abbrev MatrixMap (A B R : Type*) [Semiring R] := Matrix A A R →ₗ[R] Matrix B B R

variable {R : Type*} [CommSemiring R]
variable {ι : Type u} [DecidableEq ι] [fι : Fintype ι]
variable {dI : ι → Type v} [∀(i :ι), Fintype (dI i)] [∀(i :ι), DecidableEq (dI i)]
variable {dO : ι → Type w} [∀(i :ι), Fintype (dO i)] [∀(i :ι), DecidableEq (dO i)]

/-- Kronecker product of multiple MatrixMaps-/
noncomputable def PiKron (Λi : ∀ i, MatrixMap (dI i) (dO i) R) : MatrixMap (∀ i, dI i) (∀ i, dO i) R :=
  let map1 := PiTensorProduct.map Λi;
  --map1 is now a LinearMap from `PiTensorProduct R fun i ↦ Matrix (dI i) (dI i) R`
  -- to `PiTensorProduct R fun i ↦ Matrix (dO i) (dO i) R`.
  --I want to, presumably through `LinearMap.toMatrix` and maybe `Matrix.reindex`, to get out
  --LinearMap from `Matrix (∀ i, dI i) (∀ i, dI i) R` to `Matrix (∀ i, dO i) (∀ i, dO i) R`
  sorry

Is there a sensible way to go about expressing this? Or do I essentially have to prove that a pi-product of Basis is a Basis for the resulting space, and do all the PiTensorProduct.lifting and so on myself? It's not an API I understand very well unfortunately so I'd rather not

[Alex Meiburg]

Here's the corresponding definition for a (non-Pi) TensorProduct, which I do have written down. (It is quite ugly, and if there's a better way to do this I'm all ears)

variable {A B C D R : Type*} [Fintype A] [Fintype B] [Fintype C] [Fintype D]
variable [DecidableEq A] [DecidableEq C]

/-- The Kronecker product of MatrixMaps. Defined here using `TensorProduct.map M₁ M₂`, with appropriate
reindexing operations and `LinearMap.toMatrix`/`Matrix.toLin`. Notation `⊗ₖₘ`. -/
noncomputable def kron [CommSemiring R] (M₁ : MatrixMap A B R) (M₂ : MatrixMap C D R) : MatrixMap (A × C) (B × D) R :=
  let h₁ := (LinearMap.toMatrix (Basis.tensorProduct (Matrix.stdBasis R A A) (Matrix.stdBasis R C C))
      (Basis.tensorProduct (Matrix.stdBasis R B B) (Matrix.stdBasis R D D)))
    (TensorProduct.map M₁ M₂);
  let r₁ := Equiv.prodProdProdComm B B D D;
  let r₂ := Equiv.prodProdProdComm A A C C;
  let h₂ := Matrix.reindex r₁ r₂ h₁;
  Matrix.toLin (Matrix.stdBasis R (A × C) (A × C)) (Matrix.stdBasis R (B × D) (B × D)) h₂

scoped[MatrixMap] infixl:100 " ⊗ₖₘ " => MatrixMap.kron

[Eric Wieser]

Is this a suitable mwe for your original question?

import Mathlib

variable {ι} {κ : ι → Type*} {R} {M : ι → Type*} [CommSemiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]

open scoped TensorProduct

noncomputable def finsuppPiTensor : (⨂[R] i, κ i →₀ M i) ≃ₗ[R] ((∀ i, κ i) →₀ (⨂[R] i, M i)) :=
  LinearEquiv.ofLinear
    (PiTensorProduct.lift sorry)
    (sorry)
    sorry
    sorry

noncomputable def Basis.piTensorProduct (b : ∀ i, Basis (κ i) R (M i)) :
    Basis (∀ i, κ i) R (⨂[R] i, M i) := by
  refine Finsupp.basisSingleOne.map <| ?_ ≪≫ₗ PiTensorProduct.congr fun i => (b i).repr.symm
  refine ?_ ≪≫ₗ (finsuppPiTensor (R := R) (κ := κ) (M := fun _ => R)).symm
  refine Finsupp.lcongr (Equiv.refl _) ?_
  apply LinearEquiv.symm
  sorry -- easy

[Alex Meiburg]

Yes, I actually just ended up writing something pretty much identical that about 1 minute ago, haha :)

[Eric Wieser]

(edited above)

[Eric Wieser]

Then you'll want to write docs#finsuppTensorFinsupp for PiTensorProduct (edited above)

[Kevin Buzzard]

Is this true? I've never seen infinite tensor products before -- why do we even have them? What are they used for? I've just been staring at the definition. If we have a countably infinite tensor product of $R^2$ s with basis $e_i,f_i$ for $i=1,2,3,...$ then how are you going to express $(e_1+f_1)\otimes(e_2+f_2)\otimes\cdots$ as a finite linear combination of the proposed basis?

[Kevin Buzzard]

The thing I've seen before is restricted tensor products, where you fix an element $m_i\in M_i$ for all $i$ and then only allow infinite tensors $e_1\otimes e_2\otimes\cdots$ for which all but finitely many of the $e_i$ are equal to $m_i$.

[Eric Wieser]

I don't think PiTensorProduct lets you have countably infinite no

Eric Wieser said:

Then you'll want to write docs#finsuppTensorFinsupp for PiTensorProduct

Note that the TensorProduct version is hardly simple!

[Kevin Buzzard]

I don't understand -- I don't see any finiteness hypothesis on iota.

[Eric Wieser]

My proposal is to push through copying the binary argument, and add that assumption when/if you find you need it

[Alex Meiburg]

Ah yes, I guess (at least for what I'm trying to write) I'm only interested in finite iota.

For infinite tensor products, the natural pi-type index does not produce a basis. If you start with a _Hilbert_ basis for _Hilbert_ spaces, then the infinite tensor product (with the natural pi-type index) does produce a new _Hilbert_ basis. This is very important in physics. But in physics, everyone uses "basis" interchangeably with "Hilbert basis", and always assumes that all vector spaces are Hilbert spaces :)

[Eric Wieser]

I think there's a similar problem with MultiLinearMap which while defined on infinite-arity functions, they are actually only non-zero when the index set is finite.

[Kevin Buzzard]

I very much doubt that an infinite tensor product of Hilbert spaces is a Hilbert space or even a normed space. How would you put a norm on an infinite tensor product of vectors all of which have norm 37 for example?

I am yet to see a use for this construction in the case when iota is infinite.

[Alex Meiburg]

It is not equivalent (as a vector space) to the standard infinite tensor product of vector spaces. But "infinite tensor product of Hilbert spaces" is indeed common enough that there are two competing definitions for it, depending on usage. The more common one is infinite tensor product with finite support. See e.g. https://mathoverflow.net/a/161209

[Kevin Buzzard]

Right -- I can certainly believe that there's a sensible definition of an infinite tensor product of Hilbert spaces! My point is just that it isn't the thing in mathlib and more generally I've never seen the thing in mathlib before.

[Kevin Buzzard]

Eric Wieser said:

I think there's a similar problem with MultiLinearMap which while defined on infinite-arity functions, they are actually only non-zero when the index set is finite.

Surely the canonical multilinear map from the infinite product to this wacky infinite tensor product is nonzero when the index set is infinite?

As a consequence of this I realise that I don't even know what $\R\otimes\R\otimes\R\otimes\cdots$ is (tensoring over $\R$). It's definitely bigger than $\R$ because you can't multiply $1\otimes 1\otimes 1\otimes\cdots$ by a real number to get $2\otimes 2\otimes 2\otimes\cdots$.

[Kevin Buzzard]

In contrast, the restricted tensor product (the one I've seen before) of infinitely many $\R$ s is just $\R$ again.

I find it pretty weird that this seemingly very natural generalisation of tensor product to the infinite case is something I've never seen before and I wonder if it's just a completely pathological object in all nontrivial cases.

[Adam Topaz]

The usual way to do this is to take some colimit over the finite tensor products.

[Adam Topaz]

But this is different from mathlib's PiTensorProduct

[Adam Topaz]

What's the universal property of PiTensorProduct?

[Adam Topaz]

Oh I see it's PiTensorProduct.lift

[Kevin Buzzard]

So to take that colimit you need to specify maps at finite level and this will involve choosing an element of each module. This will then become what I called the restricted tensor product above. But it occurs to me now that instead of taking the colimit you can just look at the submodule of this monstrosity generated by the finite tensor products so there's a use case for PiTensorProduct. It reminds me of how we've constructed the finite adeles as a subspace of a pathological object (the infinite product of the completions of the global field).

[Paradoxy]

@Eric Wieser , @Alex Meiburg I had a look at https://github.com/leanprover-community/mathlib4/pull/11156/files, and the proposed basis actually works. i.e

noncomputable def Basis.piTensorProduct (b : Π i, Basis (κ i) R (V i)) :
  Basis (Π i, κ i) R (⨂[R] i, V i) :=
  Finsupp.basisSingleOne.map
    ((PiTensorProduct.congr (fun i ↦ (b i).repr)).trans <|
        finsuppPiTensorProduct.trans <|
          Finsupp.lcongr (Equiv.refl _) (constantBaseRingEquiv _ R).toLinearEquiv).symm

However, it relies on finsuppPiTensorProduct from another pull request here https://github.com/leanprover-community/mathlib4/pull/11155, which in turn needs PiTensorProduct.directSum from https://github.com/leanprover-community/mathlib4/blob/707c205109434190c27ed585164731ce262918cc/Mathlib/LinearAlgebra/DirectSum/PiTensorProduct.lean that no longer exists. PiTensorProduct.directSum is proved by PiTensorProduct.dfinsupp, existing in "https://github.com/leanprover-community/mathlib4/blob/707c205109434190c27ed585164731ce262918cc/Mathlib/LinearAlgebra/DFinsupp/PiTensorProduct.lean". Since we do not have PiTensorProduct.dfinsupp either, I checked MultilinearMap.fromDFinsuppEquiv in LinearAlgebra/Multilinear/DFinsupp, as expected, it did not exist, attempting the previously proposed proof for MultilinearMap.fromDFinsuppEquiv gives the following error:

failed to synthesize
Module R ((p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) N)

Which means either the instance corresponding to this Module is removed, or it is relocated. Any idea how to trace back the location of this instance?

[Kevin Buzzard]

PiTensorProduct.directSum never existed in master (as opposed to "no longer exists"), it was proposed in #11155 which never got merged. The PR is tagged "please-adopt" so maybe a place to start is to get that PR over the line or to cherry-pick the parts which you need?

[Eric Wieser]

docs#PiTensorProduct does exist, so I guess you mean something else?

[Eric Wieser]

#25141 was my latest attempt at spinning things off #11155, but I haven't yet had time to re-evaluate where I got to.

[Kevin Buzzard]

Sorry, edited, it's PiTensorProduct.directSum which I'm claiming never existed (and mathlib-changelog.org agrees with me)

[Joël Riou]

I have been refactoring Sophie's PR. First, in #26464, I show that the pi tensor product is finitely generated under suitable assumptions, in #26465 I will construct a presentation of it, and from that it will be easy (#26467) to obtain a basis of the pi tensor product from a (finite) family of bases.