Sites, sheaves and sheafification as a QIT #1031
Conversation
thanks to Ingo Blechschmidt!
| (patch : ⟨ cov ⟩) → | ||
| restrict (patchArr cov patch) (amalgamate cover fam) ≡ fst fam patch | ||
|
|
||
| F : Presheaf C (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) ℓP) |
There was a problem hiding this comment.
Should this not have a more descriptive name, like sheafification?
There was a problem hiding this comment.
The exposed name is Sheafification.F. Do you think it should still be called sheafification inside the named module Sheafification?
There was a problem hiding this comment.
I guess you don't expect/want people to open the module Sheafification? If you had a coverage J in context, it could be convenient to write open Sheafification J and then for any presheaf P write sheafification P instead of Sheafification.F J P. In that case it would probably be best to make F⟅_⟆ private.
There was a problem hiding this comment.
I think I actually went for a named module precisely to give users the option to open it with arguments (either just J or both J and P). So let's go with sheafification and isSheafSheafification, right?
There was a problem hiding this comment.
Side remark: I can think of the following notations for sheafification in the literature, which seem not very helpful either.
-
$a$ (for "associated sheaf functor") [MacLane, Moerdijk: Sheaves in Geometry an Logic] -
$i^*$ (because it is the inverse image part of the geometric morphism$i$ from sheaves to presheaves)
There was a problem hiding this comment.
it would probably be best to make
F⟅_⟆private.
That also makes all the constructors of the HIT private, unfortunately. At least I can't find a way to mark only the name ⟨F⟅_⟆⟩ as private.
So I guess I should rename it to ⟨sheafification⟅_⟆⟩.
There was a problem hiding this comment.
I replaced all Fs now (that stood for a sheafification). Good like that?
There was a problem hiding this comment.
Yeah, looks good to me, but it is of course a purely stylistic matter. There are instances of both in the library, named modules with short names, like f for a certain function, and named modules with terms that have essentially the same name as the module (intended to opened). I don't want to advocate too heavily for one of the options, but if everyone is happy now, we can leave things as they are, I would say.
| (patch : ⟨ cov ⟩) → | ||
| restrict (patchArr cov patch) (amalgamate cover fam) ≡ fst fam patch | ||
|
|
||
| F : Presheaf C (ℓ-max (ℓ-max (ℓ-max (ℓ-max ℓ ℓ') ℓcov) ℓpat) ℓP) |
There was a problem hiding this comment.
I guess you don't expect/want people to open the module Sheafification? If you had a coverage J in context, it could be convenient to write open Sheafification J and then for any presheaf P write sheafification P instead of Sheafification.F J P. In that case it would probably be best to make F⟅_⟆ private.
|
@mzeuner I think I handled everything now! |
|
I think the PR is ready to be merged @mortberg @felixwellen |
|
Nice! |
|
Note to my future self: it would probably have been smarter to split this PR into two (1. sites, 2. sheafification). :-) |
|
Looks good to me (just skimming - two people already looked at it). |
This PR provides a definition of a coverage on a category (turning it into a site) and formulates the sheaf condition (amalgamation property) for presheaves on such a site. Furthermore, the sheafification of a presheaf on a site is constructed by means of a quotient inductive type (QIT), and the appropriate universal property is shown.