4.1. Coherent topology
Any precoherent category can be equipped with the coherent coverage, where covering families are given by finite effective epimorphic families. The coherent topology is the topology generated by the coherent coverage.
- No associated Lean code or declarations.
One would hope that the topology on \et{X} given by jointly surjective
families is the precoherent topology. Since effective epimorphisms are simply
surjective maps in \et{X}, this would mean that every cover in \et{X} can
be refined by a finite cover. This is not true though, because \et{X} also
contains non-quasi-compact schemes.
The situation is slightly better if we instead consider the affine étale site
\affet{X} of X, the category of affine schemes étale over X.
Unfortunately, it is not clear to the authors if effective epimorphisms in
\affet{X} are still surjective.
Let from now on \mathcal{C} be precoherent equipped with the coherent
topology.
- No associated Lean code or declarations.
Let F \colon \pro{\mathcal{C}}^{\mathrm{op}} \to \mathrm{Set} be a sheaf.
Then F|_{\mathcal{C}^{\mathrm{op}}} is a sheaf.
By Proposition 4.1.2, the inclusion functor
\mathcal{C} \to \pro{\mathcal{C}} induces a morphism on sites
\nu\colon \pro{\mathcal{C}} \to \mathcal{C}. The direct image functor
\nu_{*}\colon \shv{\pro{\mathcal{C}}} \to \shv{\mathcal{C}} agrees with the
restriction F \mapsto F|_{\mathcal{C}^{\mathrm{op}}}.
- No associated Lean code or declarations.
Let F \colon \pro{\mathcal{C}}^{\mathrm{op}} \to \mathrm{Set} be a
presheaf. Suppose F|_{\mathcal{C}^{\mathrm{op}}} is a sheaf and F
preserves filtered colimits. Then F is a sheaf.
Combining Proposition 4.1 and Proposition 4.1.3 yields:
- No associated Lean code or declarations.
Let F be a sheaf on \mathcal{C}. Then the unit
F \to \nu_{*} \nu^{-1} F is an isomorphism.
Denote by \mathrm{res} the restriction functor
\mathrm{PShv}(\pro{\mathcal{C}}) \to \mathrm{PShv}(\mathcal{C}) and by
\mathrm{ext} the left-adjoint of Proposition 4.1. By
Proposition 4.1.3, \mathrm{ext} restricts to a functor
\mathrm{Shv}(\mathcal{C}) \to \mathrm{Shv}(\pro{\mathcal{C}}) that is the
left-adjoint of \nu_*. In particular it agrees with \nu^{-1} and the
result follows.