Tensor products indexed by a set

Stream: mathlib4

[Dagur Asgeirsson]

I'm reviewing #32608 and it made me wonder if we want specialized API for tensor products indexed by sets, i.e. a definition Set.TensorProduct which is the restriction of a PiTensorProduct to a set of the indexing type. Currently this PR uses PiTensorProducts with sets coerced to types as indexing types.

I'll mark this PR as awaiting-zulip until we've had some input from regular users of tensor products here.

[Kevin Buzzard]

Can you explain mathematically what you're talking about? I don't quite follow yet.

I don't really see why we ever need infinite tensor products and as far as I can see they are completely pathological objects. For example a countably infinite tensor product of $\R$'s over $\R$ is uncountably-infinite-dimensional as far as I can see (and in particular not one-dimensional, despite the fact that an infinite product of 1's is 1). I totally understand why we need restricted tensor products but we could define these as direct limits of finite tensor products.

[Kevin Buzzard]

We have restricted products (a bunch of stuff in mathlib and a ton more stuff in FLT) and these are constructed set-theoretically as a subset of a product rather than a direct limit, but we can't do the same thing for restricted tensor products because if one summand isn't flat then the maps aren't going to be injective.

[Dagur Asgeirsson]

Oh, what I'm talking about is completely non-mathematical. I'm not commenting on anything related to infinite tensor products. This PR has things like:

variable {S₁ S₂ : Set ι} (H : Disjoint S₁ S₂) [(i : ι) → Decidable (i ∈ S₁)]

/-- Tensors indexed by a set `S₁` times tensors indexed by a disjoint set `S₂`
are isomorphic to tensors indexed by the union `S₁ ∪ S₂`. -/
def tmulUnionEquiv :
    ((⨂[R] (i₁ : S₁), s i₁) ⊗[R] (⨂[R] (i₂ : S₂), s i₂)) ≃ₗ[R] ⨂[R] (i : ↥(S₁ ∪ S₂)), s i :=
  (tmulEquivDep R (fun i ↦ s ((Equiv.Set.union H).symm i))) ≪≫ₗ
  (reindex R (fun i : ↥(S₁ ∪ S₂) ↦ s i) (Equiv.Set.union H)).symm

and what I'm asking is, should we have something like Set.TensorProduct which would just be defined as ⨂[R] (i : S), s i, where S : Set ι, possibly with notation like ⨂[R] i ∈ S, s i, or are we fine with coercing Sets to indexing types like this PR does?

[Yaël Dillies]

I think we're fine with coercing?

[Eric Wieser]

I'm a little hesitant to add API like

def univEquiv : (⨂[R] i, s i) ≃ₗ[R] ⨂[R] i : ↥univ, s i.val :=
  reindex R s (Equiv.Set.univ ι).symm

which is a special case of reindex. I guess the argument is that you need the def to avoid ending up with Equiv.Set.univ _ on the RHS of the type?

[Kevin Buzzard]

I see. We have Set.pi which uses the underlying Pi type in its construction and I was just scared that you wanted to use the underlying big tensor product in the construction of Set.TensorProduct

[David Gross]

Author here. Let me chime in.

[David Gross]

Thanks, Dagur, for reviewing this.

Our prime motivation is to define "restricted tensor products", as mentioned by Kevin. We described the bigger goals here.

The PR lays the foundation for that. There's a stub with a working definition (in fact, a couple, this is still experimental) based on the PR.

[David Gross]

The PR does go a bit beyond what's strictly needed for restricted TPs. That's partly because there is a TBD item in PiTensorProduct.lean:

---

• API for the various ways ι can be split into subsets; connect this with the binary
  tensor product.

---

[David Gross]

I understand it was placed there by @Frédéric Dupuis.

[Kevin Buzzard]

Re the stub:

Given a family of modules s : ι → Type*, each with a distinguished element
(s₀ i) : s i, the _support_ of a tensor t : ⨂ i, s i is the set of indices
i : ι where t differs from s₀ i. (More precisely: the smallest set S such
that t is of the form tₛ ⊗ (⨂ₜ i : Sᶜ, s₀ i) with tₛ : ⨂ i : S, s i).

I don't think this makes sense. For example $1\otimes37=37\otimes1$ in $\R\otimes_{\R}\R$ (with the factors indexed by $\{1,2\}$) so $S=\{1\}$ or $S=\{2\}$ both work if $s_0=1$ for both copies of $\R$, but $S$ empty doesn't and there is no smallest $S$.

[David Gross]

Kevin Buzzard said:

Re the stub:
I don't think this makes sense. For example $1\otimes2=2\otimes1$ in $\R\otimes_{\R}\R$ (indexed by $\{1,2\}$) so $S=\{1\}$ or $S=\{2\}$ both work if $s_0=1$, but $S$ empty doesn't and there is no smallest $S$.

OK, thanks.

(That was my attempt to explain the structure in a concise way. We don't formalize "support" in the file).

[Kevin Buzzard]

Tensor products are really weird objects because a general element of a tensor product has no "canonical form". This makes it very difficult to talk about exactly "where" an element of the tensor product is supported. My idea for how restricted tensor products should be formalized is that you first formalize finite tensor products (done), and then set up a docs#DirectedSystem indexed by Finset ι with the transition maps sending the extra indices all to $s_0$, and then take the docs#DirectLimit . Then a general theorem will tell you that an arbitrary element comes from something at a finite level but it won't give you a "canonical" level.

[David Gross]

Kevin Buzzard said:

My idea for how restricted tensor products should be formalized is that you first formalize finite tensor products (done), and then set up a docs#DirectedSystem indexed by Finset ι with the transition maps sending the extra indices all to $s_0$, and then take the docs#DirectLimit .

Indeed. That's what we're doing.

[David Gross]

There are other reasons for why a "Set API" to tensor indices makes sense.

A simple example: If S : Set ι and L is a linear map defined on ⨂ i : S, E i, then it naturally induces a linear map L' on ⨂ i : ι, E i (by linear extension from pure tensors, where L' acts trivially on factors whose indices lie outside of S).

(That's a standard definition in quantum mechanics. Here, the index type labels "distinguishable degrees of freedom". The linear map L' models a physical operation which only affects the d.o.f.'s in S.)

For what it's worth: The above definition is included in the PR. There's a follow-up PR which includes the analogous construction for a finite family of disjoint sets. And once the restricted tensor product is done, we can extend it to infinite families of disjoint sets. The latter is used e.g. in the definition of quantum cellular automata and certain renormalization procedures in quantum many-body theory.

So I feel like the original "TBD item" asking for a Set API to tensor products is well-motivated!

A different question is whether we got the design decisions right. This is our first PR that's more than just a few lines. So any feedback is extremely welcome!

[Kevin Buzzard]

Again I can't make sense of this. What does "L' acts trivially on factors whose indices lie outside of S" mean? The infinite tensor product is a pathological object. But I don't understand you even if you're talking about the restricted tensor product.

[David Gross]

Kevin Buzzard said:

What does "L' acts trivially on factors whose indices lie outside of S" mean?

I just mean this: If $E_i$ is a family of vector spaces for $i : \iota$, and if L is a linear map on $\bigotimes_{i : S} E_i$, then L' is the linear map on $\bigotimes_{i : \iota} E_i$ which acts as

$$L' \, \bigotimes_{i : \iota} v_i := \big(L\bigotimes_{i : S} v_i\big)\otimes \big(\bigotimes_{i : S^c} v_i\big)$$

for any family $v_i \in E_i$.

This makes sense for any $\iota$ (finite or infinite) and also generalizes to the restricted tensor product (though the latter isn't part of this first PR yet).

[David Gross]

Kevin Buzzard said:

Tensor products are really weird objects because a general element of a tensor product has no "canonical form". This makes it very difficult to talk about exactly "where" an element of the tensor product is supported.

I guess the right way of defining the "support" of an element x in the restricted tensor product would be as the intersection of all sets S such that x lies in the image of ⨂ i : S, E i. In your example, this would give the empty set, as it should.

[Frédéric Dupuis]

I think we definitely need API for these kinds of manipulations! It's very common (at least in quantum information) to take a map on some subset of the tensor factors, and extend it to the full space by tensoring it with the identity everywhere else as in the $L'$ example above.

[Kevin Buzzard]

David Gross said:

I just mean this:

OK so my revised question is "what do you mean by "a linear map on $X$"? I am still a bit lost. For me a linear map has both a source and a target, and you're only specifying the source.

[Paradoxy]

Eric Wieser said:

I'm a little hesitant to add API like

def univEquiv : (⨂[R] i, s i) ≃ₗ[R] ⨂[R] i : ↥univ, s i.val :=
  reindex R s (Equiv.Set.univ ι).symm

which is a special case of reindex. I guess the argument is that you need the def to avoid ending up with Equiv.Set.univ _ on the RHS of the type?

Yes. Set API only works on tensors indexed by Sets coerced into a Subtype (in some cases it also works on Finsets, but that is another discussion). Now, what if we want to use this API on a tensor that is not initially indexed by a Set, but an arbitrary type? univEquiv makes this possible.

[Kevin Buzzard]

It seems to me that a "linear map on $X$" might just mean what I would call "a linear map from $X$ to $X$" in which case you're just extending by tensoring with the identity function (and imagining the arbitrary tensor product as being a binary tensor product over two disjoint index sets).

[Paradoxy]

Kevin Buzzard said:

David Gross said:

I just mean this:

OK so my revised question is "what do you mean by "a linear map on $X$"? I am still a bit lost. For me a linear map has both a source and a target, and you're only specifying the source.

Sorry for jumping in, but how does the target of LinearMap become relevant?

In the current PR, we have provided three extensions:

/-- For sets `S ⊆ T`, tensors indexed by `S` times tensors indexed by `T \ S`
are isomorphic to tensors indexed by `T`. -/
def tmulUnifyEquiv :
    (⨂[R] i₁ : S, s i₁) ⊗[R] (⨂[R] i₂ : ↥(T \ S), s i₂) ≃ₗ[R] ⨂[R] i : T, s i :=
  (tmulUnionEquiv (disjoint_sdiff_right)) ≪≫ₗ
    (reindex R (fun i : ↥(S ∪ T \ S) ↦ s i) (Equiv.subtypeEquivProp (union_diff_cancel hsub)))

def extendLinearHom : ((⨂[R] i : S, s i) →ₗ[R] M) →ₗ[R]
    (⨂[R] i : T, s i) →ₗ[R] (M ⊗[R] (⨂[R] (i₂ : ↑(T \ S)), s i₂)) :=
  let TmS := ⨂[R] (i : ↑(T \ S)), s i
  ((tmulUnifyEquiv hsub).congrLeft (M:=M ⊗[R] TmS) R).toLinearMap ∘ₗ LinearMap.rTensorHom TmS

def extendEnd : End R (⨂[R] i : S, s i) →ₗ[R] End R (⨂[R] i : T, s i) :=
  (tmulUnifyEquiv hsub).congrRight.toLinearMap ∘ₗ extendLinearHom hsub

def extendFunctional :
    ((⨂[R] i : S, s i) →ₗ[R] R) →ₗ[R] (⨂[R] i : T, s i) →ₗ[R] ⨂[R] (i₂ : ↑(T \ S)), s i₂ :=
  (TensorProduct.lid R _).congrRight.toLinearMap ∘ₗ (extendLinearHom hsub)

Where we have assumed $S \subseteq T$. In @David Gross 's example, T will be taken as Set.univ in these extensions. As you can see, in the extendLinearHom the target is assumed to be some arbitrary module, so it doesn't have to be an endomorphism. The way this works is by padding the linear map with identity by LinearMap.rTensorHom and re-interpreting the binary tensor product in the domain through tmulUnifyEquiv as a single tensor. In the case of extendEnd we can also re-interpret the target as a single tensor through tmulUnifyEquiv as well.

[Kevin Buzzard]

Sure, in which case you're just saying "you can tensor an arbitrary linear map with the identity map" which is indeed true

[David Gross]

Kevin Buzzard said:

Sure, in which case you're just saying "you can tensor an arbitrary linear map with the identity map" which is indeed true

Yes, indeed. Mathematically, everything in this PR is obvious. What it does is providing an API for manipulations like this one:

Kevin Buzzard said:

(and imagining the arbitrary tensor product as being a binary tensor product over two disjoint index sets).

...which is what we use in the definition of the restricted tensor product, and which is also what the existing TBD item calls for: "API for the various ways ι can be split into subsets; connect this with the binary tensor product".

[Eric Wieser]

Frédéric Dupuis said:

I think we definitely need API for these kinds of manipulations!

I'm somewhat skeptical of this, as I discuss on github. What is it that means we need things like:

def PiTensorProduct.singletonSetEquiv (i₀ : ι) : (⨂[R] i : ({i₀} : Set ι), M i) ≃ₗ[R] M i₀

yet have survived just fine without any of the following?

-- use `Equiv.funUnique` instead
def Function.singletonSetEquiv (i₀ : ι) : (({i₀} : Set ι) → M) ≃ M
-- use `Equiv.piUnique` instead
def Pi.singletonSetEquiv (i₀ : ι) : (Π i : ({i₀} : Set ι), M i) ≃ M i₀
-- use `Equiv.finsuppUnique` instead
def Finsupp.singletonSetEquiv (i₀ : ι) : (({i₀} : Set ι) →₀ M) ≃ M
def DFinsupp.singletonSetEquiv (i₀ : ι) : (Π₀ i : ({i₀} : Set ι), M i) ≃ M₀ i₀
def DirectSum.singletonSetEquiv (i₀ : ι) : (⨁ i : ({i₀} : Set ι), M i) ≃ M i₀

[David Gross]

Eric, thanks for the review.

We’re new to this ecosystem. So other people are better positioned to decide whether the benefits outweigh the costs, or whether the level of detail we have picked is appropriate.

Maybe I can still raise two points.

First, I think that these manipulations will appear in the library in some form sooner rather than later.

Indeed, our main interest currently is to implement restricted tensor products. The obvious way to do this (as shown in our stub, and also suggested by Kevin) is to set up a directed system with components given by the tensors indexed by finite subsets of a global index type.

This already requires some rudimentary form of “Set API”.

More elaborate manipulations of index sets appear pretty early in the mathematical treatment of the theory. As an example, consider the “associativity property”, given at the bottom of page 5 of the linked reference.

Second point: What breaks the symmetry between tensor products and, say, direct sums?

I guess my perception here is colored by quantum physics. There, tensor factors play a distinguished role (modelling physical degrees of freedom). A “calculus of tensor indices” lies at the heart of, e.g., entanglement theory, quantum circuits, cellular automata, some renormalization schemes, …

Empirically, as a quantum physicist, I find myself grouping tensor factors every day in a way that just doesn’t come up for the other cases. So, I guess, there's a least one relevant area of mathematics where this use case is special.

Of course, that’s not to say that our approach hits the appropriate language / level of detail.

[Frédéric Dupuis]

Just to elaborate a bit on David's post and give a somewhat more concrete example: it's very common in quantum information theory to have, say, a quantum state $ρ$ on tensor factors $A^n$ (so a linear map from ⨂[ℂ] i : Fin n, A to itself) and then view it as being on (⨂[ℂ] i : Fin (n / 2), A) ⊗ (⨂[ℂ] i : Fin (n / 2), A) in order to apply a theorem that applies to bipartite systems. And of course more complex manipulations like this happen all the time as well. These manipulations arise in "paper math" in a way that it doesn't for functions in my experience.

[Eric Wieser]

@Frédéric Dupuis, note that that example you give doesn't actually use set indices. My hesitation is not about decomposition, but rather about adding special cases for sets rather than stopping at the generality of docs#PiTensorProduct.tmulEquivDep, docs#PiTensorProduct.subsingletonEquiv, and docs#PiTensorProduct.reindex

[Paradoxy]

(deleted)