felixwellen / synthetic-zariski

Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos
MIT License
50 stars 5 forks source link

Discussion on renamings #29

Open felixwellen opened 5 months ago

felixwellen commented 5 months ago

At the last hour of SAG-4, we had a discussion on names. The following was discussed in more detail:

felixwellen commented 5 months ago

@iblech , @MatthiasHu @hmoeneclaey : It would be interesting to have your opinions on the third, since you were not in the discussion. If you agree, we could just change that everywhere.

mnieper commented 5 months ago
* Everyone taking part in the discussion agreed after exchanging arguments for a while, that we should abandon the current practice of having different names for "the same" types, e.g. Gm, A×, R× all denote the same, as do An and Rn.  The distinction was usually justified by using them to make the coercions to schemes, groups, rings, algebras explicit. However, it does not seems that it is reasonably clear when to use which notation and it has been a source of confusion. Also, just using R everywhere seems a lot simpler and emphasizes the advantage of SAG that this is possible.

What are possible reasons speaking against renaming all instances of $R$ into $\mathbb A$? In our theory, $R$ is as fundamental as $\mathbb N$, for example, and deserves a bold letter (at least not an italic one standing for some type variable). $\mathbb A$ stands, of course, for anneau. This is also closer to classical algebraic geometry, where the ring in the context of schemes over a ring is usually called $A$.

xuanruiqi commented 5 months ago

I don't think conflating $\mathbb{A}$ and $R$ is a good idea though. One usually thinks of the former as a set and the latter as a ring.

felixwellen commented 5 months ago

We thought so as well in the beginning, but I was convinced in the discussion. It is actually common, well-working practice to conflate, for example, all the different $\mathbb R$ s for the manifold, the set, the group, the affine space, the field,...

felixwellen commented 5 months ago
* Everyone taking part in the discussion agreed after exchanging arguments for a while, that we should abandon the current practice of having different names for "the same" types, e.g. Gm, A×, R× all denote the same, as do An and Rn.  The distinction was usually justified by using them to make the coercions to schemes, groups, rings, algebras explicit. However, it does not seems that it is reasonably clear when to use which notation and it has been a source of confusion. Also, just using R everywhere seems a lot simpler and emphasizes the advantage of SAG that this is possible.

What are possible reasons speaking against renaming all instances of R into A? In our theory, R is as fundamental as N, for example, and deserves a bold letter (at least not an italic one standing for some type variable). A stands, of course, for anneau. This is also closer to classical algebraic geometry, where the ring in the context of schemes over a ring is usually called A.

I see the point. But if we call the ring $\mathbb A$ what letter can we use for an algebra over it? $A$ seems suboptimal, at least in spoken language.

xuanruiqi commented 5 months ago

Or we can perhaps try $k$. It is a (constructive) field after all, and this notation is consistent with use in algebraic geometry where one regularly speaks of schemes over $k$. Of course, as discussed, they are not equivalent to really schemes over $k$ but nevertheless.

Also, $A$ stands for both French anneau and English algebra, so it does seem that $A$ would better fit an algebra (i.e. ring) over the base ring.

mnieper commented 5 months ago

I see the point. But if we call the ring $\mathbb A$ what letter can we use for an algebra over it? $A$ seems suboptimal, at least in spoken language.

If more than one ring is involved, one usually uses letters like $B$ and $C$ following in the alphabet.

Or we can perhaps try $k$. It is a (constructive) field after all, and this notation is consistent with use in algebraic geometry where one regularly speaks of schemes over $k$. Of course, as discussed, they are not equivalent to really schemes over $k$ but nevertheless.

By my reasoning above, it should be $\mathbb k$ then. So far, $k$ has been reserved for the external ring over which the sheaf model is constructed.

The external object that corresponds to our internal ring is the functor that maps each algebra over the base ring $k$ to itself. This functor is classically called $\mathbb A$ and neither $k$ nor $\mathbb k$.

Also, stands for both French anneau and English algebra, so it does seem that would better fit an algebra (i.e. ring) over the base ring.

