Commit 2021-11-15 05:07 189e0662

View 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 Note: There are two very long proofs here, so I added several comments explaining what's going on.

Estimated changes