[Merged by Bors] - feat(category_theory/sites/plus): P⁺ for a presheaf P.
#10284
Conversation
adamtopaz
added
awaiting-CI
github-actions
bot
removed
the
awaiting-CI
|
|
||
| instance : inhabited (J.cover X) := ⟨⊤⟩ | ||
|
|
||
| /-- An auxiliary structure, used to define `S.index` in `plus.lean`. -/ |
There was a problem hiding this comment.
These names L and R are very "unreadable". If you only plan to use this in plus.lean, I would suggest moving them there, and marking them as implementation detail. If you want to expose them to others, maybe we can cook up a more descriptive name + docstring?
There was a problem hiding this comment.
I think I want to keep these definitions in this file, since they will be used is sheaf.lean in my next PR. (Actually, I just shuffled some things around and moved the cover.index definition from plus.lean to grothendieck.lean for the same reason).
The names L and R are meant to match the fields in cover.index which in turn match the fields in multicospan_index, so that's one possible argument for keeping them. Although I agree they're not very descriptive... I'll try to come up with a better name.
There was a problem hiding this comment.
Okay! I renamed S.L -> S.arrow and S.R -> S.relation for S : J.cover X.
src/category_theory/sites/plus.lean
Outdated
| /-- The canonical map from `P` to `J.plus.obj P`. | ||
| See `to_plus` for a functorial version. -/ | ||
| @[simps] | ||
| def map_to_plus : P ⟶ (J.plus D).obj P := |
There was a problem hiding this comment.
map sounds to much like you are mapping something through a functor or homomorphism. So I thought this might be to_plus.app, but dot-notation is also not ideal. At the same time, you want to reserve to_plus_app for simps. Would to_plus_on_obj be a compromise?
| def map_to_plus : P ⟶ (J.plus D).obj P := | |
| def to_plus_on_obj : P ⟶ (J.plus D).obj P := |
There was a problem hiding this comment.
I agree the name is not ideal. I also realized that there were some @simps generated lemmas like plus_obj_2 because of naming collisions, so I renamed a few things. I'm happy to change the names again if needed.
|
|
||
| instance : inhabited (J.cover X) := ⟨⊤⟩ | ||
|
|
||
| /-- An auxiliary structure, used to define `S.index` in `plus.lean`. -/ |
github-actions
bot
added
ready-to-merge
This file adds the construction of `P⁺`, for a presheaf `P : Cᵒᵖ ⥤ D`, whenever `C` has a Grothendieck topology `J` and `D` has the appropriate (co)limits. Later, we will show that `P⁺⁺` is the sheafification of `P`, under certain additional hypotheses on `D`. See https://stacks.math.columbia.edu/tag/00W1
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
P⁺ for a presheaf P.P⁺ for a presheaf P.
This file adds the construction of
P⁺, for a presheafP : Cᵒᵖ ⥤ D, wheneverChas a Grothendieck topologyJandDhas the appropriate (co)limits.Later, we will show that
P⁺⁺is the sheafification ofP, under certain additional hypotheses onD.See https://stacks.math.columbia.edu/tag/00W1