mathlib3

189e0662 - feat(category_theory/sites/sheafification): The sheafification of a presheaf. (#10303)

feat(category_theory/sites/sheafification): The sheafification of a presheaf. (#10303) We construct the sheafification of a presheaf `P` taking values in a concrete category `D` with enough (co)limits, where the forgetful functor preserves the appropriate (co)limits and reflects isomorphisms. We follow the construction on the stacks project https://stacks.math.columbia.edu/tag/00W1 **Note:** There are two very long proofs here, so I added several comments explaining what's going on.