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

• https://ncatlab.org/nlab/show/canonical+topology
• https://ncatlab.org/nlab/show/subcanonical+coverage
• https://stacks.math.columbia.edu/tag/00Z9
• https://math.stackexchange.com/a/358709/

theorem CategoryTheory.Sheaf.isSheafFor_bind {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type v)) (U : CategoryTheory.Sieve X) (B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → CategoryTheory.Sieve Y) (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 (CategoryTheory.Sieve.pullback g (B h)).arrows) : CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.bind U.arrows B).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} [CategoryTheory.Category.{v, u} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type v)) (R S : CategoryTheory.Sieve X) (hR : CategoryTheory.Presieve.IsSheafFor P R.arrows) (hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f R).arrows) (hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) : CategoryTheory.Presieve.IsSheafFor P S.arrows

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

def CategoryTheory.Sheaf.finestTopologySingle {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v)) : CategoryTheory.GrothendieckTopology 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

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

def CategoryTheory.Sheaf.finestTopology {C : Type u} [CategoryTheory.Category.{v, u} C] (Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type v))) : CategoryTheory.GrothendieckTopology 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

• CategoryTheory.Sheaf.finestTopology Ps = sInf (CategoryTheory.Sheaf.finestTopologySingle '' Ps)

theorem CategoryTheory.Sheaf.sheaf_for_finestTopology {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type v)} (Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type v))) (h : P ∈ Ps) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.finestTopology Ps) P

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} [CategoryTheory.Category.{v, u} C] (Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type v))) (J : CategoryTheory.GrothendieckTopology C) (hJ : ∀ P ∈ Ps, CategoryTheory.Presieve.IsSheaf J P) : J ≤ CategoryTheory.Sheaf.finestTopology Ps

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

def CategoryTheory.Sheaf.canonicalTopology (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.GrothendieckTopology C

The canonicalTopology 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

• CategoryTheory.Sheaf.canonicalTopology C = CategoryTheory.Sheaf.finestTopology (Set.range CategoryTheory.yoneda.obj)

theorem CategoryTheory.Sheaf.isSheaf_yoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.canonicalTopology C) (CategoryTheory.yoneda.obj X)

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

theorem CategoryTheory.Sheaf.isSheaf_of_isRepresentable {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v)) [P.IsRepresentable] : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.canonicalTopology C) P

A representable functor is a sheaf for the canonical topology.

class CategoryTheory.GrothendieckTopology.Subcanonical {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology 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.

• le_canonical : J ≤ CategoryTheory.Sheaf.canonicalTopology C

theorem CategoryTheory.GrothendieckTopology.le_canonical {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J ≤ CategoryTheory.Sheaf.canonicalTopology C

instance CategoryTheory.GrothendieckTopology.instSubcanonicalCanonicalTopology {C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Sheaf.canonicalTopology C).Subcanonical

Equations

• ⋯ = ⋯

theorem CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (h : ∀ (X : C), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)) : J.Subcanonical

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

theorem CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] (P : CategoryTheory.Functor Cᵒᵖ (Type v)) [P.IsRepresentable] : CategoryTheory.Presieve.IsSheaf J P

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

def CategoryTheory.GrothendieckTopology.yoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : CategoryTheory.Functor C (CategoryTheory.Sheaf J (Type v))

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

Equations

• J.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 := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.yoneda_map_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (J.yoneda.map f).val = CategoryTheory.yoneda.map f

@[simp]

theorem CategoryTheory.GrothendieckTopology.yoneda_obj_val {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] (X : C) : (J.yoneda.obj X).val = CategoryTheory.yoneda.obj X

def CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.comp (CategoryTheory.sheafToPresheaf J (Type v)) ≅ CategoryTheory.yoneda

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

Equations

• J.yonedaCompSheafToPresheaf = CategoryTheory.Iso.refl (J.yoneda.comp (CategoryTheory.sheafToPresheaf J (Type ?u.54)))

def CategoryTheory.GrothendieckTopology.yonedaFullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.FullyFaithful

The yoneda functor into the sheaf category is fully faithful

Equations

• J.yonedaFullyFaithful = CategoryTheory.Yoneda.fullyFaithful.ofCompFaithful

instance CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.Full

Equations

• ⋯ = ⋯

instance CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.Faithful

Equations

• ⋯ = ⋯

@[deprecated CategoryTheory.GrothendieckTopology.Subcanonical]

def CategoryTheory.Sheaf.Subcanonical {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : Prop

Alias of CategoryTheory.GrothendieckTopology.Subcanonical.

---

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

• @CategoryTheory.Sheaf.Subcanonical = @CategoryTheory.GrothendieckTopology.Subcanonical

@[deprecated CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj]

theorem CategoryTheory.Sheaf.Subcanonical.of_isSheaf_yoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (h : ∀ (X : C), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)) : J.Subcanonical

Alias of CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj.

---

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

@[deprecated CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable]

theorem CategoryTheory.Sheaf.Subcanonical.isSheaf_of_isRepresentable {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] (P : CategoryTheory.Functor Cᵒᵖ (Type v)) [P.IsRepresentable] : CategoryTheory.Presieve.IsSheaf J P

Alias of CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable.

---

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

@[deprecated CategoryTheory.GrothendieckTopology.yoneda]

def CategoryTheory.Sheaf.Subcanonical.yoneda {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : CategoryTheory.Functor C (CategoryTheory.Sheaf J (Type v))

Alias of CategoryTheory.GrothendieckTopology.yoneda.

---

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

Equations

• @CategoryTheory.Sheaf.Subcanonical.yoneda = @CategoryTheory.GrothendieckTopology.yoneda

@[deprecated CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf]

def CategoryTheory.Sheaf.Subcanonical.yonedaCompSheafToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.comp (CategoryTheory.sheafToPresheaf J (Type v)) ≅ CategoryTheory.yoneda

Alias of CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf.

---

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

Equations

• @CategoryTheory.Sheaf.Subcanonical.yonedaCompSheafToPresheaf = @CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf

@[deprecated CategoryTheory.GrothendieckTopology.yonedaFullyFaithful]

def CategoryTheory.Sheaf.Subcanonical.yonedaFullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) [J.Subcanonical] : J.yoneda.FullyFaithful

Alias of CategoryTheory.GrothendieckTopology.yonedaFullyFaithful.

---

The yoneda functor into the sheaf category is fully faithful

Equations

• @CategoryTheory.Sheaf.Subcanonical.yonedaFullyFaithful = @CategoryTheory.GrothendieckTopology.yonedaFullyFaithful