# The canonical topology on a category #

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 finestTopologySingle 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 finestTopology 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 canonicalTopology: 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 #

theorem CategoryTheory.Sheaf.isSheafFor_bind {C : Type u} {X : C} (P : ) (U : ) (B : Y : C⦄ → f : Y X⦄ → U.arrows f) (hU : CategoryTheory.Presieve.IsSheafFor P U.arrows) (hB : ∀ ⦃Y : C⦄ ⦃f : Y X⦄ (hf : U.arrows f), CategoryTheory.Presieve.IsSheafFor P (B hf).arrows) (hB' : ∀ ⦃Y : C⦄ ⦃f : Y X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z Y), CategoryTheory.Presieve.IsSeparatedFor P ().arrows) :

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 isSheafFor_trans. Adapted from [Joh02], Lemma C2.1.7(i) with suggestions as mentioned in https://math.stackexchange.com/a/358709/

theorem CategoryTheory.Sheaf.isSheafFor_trans {C : Type u} {X : C} (P : ) (R : ) (S : ) (hR : CategoryTheory.Presieve.IsSheafFor P R.arrows) (hR' : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, S.arrows f) (hS : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, R.arrows f) :

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 finestTopology. Adapted from [Joh02], Lemma C2.1.7(ii) with suggestions as mentioned in https://math.stackexchange.com/a/358709

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
• One or more equations did not get rendered due to their size.
Instances For

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
• = sInf (CategoryTheory.Sheaf.finestTopologySingle '' Ps)
Instances For
theorem CategoryTheory.Sheaf.sheaf_for_finestTopology {C : Type u} {P : } (Ps : Set ()) (h : P Ps) :

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

theorem CategoryTheory.Sheaf.le_finestTopology {C : Type u} (Ps : Set ()) (hJ : PPs, ) :

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

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

Equations
Instances For
theorem CategoryTheory.Sheaf.isSheaf_yoneda_obj {C : Type u} (X : C) :
CategoryTheory.Presieve.IsSheaf (CategoryTheory.yoneda.obj X)

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

theorem CategoryTheory.Sheaf.isSheaf_of_representable {C : Type u} (P : ) [P.Representable] :

A representable functor is a sheaf for the canonical topology.

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
Instances For
theorem CategoryTheory.Sheaf.Subcanonical.of_yoneda_isSheaf {C : Type u} (h : ∀ (X : C), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)) :

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

theorem CategoryTheory.Sheaf.Subcanonical.isSheaf_of_representable {C : Type u} (P : ) [P.Representable] :

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

@[simp]
theorem CategoryTheory.Sheaf.Subcanonical.yoneda_obj_val {C : Type u} (X : C) :
(hJ.yoneda.obj X).val = CategoryTheory.yoneda.obj X
@[simp]
theorem CategoryTheory.Sheaf.Subcanonical.yoneda_map_val {C : Type u} :
∀ {X Y : C} (f : X Y), (hJ.yoneda.map f).val = CategoryTheory.yoneda.map f

If J is subcanonical, we obtain a "Yoneda" functor from the defining site into the sheaf category.

Equations
• hJ.yoneda = { obj := fun (X : C) => { val := CategoryTheory.yoneda.obj X, cond := }, map := fun {X Y : C} (f : X Y) => { val := CategoryTheory.yoneda.map f }, map_id := , map_comp := }
Instances For
def CategoryTheory.Sheaf.Subcanonical.yonedaCompSheafToPresheaf {C : Type u} :
hJ.yoneda.comp CategoryTheory.yoneda

The yoneda embedding into the presheaf category factors through the one to the sheaf category.

Equations
Instances For
def CategoryTheory.Sheaf.Subcanonical.yonedaFullyFaithful {C : Type u} :
hJ.yoneda.FullyFaithful

The yoneda functor into the sheaf category is fully faithful

Equations
• hJ.yonedaFullyFaithful = CategoryTheory.Yoneda.fullyFaithful.ofCompFaithful
Instances For
Equations
• =
Equations
• =