stacks tags

Stream: general

[Johan Commelin]

Top 35, with labels

00DV 119 algebra-lemma-NAK
01ZM 69 limits-lemma-descend-finite-presentation
02KH 64 coherent-lemma-flat-base-change-cohomology
06Z0 61 perfect-lemma-affine-compare-bounded
03H4 57 spaces-properties-lemma-points-cartesian
01XB 48 coherent-lemma-quasi-coherent-affine-cohomology-zero
00NX 47 algebra-lemma-finite-projective
01UA 46 morphisms-lemma-fppf-open
0149 41 derived-lemma-representable-homological
00DS 41 algebra-lemma-silly
01LC 40 schemes-lemma-push-forward-quasi-coherent
00E0 40 algebra-lemma-Zariski-topology
00MB 39 algebra-lemma-completion-flat
00EU 37 algebra-lemma-minimal-prime-reduced-ring
01T6 36 morphisms-lemma-finite-type-noetherian
00XR 36 sites-lemma-when-shriek
00U2 36 algebra-lemma-etale
03H6 34 spaces-properties-lemma-quasi-compact-affine-cover
01W6 34 morphisms-lemma-image-proper-scheme-closed
00NQ 34 algebra-lemma-regular-ring-CM
01Z4 33 limits-lemma-descend-opens
00HN 32 algebra-lemma-characterize-zero-local
001P 32 categories-lemma-yoneda
08J5 31 derived-remark-truncation-distinguished-triangle
01T2 31 morphisms-lemma-locally-finite-type-characterize
00KW 31 algebra-lemma-one-equation
07SK 29 spaces-limits-lemma-descend-finite-presentation
01WM 29 morphisms-lemma-integral-universally-closed
01U9 29 morphisms-lemma-base-change-flat
015J 29 derived-lemma-two-ss-complex-functor
04XB 28 stacks-properties-section-properties-morphisms
04KF 28 spaces-properties-lemma-describe-etale-local-ring
01WN 28 morphisms-lemma-finite-proper
00HL 28 algebra-lemma-flat-tor-zero
00HI 28 algebra-lemma-flat-base-change

[Johan Commelin]

A brief glance, we have NAKayama, yoneda, Zariski-topology. Most of the rest seems quite far away.

[Rob Lewis]

Johan Commelin said:

I think the chance that old tags rot is very small. So the main issue is that new things should get tagged. This will have to be a community effort. But I think it's ok if we do it in bursts.

But like you said there are a lot of stacks tags, and there are a lot of contributors here who don't know the project. How do these bursts work? Read all the stacks tags and remember what's been added to mathlib since the last iteration? Or look at a month of mathlib commits and see which ones might have corresponding tags?

[Rob Lewis]

Is there any chance of a new stacks tag that corresponds to something already in mathlib?

[Johan Commelin]

I think the latter chance is very small (but increasing?!)

[Johan Commelin]

Those bursts would have to be done by the algebraists in our community. Look through ring_theory/ and algebraic_geometry/ for lemmas that don't have @[stacks] but for which you expect that SP will have a tag for it.

[Rob Lewis]

Johan Commelin said:

I think the latter chance is very small (but increasing?!)

Do old tags ever get split? Like, ABC gets expanded and a lemma becomes DEF? That seems like the more likely way for this to happen.

[Johan Commelin]

They make a very strong effort to never change the statement of a tag (apart from cosmetic changes).

[Johan Commelin]

So if there is a split, my guess is that you'll get two new tags, and the old one will be "deprecated" (but still point to the old result, but not show up in their most rendering of the website)

[Rob Lewis]

Right, so if ABC is in mathlib and gets split into DEF and GHI, then DEF and GHI are new tags that are likely in mathlib

[Rob Lewis]

So you need to track changes on their end as well as ours

[Johan Commelin]

I think they maintain a list of deprecated tags. So part of a "burst" could be to check against that list.

[Johan Commelin]

