Documentation

Mathlib.CategoryTheory.Sites.Closed

Closed sieves #

A natural closure operator on sieves is a closure operator on Sieve X for each X which commutes with pullback. 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 predicate. 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.

Main definitions #

Tags #

closed sieve, closure, Grothendieck topology

References #

@[simp]
theorem CategoryTheory.GrothendieckTopology.close_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Sieve X) :
∀ (x : C) (f : x X), (J₁.close S).arrows f = J₁.Covers S f

The J-closure of a sieve is the collection of arrows which it covers.

Equations
  • J₁.close S = { arrows := fun (x : C) (f : x X) => J₁.Covers S f, downward_closed := }
Instances For

    Any sieve is smaller than its closure.

    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.

    Equations
    • J₁.IsClosed S = ∀ ⦃Y : C⦄ (f : Y X), J₁.Covers S fS.arrows f
    Instances For
      theorem CategoryTheory.GrothendieckTopology.covers_iff_mem_of_isClosed {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} {S : CategoryTheory.Sieve X} (h : J₁.IsClosed S) {Y : C} (f : Y X) :
      J₁.Covers S f S.arrows f

      If S is J₁-closed, then S covers exactly the arrows it contains.

      Being J-closed is stable under pullback.

      The closure of a sieve S is the largest closed sieve which contains S (justifying the name "closure").

      The closure of a sieve is closed.

      @[simp]
      theorem CategoryTheory.GrothendieckTopology.closureOperator_isClosed {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) (X : C) (S : CategoryTheory.Sieve X) :
      (J₁.closureOperator X).IsClosed S = J₁.IsClosed S

      A Grothendieck topology induces a natural family of closure operators on sieves.

      Equations
      Instances For

        The sieve S is closed iff its closure is equal to itself.

        Closing under J is stable under pullback.

        @[simp]
        theorem CategoryTheory.GrothendieckTopology.close_close {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Sieve X) :
        J₁.close (J₁.close S) = J₁.close S

        The sieve S is in the topology iff its closure is the maximal sieve. This shows that the closure operator determines the topology.

        The presheaf sending each object to the set of J-closed sieves on it. This presheaf is a J-sheaf (and will turn out to be a subobject classifier for the category of J-sheaves).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The presheaf of J-closed sieves is a J-sheaf. The proof of this is adapted from [MM92], Chapter III, Section 7, Lemma 1.

          If presheaf of J₁-closed sieves is a J₂-sheaf then J₁ ≤ J₂. Note the converse is true by classifier_isSheaf and isSheaf_of_le.

          If being a sheaf for J₁ is equivalent to being a sheaf for J₂, then J₁ = J₂.

          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.

          Equations
          Instances For

            The topology given by the closure operator J.close on a Grothendieck topology is the same as J.