Remove `Spec()` notation

Stream: mathlib4

[Andrew Yang]

Continuing the trend of notation bikesheding, I am planning to remove the usage of Spec() notation in mathlib in #30272. It will be kept as a scoped notation so that down stream projects could still use it if they prefer to.
The reason being

1. It is really confusing that Spec(R) and Spec (R) have different meanings.
2. It hides CommRingCat.of, which is often the source of erw errors and other confusing behaviour.
3. It makes people erronously write Spec (.of R) for R : CommRingCat more easily.
4. It doesn't have much benefit to outweigh the downsides listed above. Spec (.of R) is a perfectly fine "vanilla" lean syntax that isn't really much longer or harder to read than Spec(R).

[Kenny Lau]

and I will continue to disagree, I think the fact that it's very close to maths notation is a huge benefit for readability, and I think we should know that ident( is always special notation because real brackets require a space before. I really don't think this is a good diff to see:

image.png

[Eric Wieser]

Can of be a coercion?

[Kevin Buzzard]

/-- The object in the category of R-algebras associated to a type equipped with the appropriate
typeclasses. This is the preferred way to construct a term of `CommRingCat`. -/
abbrev of (R : Type u) [CommRing R] : CommRingCat :=
  ⟨R⟩

Can an abbrev be a coercion?

[Kenny Lau]

and for more context, as discussed in the thread I linked to, I wish to eventually make Proj(R) a notation as well, which takes in a ring R with a canonical graded structure. (Recall that Proj really takes a grading, which for now is a term of type ℕ → Submodule R A.)

Then, the problem here is that if mathlib decides it doesn't want Proj(R) as well, seeking an alternative such as Spec (.of R) would be impossible, because the input that Proj takes has type Function, and nobody in their right mind would name the function that returns the canonical graded structure of a ring as Function.of, so there's no Proj (.of R) alternative available.

The alternative here would be something like Proj (Graded.of R) (ideally), which is much longer than Proj(R), and Graded.of still looks a bit off because there is no such structure/class called Graded (and once again it is actually a Function).

[Andrew Yang]

As I stressed above, I don't think hiding of by the removal of a space it is the right call because it is a important implementation detail (not as in it is mathematical important but as in it bites you if you are not careful).
I would be open to a proposal of a notation for of although I personally find nothing wrong with of. Something that looks weird and signals something odd is going on like the coe sort arrow ↥.

[Kenny Lau]

Kenny Lau said:

