module Cat.Site.Base where

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.


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🔗

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

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
      part  : Parts T
      patch : is-patch T part
  record Section {U} {T : Sieve C U} (p : Patch T) : Type (o ⊔ ℓ ⊔ ℓs) where
      {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

      : ∀ {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)) _ _

      : ∀ {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)) _ _

    : ∀ {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 _=>_

    : ∀ {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

    : ∀ {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

  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 $
      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₂

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

  open Precategory C

    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:

      : ∀ {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.

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

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.↩


  • Johnstone, Peter T. 2002. Sketches of an Elephant: a Topos Theory Compendium. Oxford Logic Guides. New York, NY: Oxford Univ. Press.