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

Created src/category_theory/sites/dense_subsite.lean

added theorem category_theory.cover_dense.ext

added theorem category_theory.cover_dense.functor_pullback_pushforward_covering

added def category_theory.cover_dense.hom_over

added theorem category_theory.cover_dense.iso_of_restrict_iso

added def category_theory.cover_dense.iso_over

added def category_theory.cover_dense.presheaf_iso

added def category_theory.cover_dense.restrict_hom_equiv_hom

added def category_theory.cover_dense.sheaf_coyoneda_hom

added theorem category_theory.cover_dense.sheaf_eq_amalgamation

added def category_theory.cover_dense.sheaf_hom

added theorem category_theory.cover_dense.sheaf_hom_eq

added theorem category_theory.cover_dense.sheaf_hom_restrict_eq

added def category_theory.cover_dense.sheaf_iso

added def category_theory.cover_dense.sheaf_yoneda_hom

added def category_theory.cover_dense.types.app_hom

added theorem category_theory.cover_dense.types.app_hom_restrict

added theorem category_theory.cover_dense.types.app_hom_valid_glue

added def category_theory.cover_dense.types.app_iso

added def category_theory.cover_dense.types.presheaf_hom

added def category_theory.cover_dense.types.presheaf_iso

added def category_theory.cover_dense.types.pushforward_family

added theorem category_theory.cover_dense.types.pushforward_family_apply

added theorem category_theory.cover_dense.types.pushforward_family_compatible

added def category_theory.cover_dense.types.sheaf_iso

added structure category_theory.cover_dense

added def category_theory.presieve.cover_by_image

added structure category_theory.presieve.cover_by_image_structure

added theorem category_theory.presieve.in_cover_by_image

added def category_theory.sieve.cover_by_image