#003W,categories-equation-fibred-groupoids-commutes
#003X,categories-equation-fibred-groupoids-commutes2
#Taken out as an exact duplicate of 00CR
#00DU,algebra-lemma-localize-colimit
#This equation was in a second proof 00EE which we removed
#00EL,algebra-equation-idempotent-exact-sequence
#Replaced proof by a new one avoiding this equation
#013L,derived-equation-new-star
#013M,derived-equation-star-star
#013Z,derived-remark-failure
#014T,derived-section-derived-triangulated
#014U,derived-definition-derived-triangulated
#0155,derived-lemma-ses-injective-ses
# Equations for relations between maps no longer needed because of
# vastly improve proof of Lemma Tag 01A6
#01A7,simplicial-equation-cd
#01A8,simplicial-equation-cs
# Changed coherent-remark-base-complex into lemma
# Changed coherent-remark-hypercoverings into lemma
#The following tag referred to a technical question whose answer is now in the
#stacks project, namely, it is answered by (the new version of) 01ZH
#01ZI,limits-remark-question-finite-type-necessary
# This section got moved to properies.tex
# This affects tags 01ZU, 01ZV, 01ZW, 01ZX, 01ZY

[Johan Commelin]

All the commented out tags are deprecated. :up: is the first chunk of about 100 such lines that grep found for me in tags/tags

[Rob Lewis]

So I'm not saying "don't do this," just trying to emphasize that this is a sustained maintenance effort that needs someone to lead the charge. Otherwise infrastructure will be built and forgotten and there will be a bunch of incomplete and outdated noise floating around.

[Kevin Buzzard]

OK I'll do it.

[Kevin Buzzard]

