open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Elements
open import Cat.Site.Constructions
open import Cat.Functor.Kan.Base
open import Cat.Diagram.Sieve
open import Cat.Functor.Hom
open import Cat.Site.Base hiding (whole ; glues ; separate)
open import Cat.Prelude

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

module Cat.Site.Closure where

Closure properties of sites🔗

module _ {o ℓ ℓs} {C : Precategory o ℓ} (A : Functor (C ^op) (Sets ℓs)) where
  open Cat C
  open Section
  open Patch
  open is-sheaf
  private module A = Psh A

If $A$ is a sheaf on a site $(\mathcal{C},J)\text{,}$ then there are quite a few sieves for which $A$ is a sheaf but which are not required to be present in $J\text{.}$ 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 $J$ under these extra constructions does not change the theory of “sheaves on $(\mathcal{C},J)$”, 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 $A\text{.}$ We will fix a completely arbitrary functor $A$ for the remainder of this section. The first thing we note is that, if a sieve $S$ contains the identity, then $A$ is a sheaf for $S\text{:}$

  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 $S$ which contains an isomorphism. Intuitively, this is because any sieve on $U$ which contains the identity (or an isomorphism) says that global data on $U$ can be constructed locally… on all of $U\text{!}$ 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 $A$ is a sheaf for a sieve $R\text{,}$ and we have some other sieve $S$ which we want to show $A$ is a sheaf for, it (almost) suffices to show that A is an $f^{\ast }(S)\text{-sheaf}$ for every $f\in R\text{.}$ If $R$ and $S$ are not part of a site, then this condition does not suffice: we also require that $A$ be $f^{\ast }(R)\text{-separated,}$ for every $f\in S\text{.}$

  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 $p$ on $S$ can be pulled back to give a patch $f^{\ast }(p)$ on $f^{\ast }(S)\text{,}$ for any $f\in R\text{;}$ Since $A$ is an $f^{\ast }(S)\text{-sheaf,}$ at each $f:V\to U$ in $R\text{,}$ there is a unique $p^{\prime \prime }(f):A(V)\text{,}$ and a short calculation shows that these $p^{\prime \prime }$ give a patch on $R\text{.}$

    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, $A$ is an $R\text{-sheaf,}$ so our patch $p^{\prime \prime }$ on $R$ glues to give an element $s:A(U)$ — a section of $p^{\prime \prime }\text{,}$ even. We must now show that $A(f)(s)=p(f)\text{,}$ for $f\in S\text{.}$ Since $s$ only agrees with $p^{\prime \prime }$ $R\text{-locally,}$ this might be a problem: that’s where the assumption that $A$ is $f^{\ast }(R)\text{-local}$ comes in (for $f\in S\text{):}$ we can reduce this to showing $A(gf)(s)=A(g)(p(f))\text{,}$ with $fg\in R\text{.}$ We would almost be in trouble again, since $p^{\prime \prime }(fg)$ is only characterised $S\text{-locally,}$ but we can appeal to separatedness again, this time at $(fg{)}^{\ast }(S)\text{.}$ 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 }) }

module
  _ {o ℓ ℓs ℓc} {C : Precategory o ℓ} {J : Coverage C ℓc}
    {A : Functor (C ^op) (Sets ℓs)} (shf : is-sheaf J A)
  where

  open Precategory C
  open is-sheaf
  open Section
  open Patch

  private
    module A = Psh A
    module shf = is-sheaf shf

On a site🔗

Now specialising to a site $(\mathcal{C},J)$ and a functor $A$ which is a $J\text{-sheaf,}$ we can show a few more pedestrian closure properties. First, $A$ is a sheaf for any sieve that contains a $J\text{-covering}$ sieve (call it $R\text{):}$

  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 $p$ is a patch on $S$ and $S$ contains $R\text{,}$ we can restrict $p$ to a patch $p^{\prime }$ on $R\text{.}$ Gluing $p^{\prime }\text{,}$ we obtain a section $s$ for $p\text{!}$ Showing this requires using the pullback-stability of $J\text{,}$ though: We must show that $A(f)(s)=p(f)\text{,}$ for $f:V\to U\in S\text{,}$ but $p$ is only characterised for $f\in R\text{!}$

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

However, by passing to the pullback sieve $f^{\ast }(R)\text{,}$ we’re allowed to show this assuming that we have some $g:W\to V\text{,}$ with $fg\in R\text{.}$ 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 $A$ is a sheaf for the pullback of any $J\text{-covering}$ 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🔗

module _ {o ℓ ℓs} {C : Precategory o ℓ} where
  open Precategory C using (Hom ; id ; _∘_)

Putting the two previous batches of lemmas together, given a site $J\text{,}$ we can define by induction a new site $\hat{J}$ which definitionally enjoys these extra closure properties, but which has exactly the same sheaves as $J\text{;}$ in the code, we refer to this as the Saturation of $J\text{.}$ 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 $J\text{-covering}$ sieve is $\hat{J}\text{-covering,}$ each of the constructors corresponds exactly to one of the lemmas above:

• max corresponds to is-sheaf-maximal;
• local corresponds to is-sheaf-transitive;
• pull corresponds to is-sheaf-pullback.

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

  instance
    H-Level-∋ : ∀ {J : Coverage C ℓs} {U} {S : Sieve C U} {n} → H-Level (J ∋ S) (suc n)
    H-Level-∋ = prop-instance squash

module _ {o ℓ ℓs ℓp} {C : Precategory o ℓ} {J : Coverage C ℓs} {A : Functor (C ^op) (Sets ℓp)}  where
  open Cat C

Proving that a $J\text{-sheaf}$ is also a $\hat{J}\text{-sheaf}$ 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 “$A$ is a sheaf for any $\hat{J}\text{-covering}$ sieve” to “$A$ is a sheaf for any pullback of a $\hat{J}\text{-covering}$ 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 $\hat{J}\text{-sheaf}$ is also a $J\text{-sheaf}$ 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

module sat {o ℓ ℓs ℓc} {C : Precategory o ℓ} {J : Coverage C ℓc} {A : Functor (C ^op) (Sets ℓs)} (shf : is-sheaf J A) where
  private module shf = is-sheaf (is-sheaf-saturation.to shf)

  whole : ∀ {U} {S : Sieve C U} (w : J ∋ S) (p : Patch A S) → A ʻ U
  whole w = shf.whole (_ , w)

  abstract
    glues : ∀ {U} {S : Sieve C U} (w : J ∋ S) (p : Patch A S) → is-section A (whole w p) p
    glues w = shf.glues (_ , w)

    separate : ∀ {U} {S : Sieve C U} (w : J ∋ S) → is-separated₁ A S
    separate w = shf.separate (_ , w)

  split : ∀ {U} {S : Sieve C U} (w : J ∋ S) (p : Patch A S) → Section A p
  split w p .Section.whole = whole w p
  split w p .Section.glues = glues w p