rfc: tensor product notation

Stream: general

[Johan Commelin]

Tl;dr: I think the $\otimes$ in $x \otimes y$ will be used an order of magnitude more often than the one in $M \otimes N$. Hence I would like to swap the subscript ₜ from the former to the latter.

---

Longer story:
I'm planning a refactor of tensor products. Roughly speaking, I want to use a characteristic predicate instead of the explicit construction. This will allow us to treat $M$ as $R \otimes_R M$, or to treat $A[X]$ as $R[X] \otimes_R A$, etc...

As part of this, I'm proposing a has_tmul class, that will enable tensor product notation.

With this post, I want to ask whether people are happy with the following notation change.

Current situation:

-- tensor product of elements (terms)
x ⊗ₜ y
x ⊗ₜ[R] y

-- tensor product of modules (types)
M ⊗ N
M ⊗[R] N

My proposal:

-- tensor product of elements (terms)
x ⊗ y
x ⊗[R] y

-- tensor product of modules (types)
M ⊗ₜ N
M ⊗ₜ[R] N

I think that currently the subscript ₜ stands for terms, but it could just as well stand for types (or tmul or tensor). So as a mnemonic, it doesn't matter too much where it sits.

The reason I would like to change this, is that if we switch to the characteristic predicate, we will be talking a lot about tensor products of terms $x \otimes y$, but not so much about the explicit construction $M \otimes N$ of tensor products of modules. Instead, we will usually introduce an auxiliary module $T$ that satisfies the characteristic predicate, and hence is canonically isomorphic to $M \otimes N$.

[Kevin Buzzard]

Is it definitely not possible to overload the notation like we do in regular maths? (one works on types, one on terms...)

[Mario Carneiro]

those aren't exactly disjoint classes

[Mario Carneiro]

strictly speaking you could have a module whose elements are types

[Kevin Buzzard]

only in your crazed computer science theoretical model of how things might be

[Kevin Buzzard]

but I take your point

[Mario Carneiro]

The best you can say is that there are two functions and if you pick the wrong one a typeclass search will fail

[Mario Carneiro]

I don't know whether / to what extent typeclass search can be used for overload resolution

[Kevin Buzzard]

The way we dealt with | vs \| was to use two extremely similar unicode characters with different shortcuts. Can we pull this off here?

[Mario Carneiro]

sure, just smuggle a zero width space in somewhere

[Kevin Buzzard]

Basically the less it looks like normal maths, the less good it is, so in some sense this change is fine by me because it didn't look quite like normal maths before and it won't quite look like it afterwards, but if we could come up with a better idea where it looked like normal maths and people who are confused can get unconfused by hovering then this would be a solution which would be nicer as far as I'm concerned.

[Kevin Buzzard]

Is the zero width space suggestion a serious one? Can we make it so that \otimes gives the type one and \otimest gives the term one, for example?

[Kevin Buzzard]

wooah https://www.fileformat.info/info/unicode/char/26d2/index.htm

[Mario Carneiro]

I know it will be considered seriously by crazed mathematicians, I haven't decided how to feel about it yet

[Kevin Buzzard]

"road closed"

[Mario Carneiro]

lolol

[Mario Carneiro]

I'm pretty sure lean-liquid uses zero width spaces somewhere

[Mario Carneiro]

The zero-width space option (the unicode confusable option is similar) has the drawback that it is hostile to authors since they can't see the effect of a typo

[Kevin Buzzard]

wait there really are two unicode chars? https://www.fileformat.info/info/unicode/char/2a02/index.htm and https://www.fileformat.info/info/unicode/char/2297/index.htm ?

[Kevin Buzzard]

there's even https://www.fileformat.info/info/unicode/char/2b59/index.htm

[Kevin Buzzard]

The unicode confusable option is strictly better than the zero width space option, right? Because I can't make \otimest produce \otimes + zero_width_space presumably?

[Mario Carneiro]

you can

[Kevin Buzzard]

