open import 1Lab.Reflection.Copattern

open import Cat.Functor.FullSubcategory
open import Cat.Instances.Functor
open import Cat.Diagram.Sieve
open import Cat.Prelude hiding (glue)

import Cat.Functor.Reasoning.Presheaf as Psh
import Cat.Reasoning as Cat

module Cat.Site.Base where

private variable
o β βc βs : Level
C : Precategory o β


# Sites and sheavesπ

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

Source

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 of objects we want to study, and we will denote its objects by letters like and The structures we will be interested in will all take the form of presheaves on β functors into the category If we have any family of maps and an element then functorial action ensures that we can restrict along the to obtain elements

A representative example is when is the frame underlying some locale and the elements are such that This setup has the particular geometric interpretation of expressing as a union of smaller parts. Extending this intuition, we would consider our original to be the global information, and the restrictions to be information local to a given sub-part of the whole

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 can we glue them together to get the global information We canβt always: this might be a failure of the functor1, or of the 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 are all restrictions of some we should investigate the properties it must have: these will tell us what properties we should impose on local data to ensure it has a chance of gluing to a The key property is, once again, functoriality β but it also has a geometric interpretation. Suppose we have two objects and drawn from our family, and some arbitrary third object and they fit into a commutative diagram like

If we are still thinking about then could simply be the intersection and the diagram commutes automatically. In any case, we have two ways of restricting to the intersection namely and By functoriality, we have

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 This lets us simplify the notion of compatibility: we now have values of at arbitrary composites of the so that it suffices to demand

## 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 we will refer to a family of elements as a family of parts. If these parts satisfy the compatibility condition defined above, relative to the sieve we will say they are a patch. The geometric intuition is key here: the are to be the literal parts of some hypothetical and theyβre a patch if they agree on the βintersectionsβ

  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 of parts, then we say that an element is a section of these parts if its restriction along each agrees with the part

  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 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 to be a sheaf, at least with respect to a sieve on any patch of has a unique section. Thinking intuitively, satisfying the sheaf condition for a sieve means that each arises uniquely as the gluing of some patch 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 is a 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 β equalityβ is exactly what we need to assure that is also a section of the patch generated by restricting  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 when defining parts, patches, sections and sheaves. But a given category, even the opens of a locale, will generally have many distinct sieves on which could equally well be taken to be decompositions of . We would like a sheaf βon β 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 on to consist of, for each a family of covering sieves on Translating this into type theory, for each we have a type of β of β, and, for each we have an associated sieve on 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 must satisfy the following stability property: if is some covering sieve, and is an arbitrary morphism, then there merely exists a covering sieve which is contained in the pullback sieve 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 we can equip any frame with a coverage. The stability condition, in that case, reduces to showing that, if a family has all of as its union, then the family has 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 For separated presheaves, we can simply reuse the definition given above, demanding it for every 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 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 with a coverage as the site The first notion we define relative to sites is the category of sheaves on a site, the full subcategory of the presheaves on which are The nature of the sheaf condition ensures that inherits most of 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


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

and define a functor by sending to the unit set, both singleton sets to and the two-element set to the restriction mappings are the projections onto the first two factors.

We will later see that, were a sheaf, the elements of would have their equality determined by their restrictions to and β but by this measure, and 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.