mathlib
9e1e4f01 - feat(category_theory/sites/*): Dense subsite (#9694)

Commit
4 years ago
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 `ℱ ⟶ ℱ'`. Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com> Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Author
Parents
Loading