mathlib

b8fb47c4 - refactor(topology/sheaves): Redefine sheaves in terms of Grothendieck topology. (#15384)

refactor(topology/sheaves): Redefine sheaves in terms of Grothendieck topology. (#15384) We change the "official definition" of sheaves over topological spaces from the equalizer diagram condition to the condition in terms of the Grothendieck topology on `Opens(X)`. The benefit is that 1. The `X.Sheaf C` category is now defeq to `(opens.grothendieck_topology X).Sheaf C`, so that functors between categories of sheaves over sites could be specialized onto topological spaces without the abundant equivalences. 2. It allows sheaves over spaces to value in arbitrary categories that doesn't have all products. The original sheaf condition is now called `presheaf.is_sheaf_equalizer_products`, and `presheaf.is_sheaf_iff_is_sheaf_equalizer_products` (in `topology.sheaves.sheaf_condition.sites`) shows that the two are equivalent. Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>