[Merged by Bors] - doc(category_theory): add doc-strings and links to the stacks project #4107
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
semorrison
added
the
awaiting-review
jcommelin
reviewed
Sep 11, 2020
| The three main structures involved are | ||
| * `is_limit c`, for `c : cone F`, `F : J ⥤ C`, expressing that `c` is a limit cone, | ||
| * `limit_cone F`, which consists of a choice of cone for `F` and the fact it is a limit cone, and | ||
| * `has_limit F`, asserting the mere existence of some limit cone for `F`. |
There was a problem hiding this comment.
This docstring morally depends on the prop-limits branch, right?
There was a problem hiding this comment.
err... Yes!
I realise also that I've now written a module doc for limits/limits.lean both on this branch, and on that branch! I guess when one gets merged, I'll merge conflicts and pick the best sentences from each. :-)
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Sep 11, 2020
…#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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.