mathlib3 documentation

category_theory.sites.closed

Closed sieves #

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 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 #

category_theory.grothendieck_topology.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.
category_theory.grothendieck_topology.closure_operator: The bundled closure_operator given by category_theory.grothendieck_topology.close.
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.

Tags #

closed sieve, closure, Grothendieck topology

References #

S. MacLane, I. Moerdijk, Sheaves in Geometry and Logic

def category_theory.grothendieck_topology.close {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} (S : category_theory.sieve X) :

category_theory.sieve X

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

Equations

J₁.close S = {arrows := λ (Y : C) (f : Y ⟶ X), J₁.covers S f, downward_closed' := _}

@[simp]

theorem category_theory.grothendieck_topology.close_apply {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} (S : category_theory.sieve X) (Y : C) (f : Y ⟶ X) :

⇑(J₁.close S) f = J₁.covers S f

theorem category_theory.grothendieck_topology.le_close {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} (S : category_theory.sieve X) :

S ≤ J₁.close S

Any sieve is smaller than its closure.

def category_theory.grothendieck_topology.is_closed {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} (S : category_theory.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

J₁.is_closed S = ∀ ⦃Y : C⦄ (f : Y ⟶ X), J₁.covers S f → ⇑S f

theorem category_theory.grothendieck_topology.covers_iff_mem_of_closed {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} {S : category_theory.sieve X} (h : J₁.is_closed S) {Y : C} (f : Y ⟶ X) :

J₁.covers S f ↔ ⇑S f

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

theorem category_theory.grothendieck_topology.is_closed_pullback {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X Y : C} (f : Y ⟶ X) (S : category_theory.sieve X) :

J₁.is_closed S → J₁.is_closed (category_theory.sieve.pullback f S)

Being J-closed is stable under pullback.

theorem category_theory.grothendieck_topology.le_close_of_is_closed {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} {S T : category_theory.sieve X} (h : S ≤ T) (hT : J₁.is_closed T) :

J₁.close S ≤ T

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

theorem category_theory.grothendieck_topology.close_is_closed {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} (S : category_theory.sieve X) :

J₁.is_closed (J₁.close S)

The closure of a sieve is closed.

theorem category_theory.grothendieck_topology.is_closed_iff_close_eq_self {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} (S : category_theory.sieve X) :

J₁.is_closed S ↔ J₁.close S = S

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

theorem category_theory.grothendieck_topology.close_eq_self_of_is_closed {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} {S : category_theory.sieve X} (hS : J₁.is_closed S) :

J₁.close S = S

theorem category_theory.grothendieck_topology.pullback_close {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X Y : C} (f : Y ⟶ X) (S : category_theory.sieve X) :

J₁.close (category_theory.sieve.pullback f S) = category_theory.sieve.pullback f (J₁.close S)

Closing under J is stable under pullback.

theorem category_theory.grothendieck_topology.monotone_close {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} :

monotone J₁.close

@[simp]

theorem category_theory.grothendieck_topology.close_close {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} (S : category_theory.sieve X) :

J₁.close (J₁.close S) = J₁.close S

theorem category_theory.grothendieck_topology.close_eq_top_iff_mem {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} (S : category_theory.sieve X) :

J₁.close S = ⊤ ↔ S ∈ ⇑J₁ X

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

def category_theory.grothendieck_topology.closure_operator {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) (X : C) :

closure_operator (category_theory.sieve X)

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

Equations

J₁.closure_operator X = closure_operator.mk' J₁.close _ _ _

@[simp]

theorem category_theory.grothendieck_topology.closure_operator_apply_apply {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) (X : C) (S : category_theory.sieve X) (Y : C) (f : Y ⟶ X) :

⇑(⇑(J₁.closure_operator X) S) f = J₁.covers S f

@[simp]

theorem category_theory.grothendieck_topology.closed_iff_closed {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) {X : C} (S : category_theory.sieve X) :

S ∈ (J₁.closure_operator X).closed ↔ J₁.is_closed S

@[simp]

theorem category_theory.functor.closed_sieves_obj {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) (X : Cᵒᵖ) :

(category_theory.functor.closed_sieves J₁).obj X = {S // J₁.is_closed S}

@[simp]

theorem category_theory.functor.closed_sieves_map_coe {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) (X Y : Cᵒᵖ) (f : X ⟶ Y) (S : {S // J₁.is_closed S}) :

↑((category_theory.functor.closed_sieves J₁).map f S) = category_theory.sieve.pullback f.unop S.val

def category_theory.functor.closed_sieves {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) :

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

category_theory.functor.closed_sieves J₁ = {obj := λ (X : Cᵒᵖ), {S // J₁.is_closed S}, map := λ (X Y : Cᵒᵖ) (f : X ⟶ Y) (S : {S // J₁.is_closed S}), ⟨category_theory.sieve.pullback f.unop S.val, _⟩, map_id' := _, map_comp' := _}

theorem category_theory.classifier_is_sheaf {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) :

category_theory.presieve.is_sheaf J₁ (category_theory.functor.closed_sieves J₁)

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

theorem category_theory.le_topology_of_closed_sieves_is_sheaf {C : Type u} [category_theory.category C] {J₁ J₂ : category_theory.grothendieck_topology C} (h : category_theory.presieve.is_sheaf J₁ (category_theory.functor.closed_sieves J₂)) :

J₁ ≤ J₂

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

theorem category_theory.topology_eq_iff_same_sheaves {C : Type u} [category_theory.category C] {J₁ J₂ : category_theory.grothendieck_topology C} :

J₁ = J₂ ↔ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), category_theory.presieve.is_sheaf J₁ P ↔ category_theory.presieve.is_sheaf J₂ P

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

@[simp]

theorem category_theory.topology_of_closure_operator_sieves {C : Type u} [category_theory.category C] (c : Π (X : C), closure_operator (category_theory.sieve X)) (hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : category_theory.sieve X), ⇑(c Y) (category_theory.sieve.pullback f S) = category_theory.sieve.pullback f (⇑(c X) S)) (X : C) :

⇑(category_theory.topology_of_closure_operator c hc) X = {S : category_theory.sieve X | ⇑(c X) S = ⊤}

def category_theory.topology_of_closure_operator {C : Type u} [category_theory.category C] (c : Π (X : C), closure_operator (category_theory.sieve X)) (hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : category_theory.sieve X), ⇑(c Y) (category_theory.sieve.pullback f S) = category_theory.sieve.pullback f (⇑(c X) S)) :

category_theory.grothendieck_topology 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

category_theory.topology_of_closure_operator c hc = {sieves := λ (X : C), {S : category_theory.sieve X | ⇑(c X) S = ⊤}, top_mem' := _, pullback_stable' := _, transitive' := _}

theorem category_theory.topology_of_closure_operator_self {C : Type u} [category_theory.category C] (J₁ : category_theory.grothendieck_topology C) :

category_theory.topology_of_closure_operator J₁.closure_operator _ = J₁

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

theorem category_theory.topology_of_closure_operator_close {C : Type u} [category_theory.category C] (c : Π (X : C), closure_operator (category_theory.sieve X)) (pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : category_theory.sieve X), ⇑(c Y) (category_theory.sieve.pullback f S) = category_theory.sieve.pullback f (⇑(c X) S)) (X : C) (S : category_theory.sieve X) :

(category_theory.topology_of_closure_operator c pb).close S = ⇑(c X) S