module Cat.Site.Base where

# Sites and sheavesπ

**Sheaf theory** is a particular formalisation of the
idea that *global* structure
$A(U)$
on a complicated object
$U$
is often best studied at its *restrictions* to simpler parts
$V_{i}$
which *glue* to recover
$U.$
Itβs particularly general, in the sense that the objects
$U$
can belong to an arbitrary category
$C,$
as long as we equip
$C$
with structure (called a **coverage**) determining what we
mean by *glue together* β and as long as our global structure
$A(U)$
is fine living at the level of sets.

Most of our material on sheaf theory is adapted from the Elephant (2002), specifically chapter C2.

To make these ideas concrete, we will fix a category
$C$
of objects we want to study, and we will denote its objects by letters
like
$U,$
$V,$
and
$W.$
The structures we will be interested in will all take the form of
*presheaves* on
$C$
β functors into the category
$Sets.$
If we have any family of maps
$(h_{i}:U_{i}βU)_{i},$
and an element
$s:A(U),$
then
$A_{β²}s$
functorial action ensures that we can restrict
$s$
along the
$h_{i}$
to obtain elements
$s_{i}:A(U_{i}).$

A representative example is when
$C$
is the frame
$Ξ©(L)$
underlying some locale
$L,$
and the elements
$U_{i}$
are such that
$U=β_{i}U_{i}.$
This setup has the particular *geometric* interpretation of
expressing
$U$
as a union of smaller parts. Extending this intuition, we would consider
our original
$s:A(U)$
to be the *global* information, and the restrictions
$s_{i}:A(U_{i})$
to be information *local* to a given sub-part of the whole
$U.$

So far, we have said nothing new: this is simply functoriality. The
interesting question is going *the other way*: if we have the
local information
$s_{i}:A(U_{i}),$
can we glue them together to get the global information
$s:A(U)?$
We canβt *always*: this might be a failure of the functor^{1}, or of the
$s_{i}.$
While it might be a bit disheartening that there are notions of
βinformationβ which can not be put together locally, these failures tell
us that we have a fruitful concept at hand.

First, assuming that our
$s_{i}:A(U_{i})$
are all restrictions of some
$s:A(U),$
we should investigate the properties it *must* have: these will
tell us what properties we should impose on local data
$t_{i}:A(V_{i})$
to ensure it has a *chance* of gluing to a
$t:A(V).$
The key property is, once again, functoriality β but it also has a
*geometric* interpretation. Suppose we have two objects
$U_{i}$
and
$U_{j}$
drawn from our family, and some arbitrary third object
$V,$
and they fit into a commutative diagram like

If we are still thinking about $C=Ξ©(L),$ then $V$ could simply be the intersection $U_{i}β©U_{j},$ and the diagram commutes automatically. In any case, we have two ways of restricting $s:A(U)$ to the intersection $V,$ namely $A(f)(s_{i})$ and $A(g)(s_{j}).$ By functoriality, we have

$A(f)(s_{i})=A(fh_{i})(s)=A(gh_{j})(s)=A(g)(s_{j}),$so that, if our βlocalβ data comes from restricting βglobalβ data,
the local restrictions automatically *agree on intersections*. We
thus have defined what it means to have *local data* with respect
to a family of morphisms (which we think of as expressing their common
codomain as being βglued togetherβ), and what it means for that data to
*glue* to give local data.

We could carry on and define sheaves from here, but we will make one
final simplifying assumption: Instead of considering *families*
of morphisms with common codomain, we will consider sieves in
$C.$
This lets us simplify the notion of compatibility: we now have values
$s(fh_{i})$
of
$s$
at arbitrary composites of the
$h_{i},$
so that it suffices to demand
$A(f)(s(h_{i}))=s(fh_{i}).$

## Terminology for local dataπ

-- Defining these notions for "non-functors" first will let us avoid -- angering the positivity checker when defining sheafifications, see -- that module for more details. module pre {o β βs} (C : Precategory o β) {Aβ : β C β β Type βs} (Aβ : β {U V} β C .Precategory.Hom U V β Aβ V β Aβ U) where open Precategory C

