Commit 2020-10-17 13:41 25d83437

feat(topology/sheaves): an equivalent sheaf condition (#4538) Another condition equivalent to the sheaf condition: for every open cover U, F.obj (supr U) is the limit point of the diagram consisting of all the F.obj V, where V ≤ U i for some i. This condition is particularly straightforward to state, and makes some proofs easier (however we don't do this here: just prove the equivalence with the "official" definition). It's particularly nice because there is no case splitting (depending on whether you're looking at single or double intersections) when checking the sheaf condition. This is the statement Lurie uses in Spectral Algebraic Geometry. Later I may propose that we make this the official definition, but I'll wait to see how it pans out in actual use, first. For now it's just provided as yet another equivalent version of the sheaf condition.