open import Cat.Diagram.Sieve
open import Cat.Prelude

import Cat.Site.Closure as Cl
import Cat.Site.Base as Site

open Site using (Coverage ; covers ; cover)
open Cl using (_βˆ‹_)

module Cat.Site.Grothendieck where

Grothendieck sitesπŸ”—

A Grothendieck topology on a category is function assigning to each a predicate on the sieves on satisfying the closure properties of sites. Every topology generates a coverage (where the space of sieves that cover is the total space of and, conversely, every site can be saturated to give a topology.

record Topology {o β„“} (C : Precategory o β„“) β„“s : Type (o βŠ” β„“ βŠ” lsuc β„“s) where
  open Precategory C
  field
    covering : (U : ⌞ C ⌟) (R : Sieve C U) β†’ Type β„“s

  _β—€_ : (U : ⌞ C ⌟) (R : Sieve C U) β†’ Type β„“s
  _β—€_ = covering

  field
    has-is-prop : βˆ€ {U} {R : Sieve C U} β†’ is-prop (U β—€ R)

    stable
      : βˆ€ {U V} (h : Hom V U) {R : Sieve C U} (hr : U β—€ R)
      β†’ V β—€ (pullback h R)

    maximal
      : βˆ€ {U} {R : Sieve C U} β†’ id ∈ R β†’ U β—€ R

    local :
      βˆ€ {U} {R : Sieve C U} (hr : U β—€ R) {S : Sieve C U}
      β†’ (βˆ€ {V} (f : Hom V U) (hf : f ∈ R) β†’ V β—€ pullback f S)
      β†’ U β—€ S

The main interest in defining this notion is that if we start with a topology demote it to a coverage and then saturate this coverage, we obtain a topology identical to the one we started with. Since many notions in sheaf theory speak of sieves belonging to the saturation of a coverage, if we know that we started with a topology, then we know that we truly haven’t added any β€œnew” coverings.

  from-topology : Coverage C _
  from-topology .covers U = βˆ«β‚š (U β—€_)
  from-topology .cover = fst
  from-topology .Site.stable (R , P) f = inc ((pullback f R , stable f P) , Ξ» h x β†’ x)

  unsaturate : βˆ€ {U} {R : Sieve C U} β†’ from-topology βˆ‹ R β†’ U β—€ R
  unsaturate = go where
    go : βˆ€ {U} {R : Sieve C U} β†’ from-topology βˆ‹ R β†’ U β—€ R
    go (Cl.inc (_ , Ξ±)) = Ξ±
    go (Cl.max x) = maximal x
    go (Cl.local s p) = local (go s) Ξ» f h β†’ go (p f h)
    go (Cl.pull h x) = stable h (go x)
    go (Cl.squash x y i) = has-is-prop (go x) (go y) i

open Topology using (covering ; has-is-prop ; stable ; maximal ; local) public

module _ {o h β„“s} {C : Precategory o h} where instance
  Membership-Topology : βˆ€ {U} β†’ Membership (Sieve C U) (Topology C β„“s) β„“s
  Membership-Topology = record { _∈_ = Ξ» S T β†’ T .covering _ S }

  Funlike-Topology : Funlike (Topology C β„“s) ⌞ C ⌟ Ξ» U β†’ Sieve C U β†’ Type β„“s
  Funlike-Topology .Funlike._#_ T = T .covering

Closure-topology : βˆ€ {o h β„“s} {C : Precategory o h} β†’ Coverage C β„“s β†’ Topology C (o βŠ” h βŠ” β„“s)
Closure-topology J .covering _ R = J βˆ‹ R
Closure-topology J .has-is-prop = hlevel 1
Closure-topology J .stable = Cl.pull
Closure-topology J .maximal = Cl.max
Closure-topology J .local = Cl.local