[Merged by Bors] - feat(category_theory): Glue data #10436
Conversation
erdOne
commented
Nov 23, 2021
erdOne
commented
erdOne
added
awaiting-CI
erdOne
removed
the
awaiting-CI
| /-! | ||
| # Gluing data | ||
|
|
||
| We define `glue_data` as a family of data needed to glue topological spaces, schemes, etc. We |
There was a problem hiding this comment.
I have the vague feeling that this should instead be rephrased using coverings in a Grothendieck topology? Does that make sense? I haven't thought hard about this.
Instead of gluing objects in a glue_data, isn't the more general theorem something like: if a sheaf for a suitable topology is locally representable, then it is globally representable?
There was a problem hiding this comment.
The thing is that we do not have the glued space to take cover of in most of my use cases.
The statement you mentioned seems to me to be closer to the comparison lemma (we can glue sheaves on a cover that is somehow dense enough).
jcommelin
added
awaiting-author
Co-authored-by: Johan Commelin <johan@commelin.net>
erdOne
added
awaiting-review
jcommelin
added
awaiting-author
Co-authored-by: Johan Commelin <johan@commelin.net>
erdOne
added
awaiting-review
| (U : J → C) | ||
| (V : J × J → C) | ||
| (f : Π i j, V (i, j) ⟶ U i) | ||
| (f_mono : ∀ i j, mono (f i j) . tactic.apply_instance) |
There was a problem hiding this comment.
I'm a little unsure about this mono assumption. If I understand correctly, we will eventually want to apply this to the case of topological spaces and/or schemes, where these morphisms f i j are open immersions. But in general there are monomorphisms in these categories that need not be open immersions. What does this mono assumption give you at this level of generality? Does it make sense to relax this assumption for the purposes of this file?
Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
|
Let's just move forward with this PR. If it turns out we need to tweak it, we can refactor later. It's holding up cool stuff. Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
