Commit 2020-09-11 11:35 0c57b2da

doc(category_theory): add doc-strings and links to the stacks project (#4107) We'd been discussing adding a @[stacks "007B"] tag to add cross-references to the stacks project (and possibly include links back again -- they say they're keen). I'm not certain that we actually have the documentation maintenance enthusiasm to make this viable, so this PR is a more lightweight solution: adding lots of links to the stacks project from doc-strings. I'd be very happy to switch back to the attribute approach later. This is pretty close to exhaustive for the "category theory preliminaries" chapter of the stacks project, but doesn't attempt to go beyond that. I've only included links where we formalise all, or almost all (in which case I've usually left a note), of the corresponding tag.