notation for torsion subgroup

Stream: mathlib4

[Kevin Buzzard]

The notation $A[n]$ to represent the subgroup of the additive abelian group $A$ comprised of solutions to $na=0$ for some natural $n$ was I think popularised by Mazur in his paper I need for FLT. @Peiran Wu has just PRed this notation to mathlib:

@[reducible]
def torsionBy := (Submodule.torsionBy ℤ A n).toAddSubgroup

@[inherit_doc]
scoped notation:max A"["n"]" => torsionBy A n

in #11742 , but I can't get it to work with numerals. Here's the phenomenon on master:

import Mathlib.Algebra.Module.Torsion

namespace AddSubgroup

variable (A : Type*) [AddCommGroup A] (n : ℕ)

/-- The additive `n`-torsion subgroup for `n` in `ℕ`. -/
@[reducible]
def torsionBy := (Submodule.torsionBy ℤ A n).toAddSubgroup

@[inherit_doc]
scoped notation:max A"["n"]" => torsionBy A n

#check A[n] -- works
#check ℤ[n] -- works
#check A[37] -- fails (ambiguous)
#check (A[37] : AddSubgroup A) -- still fails:
/-
ambiguous, possible interpretations
  A[37] : AddSubgroup A

  A[37] : AddSubgroup A
-/

Is there any way of getting this standard notation to work? I promise I don't need list notation. Otherwise there's always these...

LEFT BLACK LENTICULAR BRACKET (U+3010, Ps): 【
RIGHT BLACK LENTICULAR BRACKET (U+3011, Pe): 】
LEFT TORTOISE SHELL BRACKET (U+3014, Ps): 〔
RIGHT TORTOISE SHELL BRACKET (U+3015, Pe): 〕
LEFT WHITE LENTICULAR BRACKET (U+3016, Ps): 〖
RIGHT WHITE LENTICULAR BRACKET (U+3017, Pe): 〗

[Yaël Dillies]

Wild guess, but what happens if you remove the @[reducible]?

[Adam Topaz]

I think it has to do with how num literals are parsed as syntax.

[Adam Topaz]

Note that these work:

#check A[(37 : ℕ)]
#check (A[(37 : ℕ)] : AddSubgroup A)

[Damiano Testa]

In fact, just A[(37:)] works. I wonder if it gets confused with wanting to use GetElem.

[Adam Topaz]

yeah, probably: This all works:

import Mathlib.Algebra.Module.Torsion

namespace AddSubgroup

variable (A : Type*) [AddCommGroup A] (n : ℕ)

/-- The additive `n`-torsion subgroup for `n` in `ℕ`. -/
@[reducible]
def torsionBy := (Submodule.torsionBy ℤ A (n : ℕ)).toAddSubgroup

@[inherit_doc]
scoped notation:max A"_["n"]" => torsionBy A (n : ℕ)

#check A _[n]
#check ℤ _[n]
#check A _[3]
#check (A _[3] : AddSubgroup A)

[Peiran Wu]

So it seems anything more than just a pair of square brackets will work. Just to put another suggestion out there, we could add a subscript plus sign (\_+) after the closing bracket, indicating that A is AddCommGroup. Should Subgroup.torsionBy be added for CommGroup, there would be an obvious counterpart.

scoped notation:max A"["n"]₊" => torsionBy A n

#check A[37]₊ -- works

[Kim Morrison]

Or just, you know, torsionBy A 37, which seems rather more readable to me. :-)

[Damiano Testa]

This also just works:

#check A [37] -- note the space!

I'm not sure about the consequences of the following, but adding

attribute [-instance] Fin.instGetElemFinVal

makes the notation work as well.

[Kim Morrison]

But why make fragile notation, or break basic stuff to make the notation work?

[Damiano Testa]

Are you suggesting to remove the torsionBy notation? I agree that it is very poorly implemented, but it is also very standard in maths...

[Kevin Buzzard]

We've used _x before in notation to mean "this is a subscript in maths"", but this really isn't a subscript.

[Kevin Buzzard]

The + sign makes it look like we're taking the positive part of the torsion

[Kevin Buzzard]

Kim Morrison said:

But why make fragile notation, or break basic stuff to make the notation work?

Could we scope the competing getElem notation?

[Antoine Chambert-Loir]

Damiano Testa said:

Are you suggesting to remove the torsionBy notation? I agree that it is very poorly implemented, but it is also very standard in maths...

I'd stay its standard, but not very standard. I also have seen indices on the right, as well as on the left. I wonder whether a notation for integers is that important. One frequently has to consider, for an $R$-module $M$ and an element $a\in R$, of the module $M[a]$ of elements $m\in M$ such that $a\cdot m=0$ (or whatever other notation), and even, if $I$ is an ideal of $R$, of the submodule $M[I]$ of elements $m\in M$ such that $a\cdot m=0$ for all $a\in I$. A uniform thing would be useful.

[Kim Morrison]

People also use it e.g. for homological shifts of an object, and I'm sure for a dozen other things. :-) It's just bad notation in a universal maths library.

[Johan Commelin]

I think it would be good if we could locally choose the meaning

[Johan Commelin]

One of the problems with AG in mathlib is that statements are becoming unbearably long. Having concise notation that matches the real world is important.

[Johan Commelin]

Of course I realise that there are many cases in informal maths where notation isn't precise/unambiguous/formalizable.
But this doesn't seem to be one of them.

[Damiano Testa]

I think that there is a mechanism for resolving ambiguities for declarations in the current namespace over another one. Could that not be the case for scoped notation as well? That is, in case of an ambiguity, the scoped one takes precedence.

[Enrico Borba]

Also used in mathlib's probability P[X]

[Kyle Miller]

You should be able to do scoped notation:max (priority := high) A"["n"]" => torsionBy A n to get notation that overrides a pre-existing one.