In the post I will discuss some features of the full text search we have available in the Stacks project website.

Basic usage: Just type in some keywords and hit return.

Notational convention: |search&*^term| means you typed exactly “search&*^term” into the search bar and hit return.

1. By default search looks for what you typed case insensitive in statements of lemmas, propositions, theorems, remarks, equations, examples, and situations.
2. It looks for words exactly how you typed them. So |stack| does not find occurrences of “stacks”. The solution is to put a wildcard at the end |stack*|.
3. Non-alphanumeric characters have special meaning, so try to avoid them. For example |quasi-compact| searches for statements which include the word “quasi” but do not have the word “compact”.
4. Using double quotes is special: For example |”quasi-compact”| will find statements including the hyphenated word “quasi-compact”.
5. If you check the box “Include proofs” it will also look in proofs.
6. If you check the box “Include sections”, then it will look in the text of sections, as well as the statements as above. This will return duplicate results, but if you did not have success with searching in statements this can be useful.

Advanced usage: There are other things you can do. I haven’t figured out all of them yet, and I’ll document more here over time. Leave a comment if you found a useful feature I haven’t mentioned. Here it goes (with more useful searches listed first):

1. The OR operator works: |”smooth morphism” OR “etale morphism”| will search for statemens containing either “smooth morphism” or “etale morphism”.
2. There is an AND operator which you can combine with the OR operator: |Noetherian AND “ring map” OR “etale morphism”|.
3. Precedence of set operators: “-“, “OR”, “AND”.
4. There is a NEAR operator: |locally NEAR/0 finite| and |locally NEAR/1 finite|. This finds occurrences of “locally” and “finite” 0 respectively 1 words apart in either order. You can also combine this with a wildcard, so |locally NEAR/1 finite*| finds both “locally of finite” and “locally finitely” which is useful.
5. Try |”\text{.*}”| or |”\label{.*}”|. This works, but I don’t know why. Do you?
6. Double quotes work across lines: |”ordinal whose cofinality”| finds a proposition whose statement has “ordinal” on one line and “whose cofinality” on the second.
7. Wildcards do not work at the beginning of words.

Of course, I should go and read the documentation. And so should you!

Conclusion. Search is a very useful tool to quickly find results containing some given keywords.

However the Stacks project is a text written by humans and not computer generated. Thus it doesn’t contain all possible true statements… Example: suppose you wanted to find the result “a finite morphism is separated” or “a finite morphism is universally closed”. The obvious searches wouldn’t find these. Namely, the first is in the text directly following the definition of a finite morphism, in Section Tag 01WG. The second is an immediate consequence of either Lemma Tag 01WM or Lemma Tag 01WN.

This brings up a whole other topic, namely, to what extend we should add lemmas stating formal consequences of previous lemmas. This turns out to be quite useful, especially for results earlier in the Stacks project. What do you think?