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

• CategoryTheory.GrothendieckTopology.close: Sends a sieve S on X to the set of arrows which it covers. This has all the usual properties of a closure operator, as well as commuting with pullback.
• CategoryTheory.GrothendieckTopology.closureOperator: The bundled ClosureOperator given by CategoryTheory.GrothendieckTopology.close.
• CategoryTheory.GrothendieckTopology.IsClosed: A sieve S on X is closed for the topology J if it contains every arrow it covers.
• CategoryTheory.Functor.closedSieves: 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.
• CategoryTheory.topologyOfClosureOperator: A closure operator on the set of sieves on every object which commutes with pullback additionally induces a Grothendieck topology, giving a bijection with CategoryTheory.GrothendieckTopology.closureOperator.

Tags

closed sieve, closure, Grothendieck topology

References

• [S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic][MM92]

@[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), (CategoryTheory.GrothendieckTopology.close J₁ S).arrows f = CategoryTheory.GrothendieckTopology.Covers J₁ S f

def CategoryTheory.GrothendieckTopology.close {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.Sieve X

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

Equations

• CategoryTheory.GrothendieckTopology.close J₁ S = { arrows := fun (x : C) (f : x ⟶ X) => CategoryTheory.GrothendieckTopology.Covers J₁ S f, downward_closed := ⋯ }

theorem CategoryTheory.GrothendieckTopology.le_close {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Sieve X) : S ≤ CategoryTheory.GrothendieckTopology.close J₁ S

Any sieve is smaller than its closure.

def CategoryTheory.GrothendieckTopology.IsClosed {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Sieve X) : Prop

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

• CategoryTheory.GrothendieckTopology.IsClosed J₁ S = ∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.GrothendieckTopology.Covers J₁ S f → S.arrows f

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 : CategoryTheory.GrothendieckTopology.IsClosed J₁ S) {Y : C} (f : Y ⟶ X) : CategoryTheory.GrothendieckTopology.Covers J₁ S f ↔ S.arrows f

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

theorem CategoryTheory.GrothendieckTopology.isClosed_pullback {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} {Y : C} (f : Y ⟶ X) (S : CategoryTheory.Sieve X) : CategoryTheory.GrothendieckTopology.IsClosed J₁ S → CategoryTheory.GrothendieckTopology.IsClosed J₁ (CategoryTheory.Sieve.pullback f S)

Being J-closed is stable under pullback.

theorem CategoryTheory.GrothendieckTopology.le_close_of_isClosed {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} {S : CategoryTheory.Sieve X} {T : CategoryTheory.Sieve X} (h : S ≤ T) (hT : CategoryTheory.GrothendieckTopology.IsClosed J₁ T) : CategoryTheory.GrothendieckTopology.close J₁ S ≤ T

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

theorem CategoryTheory.GrothendieckTopology.close_isClosed {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.GrothendieckTopology.IsClosed J₁ (CategoryTheory.GrothendieckTopology.close J₁ S)

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) : (CategoryTheory.GrothendieckTopology.closureOperator J₁ X).IsClosed S = CategoryTheory.GrothendieckTopology.IsClosed J₁ S

def CategoryTheory.GrothendieckTopology.closureOperator {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) (X : C) : ClosureOperator (CategoryTheory.Sieve X)

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

Equations

• CategoryTheory.GrothendieckTopology.closureOperator J₁ X = ClosureOperator.ofPred (CategoryTheory.GrothendieckTopology.close J₁) (CategoryTheory.GrothendieckTopology.IsClosed J₁) ⋯ ⋯ ⋯

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

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

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

theorem CategoryTheory.GrothendieckTopology.pullback_close {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} {Y : C} (f : Y ⟶ X) (S : CategoryTheory.Sieve X) : CategoryTheory.GrothendieckTopology.close J₁ (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f (CategoryTheory.GrothendieckTopology.close J₁ S)

Closing under J is stable under pullback.

theorem CategoryTheory.GrothendieckTopology.monotone_close {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} : Monotone (CategoryTheory.GrothendieckTopology.close J₁)

@[simp]

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

theorem CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C} (S : CategoryTheory.Sieve X) : CategoryTheory.GrothendieckTopology.close J₁ S = ⊤ ↔ S ∈ J₁.sieves X

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

@[simp]

theorem CategoryTheory.Functor.closedSieves_map_coe {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (S : { S : CategoryTheory.Sieve X.unop // CategoryTheory.GrothendieckTopology.IsClosed J₁ S }), ↑((CategoryTheory.Functor.closedSieves J₁).map f S) = CategoryTheory.Sieve.pullback f.unop ↑S

@[simp]

theorem CategoryTheory.Functor.closedSieves_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) (X : Cᵒᵖ) : (CategoryTheory.Functor.closedSieves J₁).obj X = { S : CategoryTheory.Sieve X.unop // CategoryTheory.GrothendieckTopology.IsClosed J₁ S }

def CategoryTheory.Functor.closedSieves {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) : CategoryTheory.Functor Cᵒᵖ (Type (max v u))

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.

theorem CategoryTheory.classifier_isSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) : CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₁)

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

theorem CategoryTheory.le_topology_of_closedSieves_isSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J₁ : CategoryTheory.GrothendieckTopology C} {J₂ : CategoryTheory.GrothendieckTopology C} (h : CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₂)) : J₁ ≤ J₂

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.

theorem CategoryTheory.topology_eq_iff_same_sheaves {C : Type u} [CategoryTheory.Category.{v, u} C] {J₁ : CategoryTheory.GrothendieckTopology C} {J₂ : CategoryTheory.GrothendieckTopology C} : J₁ = J₂ ↔ ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))), CategoryTheory.Presieve.IsSheaf J₁ P ↔ CategoryTheory.Presieve.IsSheaf J₂ P

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

@[simp]

theorem CategoryTheory.topologyOfClosureOperator_sieves {C : Type u} [CategoryTheory.Category.{v, u} C] (c : (X : C) → ClosureOperator (CategoryTheory.Sieve X)) (hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X), (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S)) (X : C) : (CategoryTheory.topologyOfClosureOperator c hc).sieves X = {S : CategoryTheory.Sieve X | (c X) S = ⊤}

def CategoryTheory.topologyOfClosureOperator {C : Type u} [CategoryTheory.Category.{v, u} C] (c : (X : C) → ClosureOperator (CategoryTheory.Sieve X)) (hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X), (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S)) : CategoryTheory.GrothendieckTopology C

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

• CategoryTheory.topologyOfClosureOperator c hc = { sieves := fun (X : C) => {S : CategoryTheory.Sieve X | (c X) S = ⊤}, top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }

theorem CategoryTheory.topologyOfClosureOperator_self {C : Type u} [CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) : CategoryTheory.topologyOfClosureOperator (CategoryTheory.GrothendieckTopology.closureOperator J₁) ⋯ = J₁

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

theorem CategoryTheory.topologyOfClosureOperator_close {C : Type u} [CategoryTheory.Category.{v, u} C] (c : (X : C) → ClosureOperator (CategoryTheory.Sieve X)) (pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X), (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S)) (X : C) (S : CategoryTheory.Sieve X) : CategoryTheory.GrothendieckTopology.close (CategoryTheory.topologyOfClosureOperator c pb) S = (c X) S