module Cat.Site.Closure where

Closure properties of sites🔗

If is a sheaf on a site then there are quite a few sieves for which is a sheaf but which are not required to be present in Put another way, the collection of sieves for which a given functor is a sheaf enjoys closure properties beyond the basic pullback-stability which we have assumed in the definition of coverage. Closing under these extra constructions does not change the theory of “sheaves on ”, and sometimes they’re quite convenient!

In reality, the first few of these properties don’t even need a site: they work for a completely arbitrary functor We will fix a completely arbitrary functor for the remainder of this section. The first thing we note is that, if a sieve contains the identity, then is a sheaf for

  is-sheaf-maximal : ∀ {U} {S : Sieve C U} → id ∈ S → is-sheaf₁ A S
  is-sheaf-maximal {S = S} id∈S p .centre .whole = p .part id id∈S
  is-sheaf-maximal {S = S} id∈S p .centre .glues f hf =
    A ⟪ f ⟫ p .part id id∈S ≡⟨ p .patch id id∈S f (subst (_∈ S) (sym (idl f)) hf) ⟩≡
    p .part (id ∘ f) _      ≡⟨ app p (idl f) ⟩≡
    p .part f hf            ∎
  is-sheaf-maximal {S = S} id∈S p .paths x = ext $
    p .part id id∈S   ≡˘⟨ x .glues id id∈S ⟩≡˘
    A ⟪ id ⟫ x .whole ≡⟨ A.F-id ⟩≡
    x .whole          ∎

Since sieves are closed under composition, this can be extended to any which contains an isomorphism. Intuitively, this is because any sieve on which contains the identity (or an isomorphism) says that global data on can be constructed locally… on all of We can thus just extract this not-actually-local data from a given patch.

  is-sheaf-iso : ∀ {V U} {S : Sieve C U} (f : V ≅ U) → f .to ∈ S → is-sheaf₁ A S
  is-sheaf-iso {S = S} f hf = is-sheaf-maximal $
    subst (_∈ S) (f .invl) (S .closed hf (f .from))

The second notion we investigate says that the notion of sheaf is, itself, local: If is a sheaf for a sieve and we have some other sieve which we want to show is a sheaf for, it (almost) suffices to show that A is an for every If and are not part of a site, then this condition does not suffice: we also require that be for every

\ Warning

In the Elephant, this lemma appears as C2.1.7. However, Johnstone’s version is incorrect as stated. It can be remedied by assuming that belongs to a site for which is a sheaf, since a sheaf on a site is automatically separated for any pullback of a covering sieve.

  is-sheaf-transitive
    : ∀ {U} {R S : Sieve C U}
    → (∀ {V} (f : Hom V U) (hf : f ∈ S) → is-separated₁ A (pullback f R))
    → (∀ {V} (f : Hom V U) (hf : f ∈ R) → is-sheaf₁ A (pullback f S))
    → is-sheaf₁ A R
    → is-sheaf₁ A S
  is-sheaf-transitive {U} {R} {S} R*sep S*sheaf Rsheaf p = q where

