Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-16 17:42 64abe5aa

View on Github →

feat(category_theory/sites): closed sieves (#5282)

closed sieves
closure of a sieve
subobject classifier in Sheaf (without proof of universal property)
equivalent sheaf condition iff same topology
closure operator induces topology

Estimated changes

Created src/category_theory/sites/closed.lean

added theorem category_theory.classifier_is_sheaf

added def category_theory.functor.closed_sieves

added def category_theory.grothendieck_topology.close

added theorem category_theory.grothendieck_topology.close_close

added theorem category_theory.grothendieck_topology.close_eq_self_of_is_closed

added theorem category_theory.grothendieck_topology.close_eq_top_iff_mem

added theorem category_theory.grothendieck_topology.close_is_closed

added theorem category_theory.grothendieck_topology.closed_iff_closed

added def category_theory.grothendieck_topology.closure_operator

added theorem category_theory.grothendieck_topology.covers_iff_mem_of_closed

added def category_theory.grothendieck_topology.is_closed

added theorem category_theory.grothendieck_topology.is_closed_iff_close_eq_self

added theorem category_theory.grothendieck_topology.is_closed_pullback

added theorem category_theory.grothendieck_topology.le_close

added theorem category_theory.grothendieck_topology.le_close_of_is_closed

added theorem category_theory.grothendieck_topology.monotone_close

added theorem category_theory.grothendieck_topology.pullback_close

added theorem category_theory.le_topology_of_closed_sieves_is_sheaf

added theorem category_theory.topology_eq_iff_same_sheaves

added def category_theory.topology_of_closure_operator

added theorem category_theory.topology_of_closure_operator_close

added theorem category_theory.topology_of_closure_operator_self

Modified src/order/closure.lean

added def closure_operator.mk'