global notation for linear span of singleton

Stream: mathlib4

[Aaron Liu]

There is a global notation R ∙ x for Submodule.span R {x}. This was incredibly confusing to me looking on loogle and docgen for theorems I want because it resembles the a • b notation for HSMul.hSMul a b. Should this notation be scoped?
The notation is defined here in Mathlib.LinearAlgebra.Span.Defs. It has about 60 uses throughout mathlib. In contrast, span {_} has about 600 uses throughout mathlib.

[Eric Wieser]

Note there was previous discussion to make it use the same symbol as hSMul, but I assume that would have been even more confusing

[Edward van de Meent]

if it gets scoped, people looking at docgen won't be confused anymore :tear:

[Edward van de Meent]

not a bug, but a feature

[Andrew Yang]

I would vote to remove this notation.

[Violeta Hernández]

Not only does it resemble •, but it also resembles the notation (R · x) for partially applied functions. I also vote remove.

[Snir Broshi]

How about replacing it instead of removing? Perhaps adding a subscript s or sp for span?

[Andrew Yang]

I find the non-notation span R {x} already quite short and clear and closer to the paper maths $\mathrm{span}_R(x)$ than any notaton could be.

[Yury G. Kudryashov]

If we remove this notation, it would be nice to "deprecate" it first (make it issue a deprecation warning and don't generate a delaborator from it).

[Eric Wieser]

Violeta Hernández said:

Not only does it resemble •, but it also resembles the notation (R · x) for partially applied functions. I also vote remove.

Perhaps also worth mentioning that the span notation was invented before this function notation existed, and so this was not considered originally.

[Eric Wieser]

(by @Heather Macbeth in !3#5538, #general > Notation for span @ 💬 )

[Patrick Massot]

Andrew Yang said:

I find the non-notation span R {x} already quite short and clear and closer to the paper maths $\mathrm{span}_R(x)$ than any notaton could be.

Have you already seen someone writing $\mathrm{span}_R(x)$ rather than $Rx$??

[Patrick Massot]

I’m not against scoping that notation of course, but I’m very puzzled by your assertion about paper maths here.

[Michael Stoll]

I usually write $\langle x \rangle_R$ ...

[Violeta Hernández]

I've never seen anyone write $Rx$? I usually just write $\langle x\rangle$.

[Violeta Hernández]

I think it'd be nice to have notation ⟨a, b, c, ...⟩ that we could reuse for span-like objects, such as docs#Submodule.span or docs#Ideal.span or docs#Subgroup.closure. Not sure if that'd be feasible.

(using some other kind of angle brackets, since ⟨x⟩ already has a meaning in Lean)

[Snir Broshi]

Violeta Hernández said:

I've never seen anyone write $Rx$?

AFAIK $\Z/n\Z$ is a pretty common notation for ZMod n, and the $n\Z$ represents the span of n in $\Z$. Though I guess that's $xR$ rather than $Rx$.
Also #new members > Stating the theorem that no ring isomorphism 2Z and 3Z is about the use of that notation in "Abstract Algebra by Dummit and Foote".

[Violeta Hernández]

Well, but that's $xR$ rather than $Rx$ isn't it

[Kevin Buzzard]

$Rx$ is common in my neck of the woods

[Johan Commelin]

Violeta Hernández said:

I think it'd be nice to have notation ⟨a, b, c, ...⟩ that we could reuse for span-like objects, such as docs#Submodule.span or docs#Ideal.span or docs#Subgroup.closure. Not sure if that'd be feasible.

(using some other kind of angle brackets, since ⟨x⟩ already has a meaning in Lean)

See also #mathlib4 > Abstracting the substructure lattice construction @ 💬 and the discussion below it.