Stacks is becoming a canonical reference for commutative algebra for the young -- even the "standard" textbooks like Matsumura and Atiyah-Macdonald seem to be going out of fashion, because Stacks is online and looks beautiful, much better than the dodgy illegal pdfs (sometimes not even OCR'ed) which the UGs have of the classic books.

For me, moving into commutative algebra is a very natural next step for mathlib. Avigad has always pointed out how Lean is really dominating when it comes to algebra. Isabelle is still way ahead on analysis and of course Coq has the odd order theorem, however the odd order theorem is tons of lemmas about finite groups and some basic undergraduate representation theory, and this does not really add new users. If you look at what is coming out way, it's mathematicians appearing out of nowhere saying things like "let's do regular rings" or "let's do flat modules". Stacks is a perfect blueprint for this stuff.

I know the material well enough to even start breaking stuff up into "mini-projects", and I can probably be trusted to be diligent enough to make sure that things aren't broken. Disadvantages: I can't do any computer things. But I think that if the buck stops with me then this will be good enough for me to at least take responsibility for problems.

[Rob Lewis]

Another thing I mentioned when we talked about this a while back. This is a big human-curated formal-informal alignment, the ML people here should be drooling at the idea. It would probably be helpful to have a story for things that don't align perfectly -- humans can adapt easily enough, maybe machines could use something systematic?

[Johan Commelin]

I agree that we could try to at least have a bool that tracks whether things "obviously don't line up perfectly". But as you point out, since the definition of $\mathbb{N}$ doesn't line up, that basically means that almost everything that follows is infected by that virus.

[Johan Commelin]

So that bool should be applied with a bit of human wisdom...

[Kevin Buzzard]

One issue which I discovered recently is that when Bhavik was working on sheaves taking values in a general category, he had to cite things like "Stacks, remark between tag X and tag Y". For me the natural number thing is right now just noise. I know this sounds weird but actually the natural numbers in some sense do not show up much in this kind of mathematics. I took a good look through stacks when this convention was pointed out a few months back, and most of the uses of naturals just seemed to be as an arbitrary countably infinite index set. One of the few times naturals do show up as as dimensions of schemes, and certainly there are 0-dimensional schemes, so all that will be happening is that Stacks will sometimes say Z_{>=0}. We can translate this, as long as I'm overseeing stuff.

[Johan Commelin]

I guess we can make PRs to Stacks that add labels to "remark between tag X and tag Y", or rewrite that part of stacks to make things slightly more explicit. My guess is that Johan will be happy to receive such PRs.

[Kevin Buzzard]

I think we need to talk to Pieter Belmans about this (he's at Bonn, the same place as Scholze, so this is cool).

[Kevin Buzzard]

I had rather hoped that this term would be a bit quieter, but preparing my course has taken a lot of my time. It's over in three weeks though.

[Patrick Massot]

It reminds me: did we settle the crazy $\pi_0$ issue? I don't care what the Stacks project thinks here, there is now way we can keep the notation and name $\pi_0$ for something related but different from what the whole universe but the Stacks project calls $\pi_0$.

[Johan Commelin]

@Patrick Massot yes, that got fixed

[Johan Commelin]

It's now called connected_components

[Pieter Belmans]

Kevin Buzzard said:

I think we need to talk to Pieter Belmans about this (he's at Bonn, the same place as Scholze, so this is cool).

I'm now here! And my only interactions with Peter have been when I was in his way to the coffee machine, or he was in my way to the tea kettle, so don't read my association to Bonn in any way :)

[Kevin Buzzard]

So we think we have enough commutative algebra and category theory now to start thinking more seriously about integration of mathlib with the stacks project.

[Kevin Buzzard]

We've needed to do a bunch of category theory to get the definition of a condensed abelian group, and people followed the stacks project to do some of this; also commutative algebra is slowly but surely appearing (e.g. we have lots of facts about Jacobson rings and the NSS, with more in the pipeline) so maybe it's time to think about how to actually do this.

[Kevin Buzzard]

Right now at our end we are considering adding a stacks project attribute which we can attach to definitions and lemmas, pointing people to the corresponding stacks project tag.

[Johan Commelin]

and documentation tools could use the attribute to generate a dictionary json or such

[Kevin Buzzard]

One issue that showed up is this, a reference to a diagram here which didn't have a tag.

[Pieter Belmans]

it's really easy to assign a new tag to a useful equation which currently does not have one, and we should be able to convince Johan of this

[Kevin Buzzard]

If we are going to start doing something at our end, I guess it would be good to know whether you think it might be useful at your end, or at least usable if you want to use it in some way. I guess the dictionary could e.g. relate stacks tags to links to the mathlib API. Is there any particular thing which you want want to see or hope to see or whatever?

[Pieter Belmans]

that's not so much a question for me per se, but more for Johan: I don't know what kind of mathlib integration he foresees

[Pieter Belmans]

when I say Johan, I mean not this Johan, but the other Johan

[Pieter Belmans]

but I think having a visual clue about which tags have been formalised, and having a link to the mathlib documentation, seems like a good thing that I hope I can convince the other Johan of

[Pieter Belmans]

I don't quite know what the analogue of a tag is in mathlib, but having a uniform way of saying "this thing here corresponds to tag 0000" should be enough to allow for scraping the source code, and then we can set up a dictionary from that

[Rob Lewis]

The easy (from our end at least) kind of "integration" is just cross referencing. For various reasons it seems simpler to store the correspondences on the mathlib side, and then it's very simple to generate a map from mathlib declarations (or files, or locations in the docs) to stacks tags.

[Johan Commelin]

Yes, that's exactly what those attributes will do. Although it will quite likely be a many-to-one dictionary. With 5 mathlib declarations working together to get one Stacks tag.

[Rob Lewis]

I don't know if the correspondences are one-to-one or many-to-many or what.

[Johan Commelin]

For example "The following are equivalent" are typically broken into pieces in mathlib.

[Pieter Belmans]

yes, exactly, I think mathlib is the more unstable thing, and the arity of the correspondence is I guess the major thing to understand

[Pieter Belmans]

so the Stacks project website (or some overlay, or some separate website) could do several things:

• show that there is some kind of relationship between tags and mathlib code, without a serious commitment
• really commit to showing certain results

[Rob Lewis]

We have a reasonable API right now for getting a "display version" of a theorem statement. See https://leanprover-community.github.io/100.html , that's generated from https://github.com/leanprover-community/mathlib/blob/master/docs/100.yaml

[Rob Lewis]

So if you wanted to really display the formal statements (on the main website or another, whatever), it's easy to set up.

[Pieter Belmans]

here (or rather on some place like https://leanprover-community.github.io/mathlib_docs/ring_theory/nullstellensatz.html) you could easily add a link to the Stacks project website I guess, based on some decoration of the code, that is one thing

[Pieter Belmans]

I don't know whether Johan wants to display anything more than just a link on the Stacks project website

[Rob Lewis]

Right, we would definitely do that and it's pretty trivial to set up.

[Pieter Belmans]

one issue from the Stacks project POV is synchronisation: how and when will the website update, when updates to mathlib happen

[Pieter Belmans]

but I guess with some continuous integration magic (that you seem to have set up anyway) you can create say a JSON file with the up-to-date information, and that can be read by the Stacks project infrastructure

[Pieter Belmans]

so I'm imagining a single file giving a tag and then a file + line number + method name, and that would be the first thing for mathlib integration in the Stacks project website

[Pieter Belmans]

in the table of contents (see e.g. https://stacks.math.columbia.edu/tag/073W and expand) we can add an icon, indicating that there is a mathlib implementation (see the indication of a slogan on tag 074W)
on the page of a tag (see e.g. https://stacks.math.columbia.edu/tag/074W) we can have the precise link to mathlib

[Rob Lewis]

Pieter Belmans said:

so I'm imagining a single file giving a tag and then a file + line number + method name, and that would be the first thing for mathlib integration in the Stacks project website

Probably a list of files + line numbers + declaration names, but yeah! How often do you see the Stacks project infrastructure retrieving the database from our end?

[Pieter Belmans]

right now we are loading and caching an RSS file for the blog posts and GitHub commits once every hour or day

[Pieter Belmans]

I can check the precise caching settings, but I'd imagine something similar here: hitting it for every request is nonsense :)

[Pieter Belmans]

RSS cache is cleared once per hour

[Rob Lewis]

If the name of a tagged declaration in mathlib changes, links to the mathlib docs will break until you resync. But I guess this won't happen too often? We can handle declarations that move to a new file but keep the same name.

[Rob Lewis]

Links to the source code on github can point to a specific commit, so those can be stable.

[Pieter Belmans]

but any such change would trigger a rebuild of that particular file (i.e. the dictionary file), no?

[Rob Lewis]

Right, but links will be broken until you pull the new dictionary.

[Rob Lewis]

It's a rare event and the broken links won't last long so I'm not too worried about it.

[Pieter Belmans]

we'd only cache that for an hour or so, so I don't worry about those things being out of sync; the Stacks project is popular, but not _that_ popular that there'd be many confused people

[Rob Lewis]

@Johan Commelin @Kevin Buzzard is the mathlib-stacks correspondence many-to-one or many-to-many?

[Rob Lewis]

And is it necessary to have tags in module docs? Or only declarations?

[Rob Lewis]

If it's only declarations, I think it's probably better to use an @[stacks "ABC"] attribute to avoid making up and parsing new markdown syntax.

[Kevin Buzzard]

Sorry, I'm about to start a meeting. We could force it to be one-to-one but this would probably be a bad idea. One of the lemmas we formalised when doing schemes was a lemma about basic ring theory which had 22 parts (which became 22 lemmas in our project) and then said "..." afterwards!

[Kevin Buzzard]

On the other hand I am struggling to think of one definition or theorem in mathlib which could genuinely be tagged with more than one tag.

[Bryan Gin-ge Chen]

I think we will end up mentioning Stacks tags in module docs and docstrings even if we have the attributes, so we should have some convention for those citations too.

[Bhavik Mehta]

Kevin Buzzard said:

On the other hand I am struggling to think of one definition or theorem in mathlib which could genuinely be tagged with more than one tag.

The closest which comes to mind for me is this lemma, which is a generalisation of both https://stacks.math.columbia.edu/tag/0073 and https://stacks.math.columbia.edu/tag/00YR (a), in particular the former talks about sheaves on a space taking values in a nice concrete category, and the latter talks about sheaves on a site taking values in the same nice concrete category but with an extra assumption on it; whereas the Lean version talks about sheaves on a site taking values in a concrete category without the extra assumption

[Ruben Van de Velde]

So should the generalization get its own stacks tag?

[Pieter Belmans]

I don't think it makes sense to modify the Stacks project in such a way, based on a quickly developing formalisation project
it makes sense to take certain cues (e.g. to make referencing easier, adding tags for equations and informal discussions), but anything beyond that you will have a very hard time convincing Johan of

[Bhavik Mehta]

Yeah, I think for the sake of exposition the way Stacks does it right now is sensible - https://stacks.math.columbia.edu/tag/0073 is in the context of talking about sheaves on a space, and the part of https://stacks.math.columbia.edu/tag/00YR which is relevant is the first part in a series of six statements, where only the first doesn't need the extra assumption

[Kevin Buzzard]

I certainly agree that asking de Jong to change any of the exposition would be a very bad idea. "Can you please split this lemma into two because of some formaliser people" means having to go through everywhere where the lemma is used and understanding the mathematics again and then deciding how to rephrase stuff. I think that we have the flexibility to write our own library so that the correspondence is a simple one-tag-to-many-defs/theorems.

[Kevin Buzzard]

Here is tag 00E0 -- this should definitely not be one lemma in Lean!

[Kevin Buzzard]

Kenny proved all 17 statements though in our preliminary formalisation of the definition of a scheme.

[Pieter Belmans]

some of the issues you encounter here, such as this monstrosity lemma with 17 parts, are only happening at the beginning of the Stacks project: the stuff that an algebraic geometer likes to get away with in order to get cracking with the geometry

[Pieter Belmans]

(I have no idea how Stacks-aware people are, if I'm stating too many obvious things in my desire to explain the Stacks project, please tell!)

[Kevin Buzzard]

there are people here ranging from professional algebraic geometers to people doing post-docs in computer science topics who know a lot about mathlib documentation but have probably never even been to the stacks project website and don't know any alg geom at all, so feel free to say obvious-to-some-people things.

[Damiano Testa]

Would it make sense to prove lemmas in mathlib style, and, once a literal stacks statement can be proved, simply add that result in? In the 17 example above, after the 17 lemmas, prove another one that is simply the conjunction of the previous 17? This way, we can keep a 1-1 correspondence to something stable...

[Kevin Buzzard]

This is another possibility but, just as the stacks people will not want to change their 1 lemma into 17 lemmas because of the mathlib people, I don't think that the mathlib people will want a conjunction of 17 lemmas just because of the stacks people. Both communities are right now extremely successful in their own ways and one reason I believe for this is the extremely high level of attention which everything gets -- as you will know if you ever tried to PR one lemma and had about 5 people suggesting alternative proofs, putting it in a different namespace, a different file, adding three more lemmas, and actually perhaps completely refactoring something else so your lemma would not be necessary. I think it's best to not try and change either side of things and instead just do the best we can to show that they are doing related things.

[Kevin Buzzard]

An alternative approach is to start a new repo stacks-in-lean which does have these horrendous conjunctions in and has mathlib as a dependency, but for me this seems to be a far more painful solution -- it will need constant maintenance, for example, and in practice if someone wants to see a lemma which really _is_ directly in mathlib (and of course this sort of thing will happen a lot) they don't really want to be sent to some random other repo with mathlib as a dependency.

My gut feeling is that actually one should be liberal here. If there is a tag X in stacks which is mathematically trivially covered by e.g. the union of three lemmas in mathlib then those lemmas should get given the @[stacks X] attribute and also probably docstrings saying what they do in a way which a mathematician would understand.

[Kevin Buzzard]

@Rob Lewis I can envisage the following situation: stacks tag X proves lemma L assuming some ultimately superfluous extra hypothesis, and then using lemma L it proves in tag X' the correct lemma L' without the superfluous hypotheses. Mathlib uses a totally different approach so doesn't need to go via L. Nobody wants to see L in mathlib because there is no point. So now we want to tag our lemma L' with both stacks tag X and X', and perhaps explain in a comment or docstring why tag X leads to a proof which is strictly stronger than what is stated in X.

Also it is kind of clear that not all tags need to be formalised in mathlib. There might be useless intermediate lemmas proved in Stacks which are never used again other than in the proof of a bigger theorem, and the mathlib proof of the bigger theorem is different and doesn't go via the lemma. So a naive "we're not done until all the tags are formalised" approach is not right.

For me the main aim is not getting an AI to learn stacks via mathlib, and my impression is that AI stuff is happy to be sloppy anyway (cf Szegedy's comment that he doesn't care at all that the naturals start at 1 in stacks and 0 in Lean because it's all heuristics anyway). For me the aim is to see if this helps with search in stacks, which to be honest I find very poor. Example : where is the definition of an affine scheme? . But maybe this is a lousy example because affine schemes are probably everywhere in stacks.

[Damiano Testa]

Kevin, I agree. I think that being liberal in the referencing is perfectly ok and in fact, desirable. If a mathlib statement proves a commutative algebra assuming comm_semiring, while the one in stacks is about a comm_ring, I think that it is more than fair that they get the same tag!

[Damiano Testa]

In fact, should we call these... "stags"?

[Scott Morrison]

It sounds like we came to the conclusion that it is pretty close to a many(mathlib)-to-one(stacks), relationship, but possibly with some exceptions.

[Scott Morrison]

I remember in the elementary category theory stuff finding quite a few cases of misalignments, often when mathlib proved "the main part" of a stacks tag but omitted some minor point.

[Scott Morrison]

I'd propose that we be open to including these as cross references. Ideally on the mathlib side there will be a link back to the stacks tag along with a note "we don't do part e" or similar.

[Bryan Gin-ge Chen]

After the current doc-gen PR is merged, I'm planning to collect all the Stacks tag URLs / other tag-like patterns in docstrings and display those in a special section of the references page.

As I said above, even if we have attributes, we'll still be mentioning Stacks tags in the docstrings, so this effort should be complementary to whatever we decide for the stacks attribute.

[Mario Carneiro]

Why not something like @[stacks "01AB" "part (a,b,c)"] if we really want to keep track of sub-tag tracking in a machine readable way, and

/-- Foos the bar. Stacks project 01AB, part (a,b,c) -/
@[stacks "01AB"]
def ...

otherwise

[Damiano Testa]

In line with this stream, I updated one of my files to add an explicit reference to the Stacks Project. This is another one of those cases where I proved a part of the statement, but not the whole lemma.

PR #6322

[Pieter Belmans]

@Kevin Buzzard to find the definition of an affine scheme using the search, it is but a small thing to search for 'affine scheme definition' and limit yourself to statements (see https://stacks.math.columbia.edu/search?query=affine+scheme+definition&radius=statements): the name of the LaTeX environment is also being used in the plaintext search, and now the first result is indeed the definition of an affine scheme :)

[Kevin Buzzard]

I think that we still need to do some thinking about exactly what data we want to be collecting here. Right now I like Mario's suggestion. I also think that perhaps I was hasty yesterday saying "who cares about the machine learning people, let's just try and make killer search for theorems". I need to spend some time looking at all the examples we have, also also things we don't have but which I would see as minor success stories (e.g. proving some standard theorem about schemes which all alg geometers know, even if it's a standard basic one) and trying to imagine what the mathlib version would actually look like. So my gut feeling right now is just to start off with some detailed notes about what the actual correspondence between the two databases looks like. I am unlikely to find the time to do this before teaching finishes, which is in just under three weeks. @Scott Morrison I think you might have already tried something like this. Is there even some branch, which perhaps was already mentioned?

[Ruben Van de Velde]

A bit of a tangential thought: it might be interesting to generate a list of stacks tags that are not formalized, while all the tags they depend on are formalized

[Kevin Buzzard]

Yes, the "boundary" of what is done. One could imagine Patrick's flowchart tool thing being helpful here.

[Scott Morrison]

Kevin Buzzard said:

Scott Morrison I think you might have already tried something like this. Is there even some branch, which perhaps was already mentioned?

All the actual tagging done in the branch#stacks using @[stacks 01AB] has since been incorporated into mathlib using full URLs in doc-strings.

What that branch does still have it a script that scrapes all those doc-strings and produces a yaml file, ready for consumption by the stacks build process.

[Bryan Gin-ge Chen]

scripts/stacks_tags.lean and meta/stacks.lean get data from the stacks attribute, not the doc strings, right?