THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
A natural closure operator on sieves is a closure operator on sieve X for each X which commutes
We show that a Grothendieck topology J induces a natural closure operator, and define what the
closed sieves are. The collection of J-closed sieves forms a presheaf which is a sheaf for J,
and further this presheaf can be used to determine the Grothendieck topology from the sheaf
Finally we show that a natural closure operator on sieves induces a Grothendieck topology, and hence
that natural closure operators are in bijection with Grothendieck topologies.
category_theory.grothendieck_topology.closed: A sieve S on X is closed for the topology J
if it contains every arrow it covers.
category_theory.functor.closed_sieves: The presheaf sending X to the collection of J-closed
sieves on X. This is additionally shown to be a sheaf for J, and if this is a sheaf for a
different topology J', then J' ≤ J.
category_theory.grothendieck_topology.topology_of_closure_operator: A closure operator on the
set of sieves on every object which commutes with pullback additionally induces a Grothendieck
topology, giving a bijection with category_theory.grothendieck_topology.closure_operator.
A sieve is closed for the Grothendieck topology if it contains every arrow it covers.
In the case of the usual topology on a topological space, this means that the open cover contains
every open set which it covers.
Note this has no relation to a closed subset of a topological space.
A closure (increasing, inflationary and idempotent) operation on sieves that commutes with pullback
induces a Grothendieck topology.
In fact, such operations are in bijection with Grothendieck topologies.