The proof is slightly complicated. Note that a patch on can be pulled back to give a patch on for any Since is an at each in there is a unique and a short calculation shows that these give a patch on

    p' : ∀ {V} (f : Hom V U) → Patch A (pullback f S)
    p' f = pullback-patch f p

    p'' : Patch A R
    p'' .part f hf = S*sheaf f hf (p' f) .centre .whole
    p'' .patch f hf g hgf = ext $ is-sheaf₁→is-separated₁ A _ (S*sheaf (f ∘ g) hgf) λ h hh →
      A ⟪ h ⟫ (A ⟪ g ⟫ (p'' .part f hf))  ≡⟨ A.collapse refl ⟩≡
      A ⟪ g ∘ h ⟫ (p'' .part f hf)        ≡⟨ S*sheaf f hf (p' f) .centre .glues (g ∘ h) (subst (_∈ S) (sym (assoc f g h)) hh) ⟩≡
      p .part (f ∘ g ∘ h) _               ≡⟨ app p (assoc _ _ _) ⟩≡
      p .part ((f ∘ g) ∘ h) _             ≡˘⟨ S*sheaf (f ∘ g) hgf (p' (f ∘ g)) .centre .glues h hh ⟩≡˘
      A.₁ h (p'' .part (f ∘ g) hgf)       ∎

    s : Section A p''
    s = Rsheaf p'' .centre

By assumption, is an so our patch on glues to give an element — a section of even. We must now show that for Since only agrees with this might be a problem: that’s where the assumption that is comes in (for we can reduce this to showing with We would almost be in trouble again, since is only characterised but we can appeal to separatedness again, this time at This finally allows the calculation to go through:

    q : is-contr (Section A p)
    q .centre .whole = s .whole
    q .centre .glues f hf = R*sep f hf λ g hg → is-sheaf₁→is-separated₁ A _ (S*sheaf (f ∘ g) hg) λ h hh →
      A ⟪ h ⟫ (A ⟪ g ⟫ (A ⟪ f ⟫ s .whole)) ≡⟨ A.ap (A.collapse refl ∙ Rsheaf p'' .centre .glues (f ∘ g) hg) ⟩≡
      A ⟪ h ⟫ p'' .part (f ∘ g) hg        ≡⟨ S*sheaf (f ∘ g) hg (p' (f ∘ g)) .centre .glues h hh ⟩≡
      p .part ((f ∘ g) ∘ h) hh            ≡˘⟨ app p (assoc f g h) ⟩≡˘
      p .part (f ∘ g ∘ h) _               ≡˘⟨ p .patch f hf (g ∘ h) (subst (_∈ S) (sym (assoc f g h)) hh) ⟩≡˘
      A ⟪ g ∘ h ⟫ (p .part f hf)          ≡⟨ A.expand refl ⟩≡
      A ⟪ h ⟫ (A ⟪ g ⟫ p .part f hf)      ∎
    q .paths x = ext $ ap whole $ Rsheaf p'' .paths
      record { glues = λ f hf → sym $ ap whole (S*sheaf f hf (p' f) .paths
        record { glues = λ g hg → A.collapse refl ∙ x .glues (f ∘ g) hg }) }

On a site🔗

Now specialising to a site and a functor which is a we can show a few more pedestrian closure properties. First, is a sheaf for any sieve that contains a sieve (call it

  is-sheaf-factor
    : ∀ {U} (s : Sieve C U) (c : J # U)
    → (∀ {V} (f : Hom V U) → f ∈ J .cover c → f ∈ s)
    → is-sheaf₁ A s
  is-sheaf-factor s c c⊆s ps = done where
    sec' = shf.split (subset→patch c⊆s ps)

If is a patch on and contains we can restrict to a patch on Gluing we obtain a section for Showing this requires using the pullback-stability of though: We must show that for but is only characterised for

    sec : Section A ps
    sec .whole = sec' .whole

However, by passing to the pullback sieve we’re allowed to show this assuming that we have some with The calculation goes through without problems:

    sec .glues f hf = ∥-∥-out! do
      (c' , sub) ← J .stable c f
      pure $ shf.separate c' λ g hg →
        A ⟪ g ⟫ (A ⟪ f ⟫ sec' .whole) ≡⟨ A.collapse refl ⟩≡
        A ⟪ f ∘ g ⟫ sec' .whole       ≡⟨ sec' .glues (f ∘ g) (sub _ hg) ⟩≡
        ps .part (f ∘ g) _           ≡˘⟨ ps .patch f hf g (c⊆s (f ∘ g) (sub g hg)) ⟩≡˘
        A ⟪ g ⟫ ps .part f hf        ∎

    done : is-contr (Section A ps)
    done .centre = sec
    done .paths x = ext $ shf.separate c λ f hf →
      A ⟪ f ⟫ sec' .whole ≡⟨ sec' .glues f hf ⟩≡
      ps .part f _        ≡˘⟨ x .glues f (c⊆s f hf) ⟩≡˘
      A ⟪ f ⟫ x .whole    ∎

As a specialisation of the lemma above, we can show that is a sheaf for the pullback of any sieve. This is sharper than the pullback-stability property, but they differ exactly by the theorem above!

  is-sheaf-pullback
    : ∀ {V U} (c : J # U) (f : Hom V U) → is-sheaf₁ A (pullback f (J .cover c))
  is-sheaf-pullback c f p = ∥-∥-out! do
    (c' , sub) ← J .stable c f
    pure (is-sheaf-factor (pullback f (J .cover c)) c' sub p)

Saturating sites🔗

Putting the two previous batches of lemmas together, given a site we can define by induction a new site which definitionally enjoys these extra closure properties, but which has exactly the same sheaves as in the code, we refer to this as the Saturation of This is actually a pretty simple process:

  data _∋_ (J : Coverage C ℓs) : {U : ⌞ C ⌟} → Sieve C U → Type (o ⊔ ℓ ⊔ ℓs) where
    inc : ∀ {U} (c : J .covers U) → J ∋ J .cover c

    max : ∀ {U} {R : Sieve C U} → id ∈ R → J ∋ R

    local
      : ∀ {U R} (hr : J ∋ R) {S : Sieve C U}
      → (∀ {V} (f : Hom V U) (hf : f ∈ R) → J ∋ pullback f S)
      → J ∋ S

    pull : ∀ {U V} (h : Hom V U) {R : Sieve C U} (hr : J ∋ R) → J ∋ pullback h R

    squash : ∀ {U} {R : Sieve C U} → is-prop (J ∋ R)

In addition to the constructor which ensures that a sieve is each of the constructors corresponds exactly to one of the lemmas above:

Note that is-sheaf-factor can be derived, instead of being a constructor, as shown below. We also truncate this type to ensure that a sieve belongs to the saturation in at most one way.

  abstract
    incl
      : ∀ {J : Coverage C ℓs} {U} {R S : Sieve C U}
      → S ⊆ R → J ∋ S → J ∋ R
    incl {J = J} {S = S} sr us = local us λ f hf → subst (J ∋_) refl $
      max $ sr (f ∘ id) (S .closed hf id)

  Saturation : Coverage C ℓs → Coverage C (o ⊔ ℓ ⊔ ℓs)
  Saturation J = from-stable-property (J ∋_) λ f R s → pull f s

Proving that a is also a can be done very straightforwardly, by induction. However, there is a gotcha: to get the induction hypotheses we need for local without running afoul of the termination checker, we must strengthen the motive of induction from “ is a sheaf for any sieve” to “ is a sheaf for any pullback of a sieve”.

  is-sheaf-sat
    : is-sheaf J A
    → ∀ {V U R} (c : J ∋ R) (h : Hom V U)
    → is-sheaf₁ A (pullback h R)

To compensate for this extra strength, we must use is-sheaf-pullback at the “leaves” inc. Other than that, it’s a very straightforward recursive computation:

  is-sheaf-sat shf (inc x) h = is-sheaf-pullback shf x h

  is-sheaf-sat _ (max {R = R} p) h = is-sheaf-maximal A $
    subst (_∈ R) id-comm-sym (R .closed p h)

  is-sheaf-sat shf {V} (local {U} {R} hR {S} x) h =
    let
      rem₁ : ∀ {W} (f : Hom W V) → h ∘ f ∈ S
           → is-separated₁ A (pullback f (pullback h R))
      rem₁ f hhf = is-sheaf₁→is-separated₁ A _ $
        subst-is-sheaf₁ A pullback-∘ (is-sheaf-sat shf hR (h ∘ f))

      rem₂ : ∀ {W} (f : Hom W V) → h ∘ f ∈ R
           → is-sheaf₁ A (pullback f (pullback h S))
      rem₂ f hf = subst-is-sheaf₁ A (pullback-id ∙ pullback-∘) $
        is-sheaf-sat shf (x (h ∘ f) hf) id
    in is-sheaf-transitive A rem₁ rem₂ (is-sheaf-sat shf hR h)

  is-sheaf-sat shf (pull h {R} hR) g = subst-is-sheaf₁ A pullback-∘ $
    is-sheaf-sat shf hR (h ∘ g)

  is-sheaf-sat shf (squash {R} x y i) h p = is-contr-is-prop
    (is-sheaf-sat shf x h p)
    (is-sheaf-sat shf y h p) i

Showing that a is also a is immediate.

  is-sheaf-saturation : is-sheaf J A ≃ is-sheaf (Saturation J) A
  is-sheaf-saturation .fst sheaf = from-is-sheaf₁ λ (R , hR) → subst-is-sheaf₁ A pullback-id $ is-sheaf-sat sheaf hR id
  is-sheaf-saturation .snd = biimp-is-equiv! _ λ shf → from-is-sheaf₁ λ c →
    to-is-sheaf₁ shf (J .cover c , inc c)

  module is-sheaf-saturation = Equiv is-sheaf-saturation