Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-12-12 07:16
84f99388
View on Github →
feat(category_theory/sites): sheaves on types (
#5259
)
Estimated changes
Modified
src/category_theory/sites/sheaf.lean
added
theorem
category_theory.presieve.is_sheaf.is_sheaf_for
Created
src/category_theory/sites/types.lean
added
def
category_theory.discrete_presieve
added
def
category_theory.discrete_sieve
added
theorem
category_theory.discrete_sieve_mem
added
def
category_theory.eval
added
theorem
category_theory.eval_app
added
theorem
category_theory.eval_map
added
theorem
category_theory.eval_types_glue
added
theorem
category_theory.generate_discrete_presieve_mem
added
theorem
category_theory.is_sheaf_yoneda'
added
theorem
category_theory.subcanonical_types_grothendieck_topology
added
theorem
category_theory.types_glue_eval
added
def
category_theory.types_grothendieck_topology
added
theorem
category_theory.types_grothendieck_topology_eq_canonical
added
def
category_theory.yoneda'
added
theorem
category_theory.yoneda'_comp