The canonical topology on a category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the finest (largest) Grothendieck topology for which a given presheaf P is a sheaf. This is well defined since if P is a sheaf for a topology J, then it is a sheaf for any coarser (smaller) topology. Nonetheless we define the topology explicitly by specifying its sieves: A sieve S on X is covering for finest_topology_single P iff for any f : Y ⟶ X, P satisfies the sheaf axiom for S.pullback f. Showing that this is a genuine Grothendieck topology (namely that it satisfies the transitivity axiom) forms the bulk of this file.

This generalises to a set of presheaves, giving the topology finest_topology Ps which is the finest topology for which every presheaf in Ps is a sheaf. Using Ps as the set of representable presheaves defines the canonical_topology: the finest topology for which every representable is a sheaf.

A Grothendieck topology is called subcanonical if it is smaller than the canonical topology, equivalently it is subcanonical iff every representable presheaf is a sheaf.

References #

source

theorem category_theory.sheaf.is_sheaf_for_bind {C : Type u} [category_theory.category C] {X : C} (P : Cᵒᵖ ⥤ Type v) (U : category_theory.sieve X) (B : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⇑U f → category_theory.sieve Y) (hU : category_theory.presieve.is_sheaf_for P ⇑U) (hB : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : ⇑U f), category_theory.presieve.is_sheaf_for P ⇑(B hf)) (hB' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : ⇑U f) ⦃Z : C⦄ (g : Z ⟶ Y), category_theory.presieve.is_separated_for P ⇑(category_theory.sieve.pullback g (B h))) :

category_theory.presieve.is_sheaf_for P ⇑(category_theory.sieve.bind ⇑U B)

To show P is a sheaf for the binding of U with B, it suffices to show that P is a sheaf for U, that P is a sheaf for each sieve in B, and that it is separated for any pullback of any sieve in B.

This is mostly an auxiliary lemma to show is_sheaf_for_trans. Adapted from [Joh02], Lemma C2.1.7(i) with suggestions as mentioned in https://math.stackexchange.com/a/358709/

source

theorem category_theory.sheaf.is_sheaf_for_trans {C : Type u} [category_theory.category C] {X : C} (P : Cᵒᵖ ⥤ Type v) (R S : category_theory.sieve X) (hR : category_theory.presieve.is_sheaf_for P ⇑R) (hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⇑S f → category_theory.presieve.is_separated_for P ⇑(category_theory.sieve.pullback f R)) (hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, ⇑R f → category_theory.presieve.is_sheaf_for P ⇑(category_theory.sieve.pullback f S)) :

category_theory.presieve.is_sheaf_for P ⇑S

Given two sieves R and S, to show that P is a sheaf for S, we can show:

P is a sheaf for R
P is a sheaf for the pullback of S along any arrow in R
P is separated for the pullback of R along any arrow in S.

This is mostly an auxiliary lemma to construct finest_topology. Adapted from [Joh02], Lemma C2.1.7(ii) with suggestions as mentioned in https://math.stackexchange.com/a/358709

source

def category_theory.sheaf.finest_topology_single {C : Type u} [category_theory.category C] (P : Cᵒᵖ ⥤ Type v) :

category_theory.grothendieck_topology C

Construct the finest (largest) Grothendieck topology for which the given presheaf is a sheaf.

This is a special case of https://stacks.math.columbia.edu/tag/00Z9, but following a different proof (see the comments there).

Equations

category_theory.sheaf.finest_topology_single P = {sieves := λ (X : C) (S : category_theory.sieve X), ∀ (Y : C) (f : Y ⟶ X), category_theory.presieve.is_sheaf_for P ⇑(category_theory.sieve.pullback f S), top_mem' := _, pullback_stable' := _, transitive' := _}

source

def category_theory.sheaf.finest_topology {C : Type u} [category_theory.category C] (Ps : set (Cᵒᵖ ⥤ Type v)) :

category_theory.grothendieck_topology C

Construct the finest (largest) Grothendieck topology for which all the given presheaves are sheaves.

This is equal to the construction of https://stacks.math.columbia.edu/tag/00Z9.

Equations

category_theory.sheaf.finest_topology Ps = has_Inf.Inf (category_theory.sheaf.finest_topology_single '' Ps)

source

theorem category_theory.sheaf.sheaf_for_finest_topology {C : Type u} [category_theory.category C] {P : Cᵒᵖ ⥤ Type v} (Ps : set (Cᵒᵖ ⥤ Type v)) (h : P ∈ Ps) :

category_theory.presieve.is_sheaf (category_theory.sheaf.finest_topology Ps) P

Check that if P ∈ Ps, then P is indeed a sheaf for the finest topology on Ps.

source

theorem category_theory.sheaf.le_finest_topology {C : Type u} [category_theory.category C] (Ps : set (Cᵒᵖ ⥤ Type v)) (J : category_theory.grothendieck_topology C) (hJ : ∀ (P : Cᵒᵖ ⥤ Type v), P ∈ Ps → category_theory.presieve.is_sheaf J P) :

J ≤ category_theory.sheaf.finest_topology Ps

Check that if each P ∈ Ps is a sheaf for J, then J is a subtopology of finest_topology Ps.

source

def category_theory.sheaf.canonical_topology (C : Type u) [category_theory.category C] :

category_theory.grothendieck_topology C

The canonical_topology on a category is the finest (largest) topology for which every representable presheaf is a sheaf.

See https://stacks.math.columbia.edu/tag/00ZA

Equations

category_theory.sheaf.canonical_topology C = category_theory.sheaf.finest_topology (set.range category_theory.yoneda.obj)

source

theorem category_theory.sheaf.is_sheaf_yoneda_obj {C : Type u} [category_theory.category C] (X : C) :

category_theory.presieve.is_sheaf (category_theory.sheaf.canonical_topology C) (category_theory.yoneda.obj X)

yoneda.obj X is a sheaf for the canonical topology.

source

theorem category_theory.sheaf.is_sheaf_of_representable {C : Type u} [category_theory.category C] (P : Cᵒᵖ ⥤ Type v) [P.representable] :

category_theory.presieve.is_sheaf (category_theory.sheaf.canonical_topology C) P

A representable functor is a sheaf for the canonical topology.

source

def category_theory.sheaf.subcanonical {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) :

Prop

A subcanonical topology is a topology which is smaller than the canonical topology. Equivalently, a topology is subcanonical iff every representable is a sheaf.

Equations

category_theory.sheaf.subcanonical J = (J ≤ category_theory.sheaf.canonical_topology C)

source

theorem category_theory.sheaf.subcanonical.of_yoneda_is_sheaf {C : Type u} [category_theory.category C] (J : category_theory.grothendieck_topology C) (h : ∀ (X : C), category_theory.presieve.is_sheaf J (category_theory.yoneda.obj X)) :

category_theory.sheaf.subcanonical J

If every functor yoneda.obj X is a J-sheaf, then J is subcanonical.

source

theorem category_theory.sheaf.subcanonical.is_sheaf_of_representable {C : Type u} [category_theory.category C] {J : category_theory.grothendieck_topology C} (hJ : category_theory.sheaf.subcanonical J) (P : Cᵒᵖ ⥤ Type v) [P.representable] :

category_theory.presieve.is_sheaf J P

If J is subcanonical, then any representable is a J-sheaf.