Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-27 14:25 c82b7082

View on Github →

feat(category_theory/sites): the canonical topology on a category (#4928) Explicitly construct the finest topology for which the given presheaves are sheaves, and specialise to construct the canonical topology. Also one or two tiny changes which should have been there before

Estimated changes