To formalise the notion of sheaf, we will need to introduce names for
the ideas weβve sketched out so far. First, if we are given a sieve
$f_{i}:U_{i}βU,$
we will refer to a family of elements
$s(f_{i}):A(U_{i})$
as a family of **parts**. If these parts satisfy the
compatibility condition defined above, relative to the sieve
$f_{i},$
we will say they are a **patch**. The geometric intuition
is key here: the
$s(f_{i})$
are to be the literal *parts* of some hypothetical
$s:A(U),$
and theyβre a patch if they agree on the βintersectionsβ
$U_{i}βVβU_{j}.$

Parts : β {U} (T : Sieve C U) β Type _ Parts {U} T = β {V} (f : Hom V U) (hf : f β T) β Aβ V is-patch : β {U} (T : Sieve C U) (p : Parts T) β Type _ is-patch {U} T part = β {V W} (f : Hom V U) (hf : f β T) (g : Hom W V) (hgf : f β g β T) β Aβ g (part f hf) β‘ part (f β g) hgf

Finally, if we have a family
$s(f_{i}):A(U_{i})$
of parts, then we say that an element
$s:A(U)$
is a **section** of these parts if its restriction along
each
$f_{i}$
agrees with the part
$s(f_{i}):$

is-section : β {U} (T : Sieve C U) β Aβ U β Parts T β Type _ is-section {U = U} T s p = β {V} (f : Hom V U) (hf : f β T) β Aβ f s β‘ p f hf

module _ {o β βs} {C : Precategory o β} (A : Functor (C ^op) (Sets βs)) where open Precategory C private module A = Psh A open pre C A.β hiding (is-section)

We will most often consider parts-which-are-patches, so we introduce a record type to bundle them; similarly, we will consider elements-which-are-sections, so they also get a record type.

record Patch {U} (T : Sieve C U) : Type (o β β β βs) where no-eta-equality field part : Parts T patch : is-patch T part

abstract app : β {V} {f g : Hom V U} {hf hg} β f β‘ g β part f hf β‘ part g hg app p = apβ part p prop! compatible : β {V W X} {i : Hom W U} {j : Hom X U} (g : Hom V W) (h : Hom V X) β {is : i β T} {js : j β T} β i β g β‘ j β h β A βͺ g β« part i is β‘ A βͺ h β« part j js compatible {i = i} {j} g h {is} {js} p = A βͺ g β« part i is β‘β¨ patch i _ g (T .closed is g) β©β‘ part (i β g) _ β‘β¨ app p β©β‘ part (j β h) _ β‘β¨ sym (patch j _ h (T .closed js h)) β©β‘ A βͺ h β« part j js β open Patch is-section : β {U} {T : Sieve C U} β A Κ» U β Patch T β Type _ is-section {T = T} p x = pre.is-section C A.β T p (x .part)

record Section {U} {T : Sieve C U} (p : Patch T) : Type (o β β β βs) where no-eta-equality field {whole} : A Κ» U glues : is-section whole p

