Commit 2020-09-22 10:04 58d0bfcc

feat(topology/sheaves): alternate formulation of the sheaf condition (#4190) Currently the sheaf condition is stated as it often is in textbooks, e.g. https://stacks.math.columbia.edu/tag/0072. That is, it is about an equalizer of the two maps ∏ F.obj (U i) ⟶ ∏ F.obj (U i) ⊓ (U j). This PR adds an equivalent formulation, saying that F.obj (supr U) (with its natural projection maps) is the limit of the diagram consisting of the F.obj (U i) and the F.obj (U i ⊓ U j). I'd like to add further reformulations in subsequent PRs, in particular the nice one I saw in Lurie's SAG, just saying that F.obj (supr U) is the limit over the diagram of all F.obj V where V is an open subset of some U i. This version is actually much nicer to formalise, and I'm hoping we can translate over quite a lot of what we've already done about the sheaf condition to that version