module Cat.Instances.Sheaves where

The topos of sheavesπŸ”—

This module collects a compendium of the nice properties enjoyed by the category of sheaves on a site.

Sh[_,_] : βˆ€ {β„“} (C : Precategory β„“ β„“) (J : Coverage C β„“) β†’ Precategory (lsuc β„“) β„“
Sh[ C , J ] = Sheaves J _

MonadicityπŸ”—

Since the sheafification construction provides a left adjoint to the fully faithful inclusion of presheaves into sheaves, we can immediately conclude that the category of sheaves on a site is monadic over the presheaves on that same site.

  Sheafification : Functor (PSh β„“ C) Sh[ C , J ]
  Sheafification = free-objects→functor (Small.make-free-sheaf J)

  Sheafification⊣ι : Sheafification ⊣ forget-sheaf J _
  Sheafification⊣ι = free-objectsβ†’left-adjoint (Small.make-free-sheaf J)

Note that since the category of is defined to literally have the same as the category of presheaves on the action of the forgetful functor on morphisms is definitionally the identity.

  Sheafification-is-reflective : is-reflective Sheafification⊣ι
  Sheafification-is-reflective = id-equiv

  Sheafification-is-monadic : is-monadic Sheafification⊣ι
  Sheafification-is-monadic = is-reflective→is-monadic _ id-equiv

Limits and colimitsπŸ”—

By general properties of reflective subcategories, we have that the category of sheaves on a site is complete and cocomplete; Completeness is by an equivalence with the Eilenberg-Moore category of the sheafification monad (which has all limits which does), and cocompleteness follows by computing the colimit in presheaves, then sheafifying the result.

  Sh[]-is-complete : is-complete β„“ β„“ Sh[ C , J ]
  Sh[]-is-complete = equivalence→complete
    (is-equivalence.inverse-equivalence Sheafification-is-monadic)
    (Eilenberg-Moore-is-complete
      (Functor-cat-is-complete (Sets-is-complete {ΞΉ = β„“} {β„“} {β„“})))

  Sh[]-is-cocomplete : is-cocomplete β„“ β„“ Sh[ C , J ]
  Sh[]-is-cocomplete F = done where
    psh-colim : Colimit (forget-sheaf J _ F∘ F)
    psh-colim = Functor-cat-is-cocomplete (Sets-is-cocomplete {ΞΉ = β„“} {β„“} {β„“}) _

    sheafified : Colimit ((Sheafification F∘ forget-sheaf J _) F∘ F)
    sheafified = subst Colimit F∘-assoc $
      left-adjoint-colimit Sheafification⊣ι psh-colim

    done = natural-iso→colimit
      (F∘-iso-id-l (is-reflectiveβ†’counit-iso Sheafification⊣ι id-equiv))
      sheafified

Concrete limitsπŸ”—

The computations above compute all limits, even the finite limits with known shape such as products and the terminal object, as an equaliser between maps to and from a very big product. To make working with finite limits of sheaves smoother, we specialise the proof that sheaves are closed under limits to these finite cases:

  Sh[]-products : has-products Sh[ C , J ]
  Sh[]-products (A , ashf) (B , bshf) = prod where
    prod' = PSh-products {C = C} A B

    prod : Product Sh[ C , J ] _ _
    prod .apex .fst = prod' .apex
    prod .π₁ = prod' .π₁
    prod .Ο€β‚‚ = prod' .Ο€β‚‚
    prod .has-is-product .⟨_,_⟩  = prod' .⟨_,_⟩
    prod .has-is-product .Ο€β‚βˆ˜βŸ¨βŸ©  = prod' .Ο€β‚βˆ˜βŸ¨βŸ©
    prod .has-is-product .Ο€β‚‚βˆ˜βŸ¨βŸ©  = prod' .Ο€β‚‚βˆ˜βŸ¨βŸ©
    prod .has-is-product .unique = prod' .unique

    prod .apex .snd = is-sheaf-limit
      {F = 2-object-diagram _ _} {ψ = 2-object-nat-trans _ _}
      (is-product→is-limit (PSh ℓ C) (prod' .has-is-product))
      (Ξ» { true β†’ ashf ; false β†’ bshf })

The terminal object in sheaves is even easier to define:

  Sh[]-terminal : Terminal Sh[ C , J ]
  Sh[]-terminal .top .fst = PSh-terminal {C = C} .top
  Sh[]-terminal .has⊀ (S , _) = PSh-terminal {C = C} .has⊀ S

  Sh[]-terminal .top .snd .whole _ _     = lift tt
  Sh[]-terminal .top .snd .glues _ _ _ _ = refl
  Sh[]-terminal .top .snd .separate _ _  = refl

Cartesian closureπŸ”—

Since sheaves are an exponential ideal in presheaves, meaning that is a sheaf whenever is, we can conclude that the category of sheaves on a site is also Cartesian closed.

  Sh[]-cc : Cartesian-closed Sh[ C , J ] Sh[]-products Sh[]-terminal
  Sh[]-cc .has-exp (A , _) (B , bshf) = exp where
    exp' = PSh-closed {C = C} .has-exp A B

    exp : Exponential Sh[ C , J ] _ _ _ _
    exp .B^A .fst = exp' .B^A
    exp .B^A .snd = is-sheaf-exponential J A B bshf
    exp .ev       = exp' .ev
    exp .has-is-exp .Ζ›        = exp' .Ζ›
    exp .has-is-exp .commutes = exp' .commutes
    exp .has-is-exp .unique   = exp' .unique