ident( is always special notation

To elaborate on this point, note how the colour changes:
image.png

[Robert Maxton]

Is it an important implementation detail? I mostly find it to be an annoyance that I-as-library-user can't really do anything about, so it should be covered up by the API as much as possible. The actual solution to most problems involving of tend to require me hiking back to whatever underlying bit of Mathlib in code I didn't write and redefining things to have exactly the right spelling of accepts-a-bundled-object vs. accepts-a-type-and-type-class vs. outright defining defs that refer to bundled objects as abbrevs to defs that refer to the unbundled types, rather than something I can address by redesigning 'my' code further down the import tree.

[Robert Maxton]

I've been wrestling with this in TopCat for a while now and it's absolutely not the case that of does very much for me other than add mental noise.

[Kenny Lau]

I've made #30285 to document the new changes in the docstring of docs#AlgebraicGeometry.Spec .

[Andrew Yang]

I agree we should add API to ease the transition from unbundled to bundled, but I don't think hiding it in a notation is API. I am happy to hide it once automation can make the transition seamless, but before that, it is a useful to have the distinction present to signify and remind the user to do the transition by hand.

[Robert Maxton]

It's less about making automation that makes the transition seamless, and more about making the existing definitions in such a way that existing automation can handle it seamlessly. Again, there's not much that a Mathlib user can actually do about, for a concrete example, the fact that docs#TopCat.sigmaIsoSigma is missing an of and therefore doesn't play well with unbundled objects on the left, except go and edit Mathlib; that says to me that this should be essentially an 'implementation detail problem' that as much as possible should be invisible from outside the library.

[Kenny Lau]

let me make a reference to another good notation in the AG library, which is ⁻¹ᵁ and ''ᵁ. you'll never be able to guess what they actually stand for, but they make statements look much cleaner and easier to read.

• f ⁻¹ᵁ U is notation for (Opens.map f.base).obj U, the preimage of an open set U under f.

https://github.com/leanprover-community/mathlib4/blob/70adeca95169a95af5987779ff931e095b213197/Mathlib/AlgebraicGeometry/OpenImmersion.lean#L84-L85:

/-- `f ''ᵁ U` is notation for the image (as an open set) of `U` under an open immersion `f`. -/
scoped[AlgebraicGeometry] notation3:90 f:91 " ''ᵁ " U:90 => (Scheme.Hom.opensFunctor f).obj U

and on top of that, the lemmas referring to them actually call them image and preimage in the name of the theorem, which to me is another sign of good notation API happening

[Kenny Lau]

and actually I did have trouble finding out what they actually are (when I needed to build more API) but i didn't mind that drawback

[Kenny Lau]

Andrew Yang said:

I agree we should add API to ease the transition from unbundled to bundled, but I don't think hiding it in a notation is API.

I think we should have enough API (if we don't already) so that we can just work with Spec(R) and forget that it ever stood for Spec (.of R). What are some deficiencies in this part that you've experienced?

[Kenny Lau]

(you usually don't rewrite types)

[Andrew Yang]

The fact that you are able to locate the fact that docs#TopCat.sigmaIsoSigma is missing an of is in part because if there is an of it will show up.

[Andrew Yang]

(and I also don't see why docs#TopCat.sigmaIsoSigma should have an of on the left but this is off topic)

[Kenny Lau]

I think that one deficiency might be how Spec.map takes CommRingCat.ofHom, to which... we should have Spec.map( as well

[Kenny Lau]

(btw surely it should be spec?)

[Christian Merten]

Kenny Lau said:

(btw surely it should be spec?)

The capitalization conventions don't apply when the name is always used in a specific spelling in the literature. In this case, Spec is never written spec.

[Christian Merten]

Kenny Lau said:

I think that one deficiency might be how Spec.map takes CommRingCat.ofHom, to which... we should have Spec.map( as well

No, for this the correct fix is to rename CommRingCat.ofHom to CommRingCat.Hom.of.

[Yaël Dillies]

@Christian Merten, @Andrew Yang, would you be happy if we made Spec(R) an elaborator that automatically checked whether R : CommRingCat or R : Type _ and applies .of accordingly? This is perfectly possibly, I simply hadn't done it because I am satisfied with the simpler statu quo, but clearly you are not.

[Kenny Lau]

how will that fix the "confusing error messages" that andrew is referring to

[Yaël Dillies]

I have no idea what these error messages are. I have never encountered them myself

[Kenny Lau]

me neither, but that's because I know that Spec(R) is Spec (.of R), so maybe I'm not in the targeted audience of Andrew's explanations

[Eric Wieser]

Kevin Buzzard said:

Can an abbrev be a coercion?

Coercions don't even need a function, you can just inline the coercion into the Coe instance as an arbitrary expression

[Yaël Dillies]

Let me take Andrew's original message apart and apply my suggestion to it:
Andrew Yang said:

1. It is really confusing that Spec(R) and Spec (R) have different meanings.

First, I don't find this really confusing. In the context of Lean 4, people have been repeatedly made aware that spaces before brackets are really important: eg we didn't scrap the congr() elaborator because congr could mean something else.
Second, with my suggestion, Spec R would still be valid syntax for R : CommRingCat, but we would encourage contributors to use Spec(R).

2. It hides CommRingCat.of, which is often the source of erw errors and other confusing behaviour.

With my suggestion, it would not hide any unnecessary CommRingCat.of, which I believe are the actual source of the erw errors you mention. Of course, it is impossible to be sure without you giving us a concrete example.

3. It makes people erronously write Spec (.of R) for R : CommRingCat more easily.

With my suggestion, Spec(R) would never introduce Spec (.of R) in the expression for R : CommRingCat.

4. It doesn't have much benefit to outweigh the downsides listed above. Spec (.of R) is a perfectly fine "vanilla" lean syntax that isn't really much longer or harder to read than Spec(R).

It has for me the so far unparalleled benefits that (not even so) large goals involving Spec (CommRingCat.of R) move from the "unreadable, :warning: brain panic :warning:" zone to the "readable, I know how to prove this" one.

Spec (.of R) is short to read in the source code, but not in the infoview. This is, I believe, why our opinions diverge.

In the future, maybe Lean will delaborate to uses of anonymous dot notation, so that Spec (CommRingCat.of R) actually delaborates as Spec (.of R). If such a change to delaboration occurred, I would agree that the Spec(R) notation would be significantly less useful (but IMO still useful enough that we should use it).

[Eric Wieser]

My coercion suggestion is to show Spec ↑R when R is a type, and Spec R when R : CommRingCat

[Eric Wieser]

Or perhaps to declare a new special arrow as a delaborator for category-theoretic of, since it's sort of the reverse of coeSort

[Kenny Lau]

so clearly it's ↓

[Eric Wieser]

I was thinking ⤒ or ⤓ or ↧ (which are all dual to ↥)

[Christian Merten]

Yaël Dillies said:

Christian Merten, Andrew Yang, would you be happy if we made Spec(R) an elaborator that automatically checked whether R : CommRingCat or R : Type _ and applies .of accordingly? This is perfectly possibly, I simply hadn't done it because I am satisfied with the simpler statu quo, but clearly you are not.

This would be much better than the old notation, but it still hides whether R : Type _ or R : CommRingCat. For me, this is a readability loss, because I can't immediately see if there is a .of or there is none.

[Christian Merten]

I agree that seeing Spec (CommRingCat.of R) in the infoview can be annoying, but if we wanted to specifically fix this, we could have a delaborator that makes this pretty-print as Spec (.of R) instead.

[Christian Merten]

The advantage with Eric's suggestion is that the distinction between R : Type _ and R : CommRingCat stays visible, but I am not sure this has to be done with a coercion. It could as well be a delaborator.

[Kenny Lau]

@Christian Merten what if we renamed Spec into Spectrum and kept Spec(R)?

[Christian Merten]

So every name becomes longer, we no longer use the standard literature name and we still have all the disadvantages of the Spec(R) notation?

[Kenny Lau]

actually why does Spec take a CommRingCat in the first place?

[Kenny Lau]

Christian Merten said:

So every name becomes longer, we no longer use the standard literature name

we can still use Spec namespace

we still have all the disadvantages of the Spec(R) notation?

one of the main disadvantages brought up was "confusing notation", now that Spec(R) and Spectrum (.of R) are very different, there should be no more confusion

[Eric Wieser]

Christian Merten said:

The advantage with Eric's suggestion is that the distinction between R : Type _ and R : CommRingCat stays visible, but I am not sure this has to be done with a coercion. It could as well be a delaborator.

Remember that coercions have two pieces; the delaborator via @[coe] and the auto-insertion via instance. My proposal is to use the latter and write a custom delaborator in place of the former

[Christian Merten]

Eric Wieser said:

Remember that coercions have two pieces; the delaborator via @[coe] and the auto-insertion via instance. My proposal is to use the latter and write a custom delaborator in place of the former

From what I gathered from this thread is that the main concern of the proponents of the Spec(R) notation is how Spec (.of R) is pretty-printed. So I don't think we need the auto-insertion of the coercion.

[Andrew Yang]

Would prefix:max "↧" => CommRingCat.ofbe a good middle ground?

[Kenny Lau]

well then people will say that TopCat.of also wants that notation

[Christian Merten]

Scoped to AlgebraicGeometry? I would not know why CommRingCat should in general deserve special treatment

[Kenny Lau]

I think as suggested before ↧ should mean "look at the expected type, find the .of function, and apply it"

[Kenny Lau]

and then we should have Spec ↧R

[Andrew Yang]

In the long run we probably should give that notation to CategoryTheory.ToType and switch to that everywhere. But I'm just asking if people would be happy about such a notation in this context.

[Kenny Lau]

I guess I can stand behind Spec ↧R

[Eric Wieser]

Note that ↥ is not notation for coeSort any more, but a generic delaborator for arbitrary coercions to sort

[Yaël Dillies]

Andrew Yang said:

Would prefix:max "↧" => CommRingCat.ofbe a good middle ground?

I think this would be good enough until we need it for a second category (any idea when that would happen?)

[Kenny Lau]

Yaël Dillies said:

we need it for a second category

right after that we discussed it already and we already had 2 suggestions

[Kenny Lau]

Kenny Lau said:

↧ should mean "look at the expected type, find the .of function, and apply it"

Andrew Yang said:

In the long run we probably should give that notation to CategoryTheory.ToType and switch to that everywhere.

[Eric Wieser]

Kenny, I think your proposal might be what you get for free if you overload the notation

[Kenny Lau]

what can i say, i love overloading notation

[Robin Carlier]

Aren't overloaded notations very bad performance-wise? From what I gather this situation is not exactly similar, but when the tensor product of objects and morphisms in a monoidal category were overloaded with same notations it was very bad.

[Kenny Lau]

I think Andrew's solution is better regardless (but might require more refactoring)

[Yaël Dillies]

The monoidal notation was performant but it had poor unification

[Robin Carlier]

That's not what I read from the benchmark result for the PR?
It also had bad unification.

[Aaron Liu]

maybe make it scoped

[Aaron Liu]

how many categories could you possibly be working with simultaneously

[Aaron Liu]

(I have no idea how many)

[Yaël Dillies]

Robin Carlier said:

That's not what I read from the benchmark result for the PR?
It also had bad unification.

Oh right, I forgot about that :speak_no_evil: