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/
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/
Given two sieves R
and S
, to show that P
is a sheaf for S
, we can show:
P
is a sheaf forR
P
is a sheaf for the pullback ofS
along any arrow inR
P
is separated for the pullback ofR
along any arrow inS
.
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
- CategoryTheory.Sheaf.finestTopology Ps = sInf (CategoryTheory.Sheaf.finestTopologySingle '' Ps)
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
- CategoryTheory.Sheaf.canonicalTopology C = CategoryTheory.Sheaf.finestTopology (Set.range CategoryTheory.yoneda.obj)
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.
- le_canonical : J ≤ CategoryTheory.Sheaf.canonicalTopology C
Instances
Equations
- ⋯ = ⋯
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.
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
The yoneda embedding into the presheaf category factors through the one to the sheaf category.
Equations
- CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf = CategoryTheory.Iso.refl (CategoryTheory.GrothendieckTopology.yoneda.comp (CategoryTheory.sheafToPresheaf J (Type ?u.54)))
Instances For
The yoneda functor into the sheaf category is fully faithful
Equations
- CategoryTheory.GrothendieckTopology.yonedaFullyFaithful = CategoryTheory.Yoneda.fullyFaithful.ofCompFaithful
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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.
Instances For
Alias of CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
.
If every functor yoneda.obj X
is a J
-sheaf, then J
is subcanonical.
Alias of CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable
.
If J
is subcanonical, then any representable is a J
-sheaf.
Alias of CategoryTheory.GrothendieckTopology.yoneda
.
If J
is subcanonical, we obtain a "Yoneda" functor from the defining site
into the sheaf category.
Instances For
Alias of CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf
.
The yoneda embedding into the presheaf category factors through the one to the sheaf category.
Equations
Instances For
Alias of CategoryTheory.GrothendieckTopology.yonedaFullyFaithful
.
The yoneda functor into the sheaf category is fully faithful