module Cat.Diagram.Sieve where

Sieves🔗

Given a category a sieve on an object is a subset of the maps closed under composition: if then The data of a sieve on corresponds to the data of a subobject of considered as an object of

Here, the subset is represented as the function arrows, which, given an arrow (and its domain), yields a proposition representing inclusion in the subset.

  record Sieve : Type (o  κ) where
    no-eta-equality
    field
      arrows :  {y}   (C.Hom y c)
      closed :  {y z f} (hf : f  arrows) (g : C.Hom y z)  (f C.∘ g)  arrows
  open Sieve public

The maximal sieve on an object is the collection of all maps It represents the identity map as a subfunctor. A family of sieves can be intersected (the underlying predicate is the “ conjunction” — the universal quantifier), and this represents a wide pullback of subobjects.

  maximal' :  {c}  Sieve C c
  maximal' .arrows x = ⊤Ω
  maximal' .closed g x = tt

  intersect :  {c} {I : Type } (F : I  Sieve C c)  Sieve C c
  intersect {I = I} F .arrows h = elΩ ((x : I)  h  F x)
  intersect {I = I} F .closed x g = inc λ i  F i .closed (□-out! x i) g

Representing subfunctors🔗

Let be a sieve on We show that it determines a presheaf and that this presheaf admits a monic natural transformation The functor determined by a sieve sends each object to the set of arrows s.t. The functorial action is given by composition, as with the functor.

  to-presheaf :  {c}  Sieve C c  PSh.Ob
  to-presheaf {c} sieve .F₀ d = el! (Σ[ f  C.Hom d c ] (f  sieve))
  to-presheaf sieve .F₁ f (g , s) = g C.∘ f , sieve .closed s _

That this functor is a subobject of follows straightforwardly: The injection map is given by projecting out the first component, which is an embedding (since “being in a sieve” is a proposition). Since natural transformations are monic if they are componentwise monic, and embeddings are monic, the result follows.

  to-presheaf↪よ :  {c} {S : Sieve C c}  to-presheaf S PSh.↪ よ₀ C c
  to-presheaf↪よ {S} .mor .η x (f , _) = f
  to-presheaf↪よ {S} .mor .is-natural x y f = refl
  to-presheaf↪よ {S} .monic g h path = ext λ i x  Σ-prop-path! (unext path i x)

Pullback of sieves🔗

If we have a sieve on and any morphism then there is a natural way to restrict the to a sieve on a morphism belongs to the restriction if the composite belongs to We refer to the resulting sieve as the pullback of along , and write it

  pullback :  {u v}  C.Hom v u  Sieve C u  Sieve C v
  pullback f s .arrows h = el (f C.∘ h  s) (hlevel 1)
  pullback f s .closed hf g = subst (_∈ s) (sym (C.assoc f _ g)) (s .closed hf g)

If we consider the collection of “sieves on ” as varying along as a parameter, the pullback operation becomes functorial. Since it is contravariant, this means that the assignment is itself a presheaf on

  abstract
    pullback-id :  {c} {s : Sieve C c}  pullback C.id s  s
    pullback-id {s = s} = ext λ h  Ω-ua
      (subst (_∈ s) (C.idl h))
      (subst (_∈ s) (sym (C.idl h)))

    pullback-∘
      :  {u v w} {f : C.Hom w v} {g : C.Hom v u} {R : Sieve C u}
       pullback (g C.∘ f) R  pullback f (pullback g R)
    pullback-∘ {f = f} {g} {R = R} = ext λ h  Ω-ua
      (subst (_∈ R) (sym (C.assoc g f h)))
      (subst (_∈ R) (C.assoc g f h))

This presheaf has an important universal property: the natural transformations correspond naturally to the subobjects of Categorically, we say that is a subobject classifier in the category for more details see subobject classifier presheaf.

  Sieves : Functor (C ^op) (Sets (o  ))
  Sieves .F₀ U .∣_∣ = Sieve C U
  Sieves .F₀ U .is-tr = hlevel 2
  Sieves .F₁ = pullback
  Sieves .F-id    = funext λ x  pullback-id
  Sieves .F-∘ f g = funext λ x  pullback-∘

Generated sieves🔗

Often, it’s more practical to define a family of maps, and to obtain a sieve from this family after the fact. To this end, we define a type Cover for families of maps into a common codomain, paired with their indexing type.

  record Cover (U :  C ) ℓ' : Type (o    lsuc ℓ') where
    field
      {index}  : Type ℓ'
      {domain} : index   C 
      map      :  i  Hom (domain i) U

The sieve generated by a cover is the collection of maps that factor through at least one of the i.e., for a map it is the proposition

  cover→sieve :  {ℓ' U}  Cover C U ℓ'  Sieve C U
  cover→sieve {U = U} f .arrows {W} g = elΩ do
    Σ[ i  f ] Σ[ h  C.Hom W (f .domain i) ] (f .map i C.∘ h  g)
  cover→sieve f .closed = rec! λ i h p g  inc (i , h C.∘ g , C.pulll p)

Since the primary purpose of Cover is to present sieves, we register an instance of the ⟦⟧-notation class, so that we can write ⟦ cov ⟧ instead of cover→sieve cov.

Sieves in a category🔗

We have defined sieves on an object above, but there is also a notion of sieve in a category a subcollection of the objects of such that if is a morphism and then

  record Sieve-in : Type (o  ) where
    no-eta-equality
    field
      objects :  C.Ob
      closed :  {x y} (hy : y  objects) (f : C.Hom x y)  x  objects
  open Sieve-in public

The two notions are related as follows:

  Sieve→Sieve-in/c : Sieve C c  Sieve-in (Slice C c)
  Sieve→Sieve-in/c s .objects (cut f) = s .arrows f
  Sieve→Sieve-in/c s .closed hy f = subst (_∈ s .arrows) (f .commutes)
    (s .closed hy (f .map))

  Sieve-in/c→Sieve : Sieve-in (Slice C c)  Sieve C c
  Sieve-in/c→Sieve s .arrows f = s .objects (cut f)
  Sieve-in/c→Sieve s .closed hf g = s .closed hf λ where
    .map  g
    .commutes  refl

  Sieve≃Sieve-in/c : Sieve C c  Sieve-in (Slice C c)
  Sieve≃Sieve-in/c .fst = Sieve→Sieve-in/c
  Sieve≃Sieve-in/c .snd = is-iso→is-equiv (iso Sieve-in/c→Sieve
     s  Sieve-in-path refl)  s  Sieve-path refl))

Furthermore, just as sieves on correspond to subobjects of the representable functor sieves in correspond to subobjects of the terminal presheaf, i.e. subterminal presheaves.

  Sieve-in→presheaf : Sieve-in C  PSh.Ob
  Sieve-in→presheaf s .F₀ c = el! (c  s .objects)
  Sieve-in→presheaf s .F₁ f hx = s .closed hx f
  Sieve-in→presheaf s .F-id = prop!
  Sieve-in→presheaf s .F-∘ _ _ = prop!

  Sieve-in→subterminal
    :  {S : Sieve-in C}  is-subterminal (PSh lzero C) (Sieve-in→presheaf S)
  Sieve-in→subterminal {S} = prop→is-subterminal-PSh _ C (Sieve-in→presheaf S)