module Cat.Diagram.Sieve where


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
      arrows : βˆ€ {y} β†’ β„™ (C.Hom y c)
      closed : βˆ€ {y z f} (g : C.Hom y z) β†’ f ∈ arrows β†’ (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' : Sieve C c
  maximal' .arrows x = ⊀Ω
  maximal' .closed g x = tt

  intersect : βˆ€ {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 g x = inc Ξ» i β†’ F i .closed g (out! x i)

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 : Sieve C c β†’ PSh.Ob
  to-presheaf 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β†ͺγ‚ˆ : {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)