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 $(C,J),$ then there are quite a few sieves for which $A$ is a sheaf but which are not required to be present in $J.$ 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 $(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.$
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:$

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!$ 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,$
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_{∗}(S)-sheaf$
for every
$f∈R.$
If
$R$
and
$S$
are not part of a site, then this condition does not suffice: we also
require that
$A$
be
$f_{∗}(R)-separated,$
for every
$f∈S.$

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
$R$
belongs to a site for which
$A$
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 $p$ on $S$ can be pulled back to give a patch $f_{∗}(p)$ on $f_{∗}(S),$ for any $f∈R;$ Since $A$ is an $f_{∗}(S)-sheaf,$ at each $f:V→U$ in $R,$ there is a unique $p_{′′}(f):A(V),$ and a short calculation shows that these $p_{′′}$ give a patch on $R.$

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-sheaf,$
so our patch
$p_{′′}$
on
$R$
glues to give an element
$s:A(U)$
— a section of
$p_{′′},$
even. We must now show that
$A(f)(s)=p(f),$
for
$f∈S.$
Since
$s$
only agrees with
$p_{′′}$
$R-locally,$
this might be a problem: that’s where the assumption that
$A$
is
$f_{∗}(R)-local$
comes in (for
$f∈S):$
we can reduce this to showing
$A(gf)(s)=A(g)(p(f)),$
with
$fg∈R.$
We would almost be in trouble again, since
$p_{′′}(fg)$
is only characterised
$S-locally,$
but we can appeal to separatedness *again*, this time at
$(fg)_{∗}(S).$
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 $(C,J)$ and a functor $A$ which is a $J-sheaf,$ we can show a few more pedestrian closure properties. First, $A$ is a sheaf for any sieve that contains a $J-covering$ sieve (call it $R):$

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

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

However, by passing to the pullback sieve $f_{∗}(R),$ we’re allowed to show this assuming that we have some $g:W→V,$ with $fg∈R.$ 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-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🔗

Putting the two previous batches of lemmas together, given a site
$J,$
we can define by induction a new site
$J$
which definitionally enjoys these extra closure properties, but which
has exactly the same sheaves as
$J;$
in the code, we refer to this as the `Saturation`

of
$J.$
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-covering$ sieve is $J-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-sheaf$
is also a
$J-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
$J-covering$
sieve” to
“$A$
is a sheaf for any *pullback of* a
$J-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 $J-sheaf$ is also a $J-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