Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-18 09:31 7cc6b53f

View on Github →

feat(category_theory/sites): sheaves on a grothendieck topology (#4608) Broken off from #4577.

Estimated changes

Modified docs/references.bib

Modified src/category_theory/limits/shapes/types.lean

added theorem category_theory.limits.types.type_equalizer_iff_unique

Created src/category_theory/sites/sheaf.lean

added def category_theory.equalizer.first_obj

added def category_theory.equalizer.first_obj_eq_family

added def category_theory.equalizer.fork_map

added theorem category_theory.equalizer.presieve.compatible_iff

added def category_theory.equalizer.presieve.first_map

added def category_theory.equalizer.presieve.second_map

added def category_theory.equalizer.presieve.second_obj

added theorem category_theory.equalizer.presieve.sheaf_condition

added theorem category_theory.equalizer.presieve.w

added theorem category_theory.equalizer.sieve.compatible_iff

added theorem category_theory.equalizer.sieve.equalizer_sheaf_condition

added def category_theory.equalizer.sieve.first_map

added def category_theory.equalizer.sieve.second_map

added def category_theory.equalizer.sieve.second_obj

added theorem category_theory.equalizer.sieve.w

added theorem category_theory.presieve.compatible_iff_sieve_compatible

added theorem category_theory.presieve.extend_agrees

added theorem category_theory.presieve.extend_restrict

added theorem category_theory.presieve.extension_iff_amalgamation

added theorem category_theory.presieve.family_of_elements.compatible.restrict

added theorem category_theory.presieve.family_of_elements.compatible.sieve_extend

added theorem category_theory.presieve.family_of_elements.compatible.to_sieve_compatible

added def category_theory.presieve.family_of_elements.compatible

added def category_theory.presieve.family_of_elements.is_amalgamation

added def category_theory.presieve.family_of_elements.pullback_compatible

added def category_theory.presieve.family_of_elements.restrict

added def category_theory.presieve.family_of_elements.sieve_compatible

added def category_theory.presieve.family_of_elements

added theorem category_theory.presieve.is_amalgamation_restrict

added theorem category_theory.presieve.is_amalgamation_sieve_extend

added theorem category_theory.presieve.is_compatible_of_exists_amalgamation

added def category_theory.presieve.is_separated

added theorem category_theory.presieve.is_separated_for.ext

added theorem category_theory.presieve.is_separated_for.is_sheaf_for

added def category_theory.presieve.is_separated_for

added theorem category_theory.presieve.is_separated_for_and_exists_is_amalgamation_iff_sheaf_for

added theorem category_theory.presieve.is_separated_for_iff_generate

added theorem category_theory.presieve.is_separated_for_top

added def category_theory.presieve.is_sheaf

added theorem category_theory.presieve.is_sheaf_for.is_amalgamation

added theorem category_theory.presieve.is_sheaf_for.is_separated_for

added theorem category_theory.presieve.is_sheaf_for.valid_glue

added def category_theory.presieve.is_sheaf_for

added theorem category_theory.presieve.is_sheaf_for_coarser_topology

added theorem category_theory.presieve.is_sheaf_for_iff_generate

added theorem category_theory.presieve.is_sheaf_for_iso

added theorem category_theory.presieve.is_sheaf_for_singleton_iso

added theorem category_theory.presieve.is_sheaf_for_subsieve

added theorem category_theory.presieve.is_sheaf_for_subsieve_aux

added theorem category_theory.presieve.is_sheaf_for_top_sieve

added theorem category_theory.presieve.is_sheaf_iso

added theorem category_theory.presieve.is_sheaf_pretopology

added theorem category_theory.presieve.is_sheaf_yoneda

added def category_theory.presieve.nat_trans_equiv_compatible_family

added theorem category_theory.presieve.pullback_compatible_iff

added theorem category_theory.presieve.restrict_extend

added theorem category_theory.presieve.restrict_inj

added theorem category_theory.presieve.separated_of_sheaf

added theorem category_theory.presieve.yoneda_condition_iff_sheaf_condition

added def category_theory.presieve.yoneda_sheaf_condition