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