Special case declarations for `Scheme.Cover`

Stream: mathlib4

[Christian Merten]

Recently, docs#AlgebraicGeometry.Scheme.Cover was replaced by an abbrev for docs#CategoryTheory.Precoverage.ZeroHypercover (a 0-hypercover is an indexed family of morphisms in the precoverage).

In the process, we deprecated many special case constructions for the case of Schemes (e.g. docs#AlgebraicGeometry.Scheme.Cover.pullbackCover). Some special declarations still remain though (of which most don't make sense in the general setting), e.g. docs#AlgebraicGeometry.Scheme.Cover.ulift.

This leads to some annoying behaviour, for example:

import Mathlib

open CategoryTheory AlgebraicGeometry

/--
error: Invalid field `ulift`: The environment does not contain `CategoryTheory.Precoverage.ZeroHypercover.ulift`
  Precoverage.ZeroHypercover.pullback₁ f U
has type
  (Scheme.precoverage IsOpenImmersion).ZeroHypercover X
-/
#guard_msgs in
noncomputable example (X Y : Scheme) (f : X ⟶ Y) (U : Y.OpenCover) : X.OpenCover :=
  (U.pullback₁ f).ulift

Whenever we use one of the general ZeroHypercover constructions, we end up with (Scheme.precoverage IsOpenImmersion).ZeroHypercovers instead of OpenCover in the infoview.

A few options to improve the situation:

1. Duplicate all general PreZeroHypercover and ZeroHypercover constructions for the special case of Scheme.Cover (and maybe also Scheme.OpenCover?!) and treat ZeroHypercover as an implementation detail that users should not interact with (this also means duplicating all generated simps lemmas!)
2. Remove AlgebraicGeometry.Scheme.Cover and move all AlgebraicGemetry.Scheme.Cover.* declarations to the AlgebraicGeometry.CategoryTheory.Precoverage.ZeroHypercover namespace. After open AlgebraicGeometry this makes these available with dot notation as before.
3. Make Scheme.Cover and Scheme.OpenCover notation equipped with a delaborator. Users would still interact with ZeroHypercover and this fact would be explained in the docstring of the Scheme.Cover notation.

In my opinion, option 1 is only feasible when done automatically by some meta program (maybe using @Dagur Asgeirsson 's duplicate attribute?), because the ZeroHypercover API will keep growing and keeping the API in sync manually would be a nightmare.
Option 2 has all the disadvantages of the TopLevelA.TopLevelB trickfeature, but avoids duplication and encourages more general statements because users are made aware of the more general ZeroHypercover API.
Option 3: Brings back the sane infoview, but does not hide the implementation.

My preference would be a combination of 2 and 3.

Happy to hear comments or suggestions (pinging some possibly interested people: @Andrew Yang, @Joël Riou, @Johan Commelin).

[Johan Commelin]

Intuitively, I think I would rank these from favorite to least favorite as 2,1,3.

[Joël Riou]

2 looks good to me.

[Andrew Yang]

I do not like 2 because this is very unreadable everywhere where the dot notation is not available: in docs, infoviews, loogle outputs, hovers etc. I do not think 1 is that bad as this is a common pattern when setting up API boundaries.

[Kevin Buzzard]

I'm not an expert in this sort of thing at all, but I am wondering whether in group cohomology we tried an analogue of 2 and it didn't work very well. @Edison Xie @Kenny Lau an I making any sense? I'm talking about how you guys decided that trying to make Rep an abbrev for Action and then getting everyone to use Action under the hood didn't work very well for you (why not?). But I might be confused and talking about something else.

[Kenny Lau]

I do like 1 the best, I think metaprogramming is the best solution in this case. As Kevin mentioned, we had to define Rep.res in our repo and use that instead of Action.res (so another API duplication) because it kept leaking into Action.

[Christian Merten]

If we did 1, where do we stop? Do we duplicate every declaration that mentions PreZeroHypercover or ZeroHypercover? I.e. we also duplicate things like docs#CategoryTheory.PreZeroHypercoverFamily or docs#CategoryTheory.MorphismProperty.IsLocalAtTarget? This is not only creating a bunch of aliases, we would also have to transform the bodies of definitions, inductive types etc.

[Christian Merten]

Kevin Buzzard said:

I'm talking about how you guys decided that trying to make Rep an abbrev for Action and then getting everyone to use Action under the hood didn't work very well for you (why not?). But I might be confused and talking about something else.

This is not what 2 is saying. 2 is saying to have no abbrev at all and directly use the docs#CategoryTheory.PreZeroHypercover API. When specific declarations are needed, they would get the AlgebraicGeometry prefix.

[Andrew Yang]

I'd say we duplicate everything that we need. So yes to IsLocalAtTarget and maybe to PreZeroHypercoverFamily.

[Andrew Yang]

A middleground is to work with ZeroHypercover directly but avoid the unintelligible names. This means no dot notation but I don't think this matters a lot.

[Christian Merten]

By "the unintelligible names" you mean the TopLevelA.TopLevelB feature?

[Christian Merten]

If so, how would you call docs#AlgebraicGeometry.Scheme.Cover.ulift then?

[Andrew Yang]

Scheme.uliftCover?

[Andrew Yang]

Or keep the name and open Scheme.Cover and write ulift \McU.

[Andrew Yang]

To clarify, the two main points against 2 are
(a) open CategoryTheory no longer works in namespace AlgebraicGeometry
(b) The AlgebraicGeometry.CategoryTheory.Precoverage.ZeroHypercover namespace is unreadable everywhere but the source code.

And the only point for 2 (compared to no-duplication + no-weird-names) is (afaik) dot notation.
I am happy to forfeit (a) for dot notation but I don't think the current downside in (b) outweighs the benefit you get from dot notation.

A way to lessen the impact of (b) is by e.g. renaming CategoryTheory.Precoverage.ZeroHypercover to CategoryTheory.Cover, and to write a delaborator to let the infoview (and perhaps statments in docs) pretty print like the source code. In this case at least only the declaration names in docs/search results are moderately bad.

[Christian Merten]

Already now without any delaborators and independent of the namespace, the docs only show the last part of the declaration's name inside the statement.
(Side note: A delaborator would not help for improving the looks of the docs, because the delaborator would probably be scoped and hence ignored by docgen.)

Are declaration names with many nested namespaces in docs / search really that bad? I don't find them visually distracting and reasonably readable, because the names are structured by ..

In my opinion, we should prioritise
(a) readability in the infoview, and
(b) readability in the sourcecode, and
(c) typing load.

(a) can be fixed by a delaborator, independent of any of the other decisions.
(b) and (c) can mostly be dealt with by open and dot notation in option 2 above.

[Christian Merten]

The (only?) place where full declaration names matter, is loogle and here I definitely agree that typing out AlgebraicGeometry.CategoryTheory.Precoverage.ZeroHypercover.Foo is annoying.

[Andrew Yang]

Are declaration names with many nested namespaces in docs / search really that bad?

Here's an example where I replaced Scheme.Cover in the docs with CategoryTheory.Precoverage.ZeroHypercover.
image.png

[Andrew Yang]

OTOH is dot notation really necessary for readability? How unreadable does the statement get without dot notation?

[Christian Merten]

I don't think this is significantly worse than:
image.png
For me both are unreadable enough that I never use the sidebar to find a declaration.

[Andrew Yang]

You are forced to look at them in loogle and docs search results and the autocompletion dropdowns though. Even if you don't personally use them, I believe they are a key part of most people's workflow that we should not disregard the usability of these tools.

[Christian Merten]

It seems to me that autocomplete is already namespace aware? (Admittedly, I don't use autocomplete, so I might very well be wrong. But some quick experiments in vscode seem to confirm this.)

[Andrew Yang]

Thinking about this a bit more, I would still strongly prefer seeing X.OpenCover over Precoverage.ZeroHypercover (Scheme.precoverage IsOpenImmersion) X in infoviews though.

[Andrew Yang]

By autocomplete I mean the dropdown search menu in docs.

[Christian Merten]

Andrew Yang said:

Thinking about this a bit more, I would still strongly prefer seeing X.OpenCover over Precoverage.ZeroHypercover (Scheme.precoverage IsOpenImmersion) X in infoviews though.

This could be (partially) fixed by a delaborator though.

[Christian Merten]

I think we should first decide on the following question:

Do we want users to interact with the general ZeroHypercover API at all or do we want to treat this entirely as an implementation detail?

[Christian Merten]

Middleground could be: We want special support for Scheme.OpenCover and anything that involves changing the topology should use ZeroHypercover directly.

[Andrew Yang]

I would be okay with this as a temporary solution, and when we start doing a bunch of concrete computations with covers in other topologies we could re-evaluate if this special support should be extended to the other topologies or scrapped entirely.

[Andrew Yang]

OTOH do you not think renaming CategoryTheory.Precoverage.ZeroHypercover to CategoryTheory.Cover would improve readability substantially though while losing little? Is 0-hypercover a common name in the literature? I usually see them called covering families or just covers.

[Christian Merten]

ZeroHypercover is in analogy with OneHypercover.

[Andrew Yang]

Yes I understand the reason but is this analogy that important? Do you need to know about OneHypercover to use the API of ZeroHypercover or to understand the mathematical concept of ZeroHypercover?