Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 19:47 ba43124c

View on Github →

feat(category_theory/sites/*): Comparison lemma (#9785)

Estimated changes

Modified src/category_theory/sites/cover_lifting.lean

modified theorem category_theory.Ran_is_sheaf_of_cover_lifting

added theorem category_theory.comp_cover_lifting

deleted def category_theory.comp_cover_lifting

modified structure category_theory.cover_lifting

added theorem category_theory.id_cover_lifting

deleted def category_theory.id_cover_lifting

added def category_theory.sites.copullback

added def category_theory.sites.pullback_copullback_adjunction

Modified src/category_theory/sites/dense_subsite.lean

added def category_theory.cover_dense.Sheaf_equiv_of_cover_preserving_cover_lifting

added theorem category_theory.cover_dense.compatible_preserving

Created src/category_theory/sites/induced_topology.lean

added def category_theory.cover_dense.Sheaf_equiv

added def category_theory.cover_dense.induced_topology

added theorem category_theory.cover_dense.locally_cover_dense

added def category_theory.locally_cover_dense.induced_topology

added theorem category_theory.locally_cover_dense.induced_topology_cover_lifting

added theorem category_theory.locally_cover_dense.induced_topology_cover_preserving

added theorem category_theory.locally_cover_dense.pushforward_cover_iff_cover_pullback

added def category_theory.locally_cover_dense

added theorem category_theory.over_forget_locally_cover_dense

Modified src/category_theory/sites/sieves.lean

modified theorem category_theory.sieve.functor_pushforward_bot

added theorem category_theory.sieve.functor_pushforward_top