New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(topology/sheaves): an equivalent sheaf condition #4538
Conversation
/-- | ||
The morphism from `V` to `U i` for some `i`. | ||
-/ | ||
def hom_to_index (V : opens_le_cover U) : V.val ⟶ U (index V) := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do you want to use .val
instead of the coe
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, there isn't a coe
unless we add one: Lean can't see that opens_le_cover
is a subtype right away. I'm dubious this actually gives us much.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ooh, you are completely right.
Thanks 🎉 bors merge |
Another condition equivalent to the sheaf condition: for every open cover `U`, `F.obj (supr U)` is the limit point of the diagram consisting of all the `F.obj V`, where `V ≤ U i` for some `i`. This condition is particularly straightforward to state, and makes some proofs easier (however we don't do this here: just prove the equivalence with the "official" definition). It's particularly nice because there is no case splitting (depending on whether you're looking at single or double intersections) when checking the sheaf condition. This is the statement Lurie uses in Spectral Algebraic Geometry. Later I may propose that we make this the official definition, but I'll wait to see how it pans out in actual use, first. For now it's just provided as yet another equivalent version of the sheaf condition. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Another condition equivalent to the sheaf condition: for every open cover `U`, `F.obj (supr U)` is the limit point of the diagram consisting of all the `F.obj V`, where `V ≤ U i` for some `i`. This condition is particularly straightforward to state, and makes some proofs easier (however we don't do this here: just prove the equivalence with the "official" definition). It's particularly nice because there is no case splitting (depending on whether you're looking at single or double intersections) when checking the sheaf condition. This is the statement Lurie uses in Spectral Algebraic Geometry. Later I may propose that we make this the official definition, but I'll wait to see how it pans out in actual use, first. For now it's just provided as yet another equivalent version of the sheaf condition. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Another condition equivalent to the sheaf condition: for every open cover
U
,F.obj (supr U)
is the limit point of the diagram consisting of all theF.obj V
, whereV ≤ U i
for somei
.This condition is particularly straightforward to state, and makes some proofs easier (however we don't do this here: just prove the equivalence with the "official" definition). It's particularly nice because there is no case splitting (depending on whether you're looking at single or double intersections) when checking the sheaf condition.
This is the statement Lurie uses in Spectral Algebraic Geometry.
Later I may propose that we make this the official definition, but I'll wait to see how it pans out in actual use, first. For now it's just provided as yet another equivalent version of the sheaf condition.