open import Cat.CartesianClosed.Instances.PSh
open import Cat.Diagram.Sieve
open import Cat.Functor.Base
open import Cat.Site.Closure
open import Cat.Site.Base
open import Cat.Prelude

import Cat.Functor.Reasoning.Presheaf as PSh
import Cat.Reasoning as Cat

open Functor
open _=>_
module Cat.Instances.Sheaves.Exponentials where

Exponentials of sheaves🔗

In this module we will show that the sheaves, for a coverage are an exponential ideal in This means that, if is a and is any presheaf at all, then the exponential object is also a The proof will rely crucially on the closure properties of sites. For this proof, keep in that the exponential is constructed1 to have sections 

is-sheaf-exponential
  : ∀ {ℓ ℓs} {C : Precategory ℓ ℓ} (J : Coverage C ℓs) (A B : Functor (C ^op) (Sets ℓ))
  → is-sheaf J B
  → is-sheaf J (PSh[_,_] {C = C} A B)
is-sheaf-exponential {C = C} J A B bshf = from-is-sheaf₁ λ c → done where
  open Cat C
  module bshf = sat bshf

  psh = PSh[_,_] {C = C} A B

The first thing we’ll do is show that is Let be a sieve of and be sections at which are equal, i.e. such that, for we have, for all maps and we have This condition is a bit of a mouthful, but all we’ve done is unfold the definition of equality in

