-
Notifications
You must be signed in to change notification settings - Fork 331
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(CategoryTheory/Sites): 1-hypercovers #12803
Conversation
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
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.
I have no real objections about this, but I do wonder whether you considered going for arbitrary hypercovers (e.g. defining them using simplicial coskeleta). Do you have a particular use in mind for 1-hypercovers?
thanks! bors r+ |
This PR defines a notion of `1`-hypercovers in a category `C` equipped with a Grothendieck topology `J`. A covering of an object `S : C` consists of a family of maps `f i : X i ⟶ S` which generates a covering sieve. In the favourable case where the fibre products of `X i` and `X j` over `S` exist, the data of a `1`-hypercover consists of the data of objects `Y j` which cover these fibre products. We formalize this notion without assuming that these fibre products actually exists. If `F` is a sheaf and `E` is a `1`-hypercover of `S`, we show that `F.val.obj (op S)` is a multiequalizer of suitable maps `F.val.obj (op (X i)) ⟶ F.val.obj (op (Y j))`. Co-authored-by: Joël Riou <[email protected]>
I do not plan to PR an adhoc definition of 2-hypercovers! For general hypercovers, we could give a definition, but we would not be able to prove much about it until we make very significant progress on the formalization of the homotopy theory of simplicial sets. Among the possible applications, 1-hypercovers are useful in order to describe elements in the sheafification of a presheaf. I have introduced a universe parameter |
Pull request successfully merged into master. Build succeeded: |
This PR defines a notion of `1`-hypercovers in a category `C` equipped with a Grothendieck topology `J`. A covering of an object `S : C` consists of a family of maps `f i : X i ⟶ S` which generates a covering sieve. In the favourable case where the fibre products of `X i` and `X j` over `S` exist, the data of a `1`-hypercover consists of the data of objects `Y j` which cover these fibre products. We formalize this notion without assuming that these fibre products actually exists. If `F` is a sheaf and `E` is a `1`-hypercover of `S`, we show that `F.val.obj (op S)` is a multiequalizer of suitable maps `F.val.obj (op (X i)) ⟶ F.val.obj (op (Y j))`. Co-authored-by: Joël Riou <[email protected]>
This PR defines a notion of `1`-hypercovers in a category `C` equipped with a Grothendieck topology `J`. A covering of an object `S : C` consists of a family of maps `f i : X i ⟶ S` which generates a covering sieve. In the favourable case where the fibre products of `X i` and `X j` over `S` exist, the data of a `1`-hypercover consists of the data of objects `Y j` which cover these fibre products. We formalize this notion without assuming that these fibre products actually exists. If `F` is a sheaf and `E` is a `1`-hypercover of `S`, we show that `F.val.obj (op S)` is a multiequalizer of suitable maps `F.val.obj (op (X i)) ⟶ F.val.obj (op (Y j))`. Co-authored-by: Joël Riou <[email protected]>
This PR defines a notion of
1
-hypercovers in a categoryC
equipped with a Grothendieck topologyJ
. A covering of an objectS : C
consists of a family of mapsf i : X i ⟶ S
which generates a covering sieve. In the favourable case where the fibre products ofX i
andX j
overS
exist, the data of a1
-hypercover consists of the data of objectsY j
which cover these fibre products. We formalize this notion without assuming that these fibre products actually exists. IfF
is a sheaf andE
is a1
-hypercover ofS
, we show thatF.val.obj (op S)
is a multiequalizer of suitable mapsF.val.obj (op (X i)) ⟶ F.val.obj (op (Y j))
.