The notion of algebra is just too general; even the base ring is an algebra (over $\mathbb Z$), so I think we can exclude it from the naming discussion. Even in French, algèbre begins with the letter "A"; nevertheless, this never persuaded the French (and English and German) literature in commutative algebra and algebraic geometry from using $A$ for a ring.

felixwellen commented 5 months ago

I did some rough, heuristic text-replacing on the foundations draft, you can see the result here:

https://felix-cherubini.de/sag-renamed.pdf

I'm sure I missed a couple of Rs and some parts of the text would have to be changed.

mnieper commented 5 months ago

I did some rough, heuristic text-replacing on the foundations draft, you can see the result here:

https://felix-cherubini.de/sag-renamed.pdf

I'm sure I missed a couple of Rs and some parts of the text would have to be changed.

Thanks for this sanity check/test. As you wrote above, the $A$ type variables should be changed into something like $B$.

felixwellen commented 5 months ago

That would be work, so let's wait what everyone says to this version. Is $B$ really the best we can come up with? It is a bit weird to talk about a "An $\mathbb A$ -algebra B".

mnieper commented 5 months ago

Another suitable option is to rename our base ring to $\mathcal O$. This has the following advantages:

felixwellen commented 5 months ago

Since that is easy now:

https://felix-cherubini.de/sag-renamed-O.pdf

felixwellen commented 5 months ago

I think most people (including myself) are still somewhat inclined towards $R$, even though it looks like a variable.

mnieper commented 5 months ago

For people coming from algebraic geometry, $R$ is confusing because it does not behave as an object one would call $R$ in classical algebraic geometry. $\mathrm H^\ast(X, R)$, for example, looks like a coefficient group with constant coefficients but rather models $\mathrm H^\ast(X, \mathcal O)$. That $R$ is constant internally is not relevant; the syntax of the language should follow the intended semantics, which is, first and foremost, the model given by the big Zariski topos.

I currently don't see any advantage of $R$ except for hysterical raisins. I see no need to use the convention that is used in SDG for the real line (which fulfils many more properties and is a platonic ideal while our $R$ is just an instance).

felixwellen commented 5 months ago

Here is another one with non-italic plain R:

https://felix-cherubini.de/sag-renamed-R.pdf

I sympathize with the $\mathcal O$ though.

iblech commented 5 months ago

Since I was explicitly cc'ed: I don't have a strong opinion myself, especially because users of SAG can name things however they want. Just as users of the classical foundations of algebraic geometry can name their base $A$, $R$, $k$, $K$ etc. It makes sense to have a good default option, but local deviations (for instance in some of the sub-projects) are also fine.

I like Marc's general idea that the symbol should stand out.

Here is an argument for tending against $\mathcal{O}$: Related to what we have been discussing over at #26, our modules are more like the collection of fibers in classical algebraic geometry than the collection of stalks. The stalks are $\mathcal{O}_{X,x}$-modules while the fibers are $k(x)$-modules, where $k(x) = \mathcal{O}_{X,x}/\mathfrak{m}_x$. So using "$k$" instead of "$\mathcal{O}$" for the fiber situation is already an established practice. Also "$\mathcal{O}$" sounds more like "local ring which is not a field" while "$k$" screams "field". That our $R$ is a field is quite important, which is why I like that this property is reflected in the notation.

Lately I have come to like the position of embracing constant sheaves, viewing the sheaf topos more as an extension of the base topos instead of a totally separate alternative topos. By passing from sets to their induced constant sheaves, what we currently call external rings and our internal $R$ are on the same footing. With this picture in mind, it makes sense to have the symbol for $R$ depend on the symbol for the external base ring. For instance, we could write: "Let $A$ be a ring. Consider the generic local $A$-algebra $\mathbb{A}$. This algebra is a field and anonymously algebraically closed, hence..." Then, later in the text, some unrelated ring $B$ and its generic local algebra $\mathbb{B}$ might appear.