Notation for crossProduct

Stream: mathlib4

[ZhiKai Pong]

@Eric Wieser I hope you don't mind me pinging, I noticed that for cross products the corresponding symbol
×₃ is typed using \x or \times or \multiplication, but then there is
⨯which is \X or \vectorproduct or \crossproduct which seem a bit odd.

I was typing \crossproduct and it took me while to realize its not what's used in the actual cross product. is there a discrepancy here and should the notation/docstrings be updated?

[Notification Bot]

A message was moved here from #new members > Using crossProduct in EuclideanSpace (Fin 3) by Eric Wieser.

[Eric Wieser]

I'd be in favor of switching to the ⨯ notation, as unicode allocates it specifically for this purpose.

[ZhiKai Pong]

do we want to keep the 3 in ⨯₃ or just ⨯?

[Eric Wieser]

I guess drop it; if we ever get the 7-dimensional version we can add a notation typeclass

[ZhiKai Pong]

is there an easier way to find all files that contain crossProduct? I'm currently going through the files manually using Imported by in the docs, which luckily isn't a lot but I'm wondering is there a better way

[Eric Wieser]

lake build and see what breaks?

[Martin Dvořák]

FYI I find × and ⨯ really hard to distinguish.

[Martin Dvořák]

Also, since dot product, which is used far more often than cross product, does not have a single-symbol operator, I find it weird to give this luxury to cross product.

[Martin Dvořák]

That's just my two cents on why I wouldn't make the suggested change.

[Martin Dvořák]

BTW copy the following five symbols into your favorite editor with your favorite font in the size you normally use ⨯×xXχ and tell us how easy it is to distinguish them from each other.

[ZhiKai Pong]

Martin Dvořák said:

BTW copy the following five symbols into your favorite editor with your favorite font in the size you normally use ⨯×xXχ and tell us how easy it is to distinguish them from each other.

(⨯×xXχΧ theres \Chi as well)

[Eric Wieser]

I claim that being able to distinguish them is easy, because all but one will give a lean type error

[ZhiKai Pong]

I've made #27006

[Martin Dvořák]

Maybe neither ×₃ nor ⨯ should be the operator; it should be ⨯₃ instead.

[Eric Wieser]

I don't think the 3 conveys anything interesting

[Kevin Buzzard]

We're trying to mimic what mathematicians write, not what they should write or what it would be convenient if they wrote.

[Eric Wieser]

ZhiKai Pong said:

I've made #27006

I've added some meta code to this PR to deprecate the syntax; maybe @Yaël Dillies has opinions since they did something similar for sum notation?

[Yaël Dillies]

Have you tried it? I'm slightly worried your suggestion will replace a ×₃ b with ⨯ rather than a ⨯ b, but if you've tried and it does the right thing, then looks reasonable

[Jireh Loreaux]

Personally, I would really prefer the ⨯₃ notation (including the ₃) because it aids with disambiguation when reading the code (e.g., on GitHub). But perhaps I'm overestimating the possibility for ambiguity.

[Eric Wieser]

I claim there is no situation where there is any risk of ambiguity, since thankfully Fin 3 -> R has no coercion to sort!

[Eric Wieser]

But maybe this should be put to a vote in a day or so, once any other interested parties have made their argument.

[Jireh Loreaux]

You're probably right that it's not necessary, but I think it would still be my preference.

[ZhiKai Pong]

do we still want a vote or is the consensus to go with ⨯₃?

[Eric Wieser]

/poll What should the syntax be for crossProduct?

• ×₃ (U+00D7 multiplication sign, status quo)
• ⨯ (U+2A2F vector or cross product)
• ⨯₃ (U+2A2F vector or cross product)

[ZhiKai Pong]

bump since there's a tie

[Edward van de Meent]

Kevin Buzzard said:

We're trying to mimic what mathematicians write, not what they should write or what it would be convenient if they wrote.

Eric Wieser said:

I claim that being able to distinguish them is easy, because all but one will give a lean type error

from this, i gather that what we really want is a custom elaborator for ×, not different notation?

[Edward van de Meent]

because i'm in favour of making it easy to type the right thing. i really don't want another "you wrote |, but you really meant ∣"

[Edward van de Meent]

it isn't even terribly difficult, i think? we can just do this:

import Mathlib

variable {α β : Type*} {R : Type*} [CommRing R] (a b : Fin 3 → R)

@[inherit_doc] scoped[Matrix] infixl:74 " × " => crossProduct

open Matrix

#check α × β -- Prod α β : Type (max u_1 u_2)

#check a × b -- (crossProduct a) b : Fin 3 → R

[Edward van de Meent]

so long as there isn't a coersion from Fin 3 -> R to Sort _ i think this should work

[Edward van de Meent]

even the hover docstring is disambiguated based on which version parses/typechecks!

[Eric Wieser]

i really don't want another "you wrote |, but you really meant ∣"

I think this is fine, as long as the linter tells you this rather than having to ask a human on zulip

[Edward van de Meent]

i don't see why there should be a distinct character for this operation

[Eric Wieser]

For divides or for vector product?

[Eric Wieser]

In either case, that sounds like a gripe to take up with the unicode consortium, and mathlib should just follow their recommendations where possible.

[Edward van de Meent]

Eric Wieser said:

mathlib should just follow their recommendations where possible

i suspect that this is a bad idea

[Weiyi Wang]

Would a custom elaborator make doc search harder? I hope it won't give me a hard time to find the actual definition if I ctrl-click on the symbol, or putting the symbol in the doc search bar

[Edward van de Meent]

i hardly ever use that feature, but guessing from the fact that the hover is correct, i think it'd work?

[Edward van de Meent]

putting the symbol in the search bar should find Matrix.«term_×_» in the example i gave above

[ZhiKai Pong]

looks like ⨯₃ wins? should we just go ahead and make this change for now or are we still considering the proposed alternatives?

[ZhiKai Pong]

@Eric Wieser I've updated #27006 according to poll results (or should I ping you on github instead?)