Commit 2021-11-15 05:07 189e0662View on Github →
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.