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

Created src/category_theory/sites/canonical.lean

added def category_theory.sheaf.canonical_topology

added def category_theory.sheaf.finest_topology

added def category_theory.sheaf.finest_topology_single

added theorem category_theory.sheaf.is_sheaf_for_bind

added theorem category_theory.sheaf.is_sheaf_for_trans

added theorem category_theory.sheaf.is_sheaf_of_representable

added theorem category_theory.sheaf.is_sheaf_yoneda_obj

added theorem category_theory.sheaf.le_finest_topology

added theorem category_theory.sheaf.sheaf_for_finest_topology

added theorem category_theory.sheaf.subcanonical.is_sheaf_of_representable

added theorem category_theory.sheaf.subcanonical.of_yoneda_is_sheaf

added def category_theory.sheaf.subcanonical

Modified src/category_theory/sites/sheaf.lean

Modified src/category_theory/sites/sieves.lean