Sheafification for TopCat.Presheaf

Stream: mathlib4

[Brian Nugent]

Currently there are two versions of sheafification in mathlib. There is TopCat.Presheaf.sheafify which is for sheaves of Types on a topological space and there is CategoryTheory.presheafToSheaf which is for any presheaf on a site. The one for TopCat doesn't seemed to be used anywhere and it seems like it could be replaced by the more general one.
Also, would people want all of the more general definitions ported over to the TopCat setting? If so, I can open a PR for it.

[Joël Riou]

It seems the file Topology.Sheaves.Sheafify is not imported by any other file.
I believe that whenever it is possible, the definitions and proofs should be done in the context of general sites, and we could provide a specialized API for topological spaces which just refers to the general API via definitions.
There are still a few things for which we do not yet have all the necessary general API, like stalks. I introduced the notion of Point of a site in #31859, and @Christian Merten and I have been developing a little bit more about points/fiber functors. At some point, some of the topological constructions for stalks may also be refactored.

[Joël Riou]

There is now a bunch of PRs related to points of general sites: #35806, #35773, #35572, #35757, #35175, #35722, #35136, #35719, #35715, #35680 and #35584.
I would like to emphasize #35584 which gives a way to show that the category of sheaves with values in a monoidal category is monoidal when the site has enough points (this was previously known to mathlib only in the case we have an internal hom of (pre)sheaves). Following #35773, I intend to show in a future PR that the same applies to categories of sheaves of modules. Ultimately, this will allow constructing the tensor product of quasi-coherent sheaves on a scheme.
This still needs a lot of cleaning up, but when all of this is merged, it will be possible to make most of the existing API for sheaves on topological spaces a particular case of the API for sheaves on general sites.