Documentation

Mathlib.CategoryTheory.Sites.Canonical

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} [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 fCategoryTheory.Sieve Y) (hU : CategoryTheory.Presieve.IsSheafFor P U.arrows) (hB : ∀ ⦃Y : C⦄ ⦃f : Y X⦄ (hf : U.arrows f), CategoryTheory.Presieve.IsSheafFor P (B Y f 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 Y f h)).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 [Elephant], 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 : CategoryTheory.Sieve X) (S : CategoryTheory.Sieve X) (hR : CategoryTheory.Presieve.IsSheafFor P R.arrows) (hR' : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, S.arrows fCategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f R).arrows) (hS : ∀ ⦃Y : C⦄ ⦃f : Y X⦄, R.arrows fCategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f 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 [Elephant], 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).

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.

    Instances For

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

      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

      Instances For

        yoneda.obj X 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.

        Instances For

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