module _ {o β βs} {C : Precategory o β} {A : Functor (C ^op) (Sets βs)} where open Cat C open Section open Patch private module A = Psh A open pre C A.β hiding (is-section) public instance Extensional-Patch : β {U βr} {S : Sieve C U} β¦ _ : Extensional (Parts S) βr β¦ β Extensional (Patch A S) βr Extensional-Patch β¦ e β¦ .Pathα΅ x y = e .Pathα΅ (x .part) (y .part) Extensional-Patch β¦ e β¦ .reflα΅ x = e .reflα΅ (x .part) Extensional-Patch β¦ e β¦ .idsα΅ .to-path p i .part = e .idsα΅ .to-path p i Extensional-Patch β¦ e β¦ .idsα΅ .to-path {x} {y} p i .patch {W = W} f hf g hgf = is-propβpathp (Ξ» i β A.β W .is-tr (A.β g (e .idsα΅ .to-path p i _ hf)) (e .idsα΅ .to-path p i _ hgf)) (x .patch f hf g hgf) (y .patch f hf g hgf) i Extensional-Patch β¦ e β¦ .idsα΅ .to-path-over p = is-propβpathp (Ξ» i β Pathα΅-is-hlevel 1 e (hlevel 2)) _ _ Extensional-Section : β {U βr} {S : Sieve C U} {p : Patch A S} β¦ _ : Extensional (A Κ» U) βr β¦ β Extensional (Section A p) βr Extensional-Section β¦ e β¦ .Pathα΅ x y = e .Pathα΅ (x .whole) (y .whole) Extensional-Section β¦ e β¦ .reflα΅ x = e .reflα΅ (x .whole) Extensional-Section β¦ e β¦ .idsα΅ .to-path p i .whole = e .idsα΅ .to-path p i Extensional-Section {p = p} β¦ e β¦ .idsα΅ .to-path {a} {b} q i .glues {V} f hf = is-propβpathp (Ξ» i β A.β V .is-tr (A.β f (e .idsα΅ .to-path q i)) (p .part f hf)) (a .glues f hf) (b .glues f hf) i Extensional-Section β¦ e β¦ .idsα΅ .to-path-over p = is-propβpathp (Ξ» i β Pathα΅-is-hlevel 1 e (hlevel 2)) _ _ subsetβpatch : β {U} {S S' : Sieve C U} β S' β S β Patch A S β Patch A S' subsetβpatch incl p .part f hf = p .part f (incl f hf) subsetβpatch incl p .patch f hf g hgf = p .patch f _ g _ pullback-patch : β {U V} {S : Sieve C U} (f : Hom V U) β Patch A S β Patch A (pullback f S) pullback-patch {S = S} f s .part g p = s .part (f β g) p pullback-patch {S = S} f s .patch g h hfg hfgh = s .patch (f β g) h hfg (S .closed h hfg) β app s (pullr refl) open _=>_ map-patch : β {B : Functor (C ^op) (Sets βs)} {U} {S : Sieve C U} (eta : A => B) β Patch A S β Patch B S map-patch eta x .part f hf = eta .Ξ· _ (x .part f hf) map-patch eta x .patch f hf g hgf = sym (eta .is-natural _ _ _ $β _) β ap (eta .Ξ· _) (x .patch f hf g hgf)

Finally, we will formalise the idea that any *global*
information
$s:A(U)$
can be made into a bunch of *local* pieces by restricting
functorially.

sectionβpatch : β {U} {T : Sieve C U} β A Κ» U β Patch A T sectionβpatch x .part f _ = A βͺ f β« x sectionβpatch x .patch f hf g hgf = A.collapse refl sectionβsection : β {U} {T : Sieve C U} (u : A Κ» U) β Section A {T = T} (sectionβpatch u) sectionβsection u .whole = u sectionβsection u .glues f hf = refl

## The notion of sheafπ

Using our terminology above, we can very concisely define what it means for a functor $A:PSh(C)$ to be a sheaf, at least with respect to a sieve $T$ on $U:$ any patch $p$ of $T$ has a unique section. Thinking intuitively, satisfying the sheaf condition for a sieve $T$ means that each $s:A(U)$ arises uniquely as the gluing of some patch $s(f_{i}):A(U_{i}).$

module _ {o β βs} {C : Precategory o β} (A : Functor (C ^op) (Sets βs)) where open Precategory C open Section open Patch

is-sheafβ : β {U} (T : Sieve C U) β Type _ is-sheafβ T = (p : Patch A T) β is-contr (Section A p)

We will also need the notion of **separated presheaf**.
These are typically defined to be the presheaves which have *at most
one* section for each patch: the type of sections for each patch is
a proposition, instead of
being contractible.

But from a type-theoretic perspective, it makes more sense to define separated presheaves in the following βunfoldedβ form, which says that that equality on $A(U)$ is a $T-local$ property.

is-separatedβ : β {U} (T : Sieve C U) β Type _ is-separatedβ {U} T = β {x y : A Κ» U} β (β {V} (f : Hom V U) (hf : f β T) β A βͺ f β« x β‘ A βͺ f β« y) β x β‘ y

Note that every sheaf is indeed separated, even after this unfolding,
using the above mapping from elements to sections. The assumption of
β$T-local$
equalityβ is exactly what we need to assure that
$y$
is *also* a section of the patch generated by restricting
$x.$

is-sheafββis-separatedβ : β {U} (T : Sieve C U) β is-sheafβ T β is-separatedβ T is-sheafββis-separatedβ T sheaf {x} {y} lp = ap whole $ let secβ : Section A (sectionβpatch x) secβ = sectionβsection x secβ : Section A (sectionβpatch x) secβ = record { whole = y ; glues = Ξ» f hf β A βͺ f β« y β‘Λβ¨ lp f hf β©β‘Λ A βͺ f β« x β } in is-contrβis-prop (sheaf (sectionβpatch x)) secβ secβ

from-is-separatedβ : β {U} {T : Sieve C U} β is-separatedβ T β β {p : Patch A T} (s : Section A p) β is-contr (Section A p) from-is-separatedβ sep sec .centre = sec from-is-separatedβ sep sec .paths x = ext $ sep Ξ» f hf β sec .glues f hf β sym (x .glues f hf) -- This is equal to `subst (is-sheafβ A)` but has better definitional -- behaviour for the relevant part. subst-is-sheafβ : β {U} {T S : Sieve C U} (p : T β‘ S) β is-sheafβ T β is-sheafβ S subst-is-sheafβ {T = T} {S = S} p shf pa = done where pa' : Patch A T pa' .part f hf = pa .part f (subst (f β_) p hf) pa' .patch f hf g hgf = pa .patch f _ g _ sec = shf pa' done : is-contr (Section A pa) done .centre .whole = sec .centre .whole done .centre .glues f hf = sec .centre .glues f (subst (f β_) (sym p) hf) β app pa refl done .paths x = ext (ap whole (sec .paths record { glues = Ξ» f hf β x .glues f (subst (f β_) p hf) β app pa refl }))

# Sites, formallyπ

Up until now, we have only been considering *single* sieves
$f_{i}:U_{i}βU$
when defining parts, patches, sections and sheaves. But a given
category, even the opens of a locale, will generally have many
*distinct* sieves on
$U$
which could equally well be taken to be *decompositions of
$U$*.
We would like a sheaf βon
$C$β
to have the local-to-global property for all of these decompositions,
but we need to impose *some* order to make sure that we end up
with a well-behaved *category of sheaves.*

We define a **coverage**
$J$
on
$C$
to consist of, for each
$U:C,$
a family
$J(U)$
of **covering sieves** on
$U.$
Translating this into type theory, for each
$U,$
we have a type
$J(U)$
of
β$J-covers$
of
$U$β,
and, for each
$x:J(U),$
we have an associated sieve
$J(x)$
on
$U.$

record Coverage {o β} (C : Precategory o β) βc : Type (o β β β lsuc βc) where no-eta-equality open Precategory C field covers : β C β β Type βc cover : β {U} β covers U β Sieve C U

The
$J(U)$
must satisfy the following *stability* property: if
$R:J(U)$
is some covering sieve, and
$f:VβU$
is an arbitrary morphism, then there merely exists a
covering sieve
$S:J(V)$
which *is contained in* the pullback sieve
$f_{β}(R).$
The quantifier complexity for this statement is famously befuddling, but
stating it in terms of sieves does simplify the formalisation:

stable : β {U V : β C β} (R : covers U) (f : Hom V U) β β[ S β covers V ] (cover S β pullback f (cover R))

Thinking back to the case of
$C=Ξ©(L),$
we can equip any frame with a coverage. The
stability condition, in that case, reduces to showing that, if a family
$U_{i}βͺU$
has all of
$U$
as its union, then the family
$(U_{i}β©V)βͺ(Uβ©V)$
has
$Uβ©V$
as *its* union.

open Coverage public instance Funlike-Coverage : Funlike (Coverage C βc) β C β (Ξ» _ β Type βc) Funlike-Coverage = record { _#_ = Ξ» C U β C .covers U } Membership-Coverage : β {U} β Membership (Coverage C βc) (Sieve C U) _ Membership-Coverage = record { _β_ = Ξ» C S β fibre (C .cover) S }

module _ {o β βc βs} {C : Precategory o β} (J : Coverage C βc) (A : Functor (C ^op) (Sets βs)) where

Finally, we (re-)define separated presheaves and sheaves with respect to a coverage $J.$ For separated presheaves, we can simply reuse the definition given above, demanding it for every $J-covering$ sieve. But for sheaves, formalisation concerns lead us to instead define an βunpackedβ record type:

is-separated : Type _ is-separated = β {U : β C β} (c : J # U) β is-separatedβ A (J .cover c) record is-sheaf : Type (o β β β βs β βc) where no-eta-equality field whole : β {U} (S : J .covers U) (p : Patch A (J .cover S)) β A Κ» U glues : β {U} (S : J .covers U) (p : Patch A (J .cover S)) β is-section A (whole S p) p separate : is-separated

This splitting of the sheaf condition into an *operation* and
*laws* will help us in defining sheafifications
later on. We can package the first two fields as saying that each patch
has a section:

split : β {U} {S : J .covers U} (p : Patch A (J .cover S)) β Section A p split p .Section.whole = whole _ p split p .Section.glues = glues _ p open is-sheaf using (whole ; glues ; separate) public

Note that, if a functor satisfies the sheaf condition for all $J-covering$ sieves, itβs also a sheaf relative to quite a few other sieves: these are the closure properties of sites.

module _ {o β βc βs} {C : Precategory o β} {J : Coverage C βc} {A : Functor (C ^op) (Sets βs)} where from-is-separated : is-separated J A β (β {U} (c : J .covers U) (s : Patch A (J .cover c)) β Section A s) β is-sheaf J A from-is-separated sep split .whole S p = split S p .Section.whole from-is-separated sep split .glues S p = split S p .Section.glues from-is-separated sep split .separate S = sep S from-is-sheafβ : (β {U} (c : J .covers U) β is-sheafβ A (J .cover c)) β is-sheaf J A from-is-sheafβ shf .whole S p = shf _ p .centre .Section.whole from-is-sheafβ shf .glues S p = shf _ p .centre .Section.glues from-is-sheafβ shf .separate S = is-sheafββis-separatedβ _ _ (shf _) to-is-sheafβ : is-sheaf J A β β {U} (c : J .covers U) β is-sheafβ A (J .cover c) to-is-sheafβ shf c p = from-is-separatedβ _ (shf .separate c) (is-sheaf.split shf p)

open Section public open Patch public module _ {o β βc βp} {C : Precategory o β} {J : Coverage C βc} {A : Functor (C ^op) (Sets βp)} where private unquoteDecl eqv = declare-record-iso eqv (quote is-sheaf) abstract instance H-Level-is-sheaf : β {n} β H-Level (is-sheaf J A) (suc n) H-Level-is-sheaf = prop-instance $ retractβis-hlevel 1 from to ft (hlevel 1) where T : Type (o β β β βc β βp) T = β {U} (S : J .covers U) (p : Patch A (J .cover S)) β is-contr (Section A p) from : T β is-sheaf J A from x .whole S p = x S p .centre .whole from x .glues S p = x S p .centre .glues from x .separate S = is-sheafββis-separatedβ A _ (x S) to : is-sheaf J A β T to shf S p = from-is-separatedβ _ (shf .separate S) (is-sheaf.split shf p) ft : β x β from (to x) β‘ x ft x = Iso.injective eqv (Ξ£-prop-path! refl)

module _ {o β βc} {C : Precategory o β} (J : Coverage C βc) βs where open Precategory open Functor

We will often refer to a category
$C$
with a coverage
$J$
as the **site**
$(C,J).$
The first notion we define relative to sites is the category of
*sheaves on a site*,
$Sh(C,J):$
the full
subcategory of the presheaves on
$C$
which are
$J-sheaves.$
The nature of the sheaf condition ensures that
$Sh(C,J)$
inherits most of
$PSh(C)βs$
good categorical properties β we refer to it as the topos of
sheaves.

Sheaf : Type _ Sheaf = Ξ£[ p β Functor (C ^op) (Sets βs) ] is-sheaf J p Sheaves : Precategory (o β β β βc β lsuc βs) (o β β β βs) unquoteDef Sheaves = define-copattern Sheaves $ Restrict {C = PSh βs C} (is-sheaf J) forget-sheaf : Functor Sheaves (PSh βs C) forget-sheaf .Fβ (S , _) = S forget-sheaf .Fβ f = f forget-sheaf .F-id = refl forget-sheaf .F-β f g = refl

For a functor that is not a sheaf, consider the category

and define a functor $A(β)$ by sending ${}$ to the unit set, both singleton sets to $Z,$ and the two-element set to $ZΓZΓZ;$ the restriction mappings are the projections onto the first two factors.

We will later see that, were $A$ a sheaf, the elements of $A({0,1})$ would have their equality determined by their restrictions to $A({0})$ and $A({1})$ β but by this measure, $(0,0,0)$ and $(0,0,1)$ would have to be equal.β©οΈ

## References

- Johnstone, Peter T. 2002.
*Sketches of an Elephant: a Topos Theory Compendium*. Oxford Logic Guides. New York, NY: Oxford Univ. Press. https://cds.cern.ch/record/592033.