What we must show, however, is that for a totally arbitrary and But, since this is an equality in and is a it suffices to choose a sieve of and to show this equality i.e. to show for any Note that, by naturality, these are equal to resp. We can then choose which lets us apply our equality (since means This concludes the proof that is 

  abstract
    sep : {U : ⌞ C ⌟} {c : J ʻ U} → is-separated₁ psh (J .cover c)
    sep {c = c} {x} {y} loc = ext λ V f z → bshf.separate (pull f (inc c)) λ g hg →
      B ⟪ g ⟫ x .η V (f , z)             ≡˘⟨ x .is-natural _ _ _ $ₚ _ ⟩
      x .η _ (f ∘ g , A ⟪ g ⟫ z)         ≡⟨ ap (x .η _) (Σ-pathp (intror refl) refl) ⟩
      x .η _ ((f ∘ g) ∘ id , A ⟪ g ⟫ z)  ≡⟨ loc (f ∘ g) hg ηₚ _ $ₚ _ ⟩
      y .η _ ((f ∘ g) ∘ id , A ⟪ g ⟫ z)  ≡˘⟨ ap (y .η _) (Σ-pathp (intror refl) refl) ⟩
      y .η _ (f ∘ g , A ⟪ g ⟫ z)         ≡⟨ y .is-natural _ _ _ $ₚ _ ⟩
      B ⟪ g ⟫ y .η V (f , z)             ∎

The proof of separatedness demonstrates the general schema for shuffling between local equality of natural transformations and local equality of their components, by passing to a pullback. The rest of the proof essentially follows from similar calculations.

This will also be the strategy to show that admits sections! To put together a section for a patch for a sieve it suffices to do so at each component; so we’ll start by showing that descends to a patch for on for any as long as we’re given Each part of is given by evaluating the corresponding part of 

  module _ {U} {c : J ʻ U} (p : Patch psh (J .cover c)) where
    p' : ∀ {V} (e : A ʻ V) (f : Hom V U) → Patch B (pullback f (J .cover c))
    p' e f .part g hg = p .part (f ∘ g) hg .η _ (id , A ⟪ g ⟫ e)
    p' e f .patch g hg h hh =
      B ⟪ h ⟫ p .part (f ∘ g) _ .η _ (id , A ⟪ g ⟫ e)          ≡˘⟨ p .part (f ∘ g) hg .is-natural _ _ _ $ₚ (id , A ⟪ g ⟫ e) ⟩
      p .part (f ∘ g) _ .η _ (id ∘ h , A ⟪ h ⟫ (A ⟪ g ⟫ e))    ≡⟨ ap (λ it → p .part (f ∘ g) hg .η _ (it , A ⟪ h ⟫ (A ⟪ g ⟫ e))) id-comm-sym ⟩
      p .part (f ∘ g) _ .η _ (h ∘ id , A ⟪ h ⟫ (A ⟪ g ⟫ e))    ≡⟨ p .patch (f ∘ g) hg h (subst (_∈ J .cover c) (assoc _ _ _) hh) ηₚ _ $ₚ (id , _) ⟩
      p .part ((f ∘ g) ∘ h) _ .η _ (id , A ⟪ h ⟫ (A ⟪ g ⟫ e))  ≡⟨ app p (sym (assoc f g h)) ηₚ _ $ₚ _ ⟩
      p .part (f ∘ g ∘ h) _ .η _ (id , A ⟪ h ⟫ (A ⟪ g ⟫ e))    ≡⟨ ap (λ e → p .part (f ∘ g ∘ h) hh .η _ (id , e)) (sym (A .F-∘ _ _ # _)) ⟩
      p .part (f ∘ g ∘ h) _ .η _ (id , A ⟪ g ∘ h ⟫ e)          ∎

Then, since is a for the component at we can glue together the relevant By the same strategy by which we showed separatedness we can show naturality, and that the resulting natural transformation really does glue 

    s' : Section (PSh[_,_] {C = C} A B) p
    s' .whole .η x (f , e) = it .whole module s' where
      it : Section B (p' e f)
      it = bshf.split (pull f (inc c)) (p' e f)

    s' .whole .is-natural x y f = ext λ g e → bshf.separate (pull (g ∘ f) (inc c)) λ h hh →
      let clo = subst (_∈ J .cover c) (sym (assoc _ _ _)) hh in
      B ⟪ h ⟫ (s'.it y (g ∘ f) (A ⟪ f ⟫ e) .whole)            ≡⟨ s'.it y (g ∘ f) (A ⟪ f ⟫ e) .glues _ hh ⟩
      p .part ((g ∘ f) ∘ h) _ .η _ (id , A ⟪ h ⟫ (A ⟪ f ⟫ e)) ≡˘⟨ (λ i → p .part (assoc g f h i) (coe1→i (λ i → assoc g f h i ∈ J .cover c) i hh) .η _ (id , A .F-∘ h f i e)) ⟩
      p .part (g ∘ f ∘ h) _ .η _ (id , A ⟪ f ∘ h ⟫ e)         ≡˘⟨ sym (B .F-∘ _ _ # _) ∙ s'.it x g e .glues (f ∘ h) clo ⟩
      B ⟪ h ⟫ (B ⟪ f ⟫ (s'.it x g e .whole))                  ∎

    s' .glues f hf = ext λ x g e →
      let clo = J .cover c .closed (J .cover c .closed hf g) id in
      s'.it x (f ∘ g) e .whole                         ≡˘⟨ B .F-id # _ ⟩
      (B ⟪ id ⟫ s'.it x (f ∘ g) e .whole)              ≡⟨ s'.it x (f ∘ g) e .glues id clo ⟩
      p .part ((f ∘ g) ∘ id) _ .η x (id , A ⟪ id ⟫ e)  ≡⟨ ap₂ (λ i1 i2 → p .part i1 i2 .η x (id , A ⟪ id ⟫ e)) (idr (f ∘ g)) prop! ⟩
      p .part (f ∘ g) _ .η x (id , A ⟪ id ⟫ e)         ≡⟨ sym (p .patch f hf g (J .cover c .closed hf g) ηₚ _ $ₚ (id , A ⟪ id ⟫ e)) ⟩
      p .part f hf .η x (g ∘ id , A ⟪ id ⟫ e)          ≡⟨ ap (p .part f hf .η x) (Σ-pathp (idr g) (A .F-id # _)) ⟩
      p .part f hf .η x (g , e)                        ∎

    done = from-is-separated₁ psh sep s'

  1. If you’re worried about the dependence on the concrete construction, don’t be: this always holds as a natural isomorphism, by the yoneda lemma:

    ↩︎