Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-12 07:25 9e1e4f01

View on Github →

feat(category_theory/sites/*): Dense subsite (#9694) Defined cover_dense functors as functors into sites such that each object can be covered by images of the functor. Proved that for a cover_dense functor G, any morphisms of presheaves G ⋙ ℱ ⟶ G ⋙ ℱ' can be glued into a morphism ℱ ⟶ ℱ'.

Estimated changes