Commit 2023-05-22 03:13 6f371680

View on Github →

feat: Add CategoryTheory.Sites.Coverage (#4113) This PR adds the notion of a coverage, and constructs the natural Galois insertion between coverages and Grothendieck topologies. We also show that a Type _-valued presheaf is a sheaf for a coverage if and only if it is a sheaf for the associated Grothendieck topology.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Coverage.lean

added theorem CategoryTheory.Coverage.eq_top_pullback

added def CategoryTheory.Coverage.gi

added def CategoryTheory.Coverage.ofGrothendieck

added theorem CategoryTheory.Coverage.ofGrothendieck_iff

added inductive CategoryTheory.Coverage.saturate

added theorem CategoryTheory.Coverage.saturate_of_superset

added def CategoryTheory.Coverage.toGrothendieck

added theorem CategoryTheory.Coverage.toGrothendieck_eq_sInf

added structure CategoryTheory.Coverage

added def CategoryTheory.Presieve.FactorsThru

added def CategoryTheory.Presieve.FactorsThruAlong

added theorem CategoryTheory.Presieve.factorsThruAlong_id

added theorem CategoryTheory.Presieve.factorsThru_of_le

added theorem CategoryTheory.Presieve.factorsThru_top

added theorem CategoryTheory.Presieve.isSheafFor_of_factorsThru

added theorem CategoryTheory.Presieve.isSheaf_coverage

added theorem CategoryTheory.Presieve.le_of_factorsThru_sieve