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 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) :

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).

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
    Instances For

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

      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.

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

      Equations
      Instances For

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

        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.

        Instances

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

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

          @[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), (CategoryTheory.GrothendieckTopology.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) :
          (CategoryTheory.GrothendieckTopology.yoneda.obj X).val = CategoryTheory.yoneda.obj X

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] :
            CategoryTheory.GrothendieckTopology.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
            Instances For
              def CategoryTheory.GrothendieckTopology.yonedaFullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] :
              CategoryTheory.GrothendieckTopology.yoneda.FullyFaithful

              The yoneda functor into the sheaf category is fully faithful

              Equations
              • CategoryTheory.GrothendieckTopology.yonedaFullyFaithful = CategoryTheory.Yoneda.fullyFaithful.ofCompFaithful
              Instances For
                instance CategoryTheory.GrothendieckTopology.instFullSheafTypeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] :
                CategoryTheory.GrothendieckTopology.yoneda.Full
                Equations
                • =
                instance CategoryTheory.GrothendieckTopology.instFaithfulSheafTypeYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] :
                CategoryTheory.GrothendieckTopology.yoneda.Faithful
                Equations
                • =
                @[deprecated CategoryTheory.GrothendieckTopology.Subcanonical]

                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
                Instances For
                  @[deprecated CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj]

                  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]

                  Alias of CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable.


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

                  @[deprecated CategoryTheory.GrothendieckTopology.yoneda]

                  Alias of CategoryTheory.GrothendieckTopology.yoneda.


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

                  Equations
                  Instances For
                    @[deprecated CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf]
                    def CategoryTheory.Sheaf.Subcanonical.yonedaCompSheafToPresheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] :
                    CategoryTheory.GrothendieckTopology.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
                    Instances For
                      @[deprecated CategoryTheory.GrothendieckTopology.yonedaFullyFaithful]
                      def CategoryTheory.Sheaf.Subcanonical.yonedaFullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.Subcanonical] :
                      CategoryTheory.GrothendieckTopology.yoneda.FullyFaithful

                      Alias of CategoryTheory.GrothendieckTopology.yonedaFullyFaithful.


                      The yoneda functor into the sheaf category is fully faithful

                      Equations
                      Instances For