For me this is no less hostile than the issues we have with | vs \| (which I see when doing number theory with undergrads asking me why 2 divides 4 doesn't typecheck)

[Mario Carneiro]

I am very conflicted about the idea of using symbols that are documented to cause confusion for related but different purposes

[Mario Carneiro]

You are right that | vs \| is the same sort of thing

[Kyle Miller]

I'll add another proposal:

-- tensor product of elements (terms)
x ⊗ y
x ⊗[R] y

-- tensor product of modules (types)
M ⊠ N
M ⊠[R] N

(I know ⊠ can have some other meaning, though, as the tensor product over the tensor product of rings.)

[Kevin Buzzard]

Isn't this worse than using a different \otimes? Because now this is actually wrong, that symbol is some sort of external tensor product thing which I've never properly understood.

[Kyle Miller]

I've seen it used to mean normal tensor product (occasionally), so I'm not sure there's a standard meaning.

[Kevin Buzzard]

https://ncatlab.org/nlab/show/external%20tensor%20product

[Mario Carneiro]

is there a circled comma? That would be great

[Mario Carneiro]

❟ anyone?

[Kevin Buzzard]

maybe we should add it to the proposal for the unicode guys together with those missing subscript letters

[Mario Carneiro]

I think a comma-like operator makes a lot more sense for the tensor product of elements than an \otimes given the notational conventions elsewhere in lean

[Kyle Miller]

I wish there were a TRIANGLED TIMES to complement SQUARED TIMES, since it'd be a mnemonic that it's a tensor product with a diagonal action.

[Kevin Buzzard]

Could we use \Ox for types and \ox for terms? These are two of the characters I mentioned earlier. We have

/- This enables the notation `⨂[R] i : ι, s i` for the pi tensor product, given `s : ι → Type*`. -/
localized "notation `⨂[`:100 R `] ` binders `, ` r:(scoped:67 f, pi_tensor_product R f) := r"
  in tensor_product

and does that stop us also using it for M ⨂[R] N? Alternatively ⭙ is unused in mathlib and looks exactly the same as \ox in my font unless you zoom in super-close

[Yaël Dillies]

I like ⛒ because it looks quite enough like the tensor product, but is also a bit different if you look close enough.

[Kevin Buzzard]

I agree that (a,b) has type A \times B but unfortunately mathematicians are just going to get confused by specialised notation which is unrecognisable to them. I think the Johan's original "switch the _t" idea is better than a comma thing, even though I do understand the logic -- I think we should aim for readability for mathematicians above all else

[Kevin Buzzard]

Is it OK to use road closed symbols for uses other than their intended purpose?

[Mario Carneiro]

I don't think we intend to close any roads in mathlib

[Mario Carneiro]

so it's probably fine

[Mario Carneiro]

I'm pretty sure we are abusing tons of unicode symbols already

[Kyle Miller]

Ok, one more proposal:

-- tensor product of elements (terms)
x ⊠ y
x ⊠[R] y

-- tensor product of modules (types)
M ⊗ N
M ⊗[R] N

The justification is that (I think) there's a sense in which the external tensor product of terms is the usual tensor product of terms. If M is a module, you can think of it as a 0-category whose objects are the terms of M, and the exterior tensor product of a term of M and a term of N is a term of the tensor product of these two 0-categories.

[Kevin Buzzard]

If Johan is correct then this would mean that the weird-to-mathematicians symbol would be the prevalent one, which is not ideal.

[Kyle Miller]

I think using similar-looking (or invisible) unicode characters as a design is a sketchy hack -- it's important to be able to look at some Lean code and know what it means. Otherwise, how can we know that we've proved the theorems we intended to prove without going through with an editor checking each characters' Unicode codepoints?

| vs ∣ and ∑ vs Σ are bad enough, and I'm not looking forward to having more of it...

[Kyle Miller]

(My biases: "a little notation is nice for algebraic reasoning, but I'm a fan of Lisp and Scheme.")

[Kevin Buzzard]

On the one hand we have the very remote but I guess pretty serious possibility that someone tensors two types together using term-tensor by accident and there happened to be a module structure on Type u so it compiled and gave a super-super-hard to find bug or even worse a misleading result, and on the other hand we have the issue of making our theorem statements readable to mathematicians with no training.

[Kyle Miller]

It might be worth considering how any changes might interact with the monoidal product notation for monoidal categories: https://github.com/leanprover-community/mathlib/blob/6d2cbf9df602a9bd62cf82e7d8ed76b34f4b1e6e/src/category_theory/monoidal/category.lean#L127

[Reid Barton]

Yeah I'm not sure I would agree with the original claim. I think I'd say that in some contexts you exclusively use the tensor product of modules and in other contexts you mostly use the tensor product of elements.

[Reid Barton]

Unicode Character 'N-ARY CIRCLED TIMES OPERATOR' (U+2A02) should probably be used for the n-ary tensor product

[Reid Barton]

Nowadays it's become fashionable to write $\otimes$ for the smash product of spectra, where there aren't really elements at all.

[Reid Barton]

By the way, don't forget about ꕕ U+A555 VAI SYLLABLE KPAN or ⛒ U+26D2 CIRCLED CROSSING LANES.

[Eric Wieser]

Yes, note we have docs#pi_tensor_product which uses the n-ary symbol

[Johan Commelin]

Reid Barton said:

Yeah I'm not sure I would agree with the original claim. I think I'd say that in some contexts you exclusively use the tensor product of modules and in other contexts you mostly use the tensor product of elements.

My goal with the refactor is that in an unbundled situation, you should almost never mention the explicit construction. But if you are working in some bundled setup where you have a monoidal category, sure, then you'll take tensor products of objects.

Do you think that makes sense? Or do you think that also in the unbundled situation, the construction should be used a good number of times, instead of some module satisfying the characteristic "predicate".

[Kevin Buzzard]

If you prove things for is_tensor_product then you'll of course be able to deduce them for the concrete tensor product, and if schemes/localisation are anything to go by, there will be plenty of instances where mathematicians use a noncanonical tensor product (possibly without noticing) so I totally agree that you'll need it. Like you I feel like the terms will be more prevalent than the types, although actually of course the terms will be taking values now in the is_tensor_product type now I guess, which might cause some confusion...

[Scott Morrison]

I would be pretty unhappy about any zero-width spaces in mathlib.

[Scott Morrison]

I would love to just use the same symbol in both situations, if Lean can cope. (In the monoidal category development, there seems to have been no problem using the same symbol for tensor products of objects and of morphisms.)

[Scott Morrison]

Much as I appreciate the existence of symbols from Vai, Canadian Syllabics, etc, I wouldn't like using near-indistinguishable symbols. Primes or subscripts are not terrible.

[Mario Carneiro]

One way to make the same symbol work would be a notation typeclass

[Mario Carneiro]

import linear_algebra.tensor_product

class {u} has_tensor {α β} (a : α) (b : β) (γ : out_param (Type u)) : Type u :=
(val : γ)

def tensor {α β} (a : α) (b : β) {γ : Type*} [has_tensor a b γ] : γ := has_tensor.val a b
infix ` ⊗ `:100 := tensor

universes u v
variables (R : Type u) [comm_semiring R] (M N : Type v)
  [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N]

instance : has_tensor M N (Type v) := ⟨tensor_product R M N⟩

instance (x : M) (y : N) : has_tensor x y (M ⊗ N) := ⟨tensor_product.tmul R x y⟩

variables (x : M) (y : N)
#check M ⊗ N -- M ⊗ N : Type v
#check x ⊗ y -- x ⊗ y : M ⊗ N

[Kevin Buzzard]

Ooh

[Kevin Buzzard]

Would we also then be able to use x ⊗ y as a term of type T if is_tensor_product R M N T?

[Mario Carneiro]

The limitation of this approach is in the decision for γ to be an out_param or not. Either way there are going to be some pains because you can't use unification to infer R, like you would if you are literally using tensor_product or tensor_product.tmul. If the output type is some generic T, then it seems even harder to have it be an out_param, although it might work if there is something preventing the construction from coming up first

[Mario Carneiro]

Lean 4 would allow more flexibility to decouple the notation from the elaboration method and use domain specific tricks to distinguish the cases

[Kevin Buzzard]

I guess x ⊗[R] y and M ⊗[R] N would be acceptable to mathematicians

[Mario Carneiro]

Right now the [R] is optional

[Mario Carneiro]

actually in the version I just posted there is no support for the R

[Mario Carneiro]

class is_tensor_product (T : Type*) :=
(e : tensor_product R M N ≃ T) -- or something

instance foo (T) [is_tensor_product R M N T] : has_tensor M N Type* := ⟨T⟩
instance bla (T) [is_tensor_product R M N T] (x : M) (y : N) : has_tensor x y T :=
⟨is_tensor_product.e.1 (tensor_product.tmul R x y)⟩

universe w
variables (T : Type w) [is_tensor_product R M N T]
#check M ⊗ N -- M ⊗ N : Type w
#check (rfl : M ⊗ N = T)
#check x ⊗ y -- x ⊗ y : T

[Mario Carneiro]

TBF I don't think this is a good idea

[Johan Commelin]

Interesting idea!

[Johan Commelin]

We certainly need support for [R]. Because we want to be able to consider $\R \otimes_\Z \R$ and $\R \otimes_\R \R$. (Similarly for the termy versions.)

[Eric Wieser]

This seems similar to how we have A × B vs (a, b). I've seen comments in the past saying that Haskell uses the same notation for both but it is confusing.

[Eric Wieser]

How about (a, b)ₗ[R] since tensor_product is like a linear version of prod?

[Johan Commelin]

I think $\otimes_t$ is better, because it has so much more resemblance with current usage in informal maths.

[Eric Wieser]

Here's a circled comma, @Mario Carneiro: ⃝,

[Kevin Buzzard]

We can't do commas. This is not acceptable. Mathematicians will find the code unreadable, their first question will be why we're not using the standard symbol, and any answer of the form "we can't" will be met with a response of "ok I'll come back when you've figured it out"

[Kevin Buzzard]

One reason lean caught on in the maths community is its liberal use of the correct unicode symbols for many things

[Kevin Buzzard]

My impression is that the CS people really can't see what the fuss is about here but to mathematicians it seems to make a huge difference

[Eric Wieser]

Would mathematicians prefer a non-comma symbol for (a, b) : A × B too?

[Kevin Buzzard]

No, we use commas for that

[Kevin Buzzard]

What you write there is perfect

[Eric Wieser]

Ah, I'm misremembering, it's A × B that I've seen often written A ⊕ B in maths, not (a, b). (See the Wikipedia page on direct sums for instance)

[Johan Commelin]

Sure, $A \times B$ and $A \oplus B$ are used a lot, and quite often they are interchangeable.

[Eric Wieser]

Which is a shame because A ⊕ B is very different in Lean

[Kevin Buzzard]

Yes, and I'm sure you can guess which one I'd like to nuke

[Kevin Buzzard]

We have A ⨿ B for that

[Eric Wieser]

I hope you mean A ⊔ B

[Kevin Buzzard]

Sure, they look the same to me

[Kevin Buzzard]

With my mathematician's glasses on

[Eric Wieser]

I guess mathlib lost its "intended semantics of unicode characters" glasses long ago...

[Kevin Buzzard]

In human maths papers in this particular case I'm pretty sure that nobody would be particularly fussed about which disjoint union character to use, it's actually surprisingly rare as a construction (at least in number theory)

[Kyle Miller]

Eric Wieser said:

This seems similar to how we have A × B vs (a, b). I've seen comments in the past saying that Haskell uses the same notation for both but it is confusing.

(Haskell does the same with [A] for a list of things of type A.)

I guess it's not so hard to get Lean to have this same notation for cartesian products:

instance pair_to_cart : has_coe_to_sort (Type u × Type v) := ⟨_, λ p, p.1 × p.2⟩

example : (ℕ, ℕ) := (1, 2)

def swap {α β : Type*} (p : (α, β)) : (β, α) := (p.2, p.1)

Could this be a way to support $\otimes$ for terms and types? Have a coercion from the term tensor product of types to the tensor product?

[Mario Carneiro]

Note that haskell has the luxury of being able to do that because terms and types are different syntactic classes. This doesn't work in dependent type theories because they are completely different operators that both validly apply to types

[Kyle Miller]

That just means Haskell has the luxury of having (ℕ, ℕ) immediately be a type, rather than needing an additional rule for when such a term is used as a type. I think it's similar to how in Automath pi types are represented by lambda expressions, though that rule is built-in rather than needing a Lean-style coercion.

(It's unclear how you'd make [A] be the type of lists, but I just brought it up to illustrate that they like this sort of notation in Haskell.)

[Mario Carneiro]

Well in DTT the product type constructor is not necessarily injective, so making them the same is at least an additional axiomatic commitment

[Mario Carneiro]

and as you say this doesn't work at all for lists

[David Wärn]

def list_to_type : list Type → Type
| [] := fin 37
| [A] := list A
| (A::B::_) := fin 37

instance : has_coe_to_sort (list Type) := ⟨_, list_to_type⟩

example : list ℕ = [ℕ] := rfl

[Mario Carneiro]

Clearly the other lists should be tuple types ;)

[Kyle Miller]

Mario Carneiro said:

and as you say this doesn't work at all for lists

I regret bringing up lists, since it has nothing to do with what I was suggesting. (Though thanks for finding a solution to this puzzle, @David Wärn.)

I find it puzzling that you're saying it doesn't work when I gave some working code. Why does it matter if the product type constructor is injective? There are obviously some problems with needing coercions, but it seems to be significantly better than relying on CIRCLED CROSSING LANES or VAI SYLLABLE KPAN.

[Mario Carneiro]

If there is a coercion, then I can see some more possibilities; I was talking about the case where there is no coercion and the two constructors are identified