# 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 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

## 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

## Equations

- CategoryTheory.Sheaf.canonicalTopology C = CategoryTheory.Sheaf.finestTopology (Set.range CategoryTheory.yoneda.toPrefunctor.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.

## Equations

## Instances For

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.