module Cat.Diagram.Sieve where

# Sievesπ

Given a category
$C,$
a **sieve** on an object
$c$
Is a subset of the maps
$aβc$
closed under composition: If
$fβS,$
then
$(fβg)βS.$
The data of a sieve on
$c$
corresponds to the data of a subobject of
$γ(c),$
considered as an object of
$PSh(C).$

Here, the subset is represented as the function `arrows`

, which, given an arrow
$f:aβc$
(and its domain), yields a proposition representing inclusion in the
subset.

record Sieve : Type (o β ΞΊ) where field arrows : β {y} β β (C.Hom y c) closed : β {y z f} (g : C.Hom y z) β f β arrows β (f C.β g) β arrows open Sieve public

instance Membership-Sieve : β {o β} {C : Precategory o β} {c d} β Membership (C .Precategory.Hom d c) (Sieve C c) _ Membership-Sieve = record { _β_ = Ξ» x S β x β S .Sieve.arrows }

The `maximal`

sieve on an object
is the collection of *all* maps
$aβc;$
It represents the identity map
$γ(c)βγ(c)$
as a subfunctor. A $ΞΊ-small$
family of sieves can be intersected (the underlying predicate is the
β$ΞΊ-ary$
conjunctionβ
$Ξ$
β the universal quantifier), and this represents a wide pullback of
subobjects.

module _ {o ΞΊ : _} (C : Precategory o ΞΊ) (c : β C β) where private module C = Cat.Reasoning C module PSh = Cat.Reasoning (PSh ΞΊ C) open PSh._βͺ_ open _=>_ open Functor

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 $S$ be a sieve on $C.$ We show that it determines a presheaf $S_{β²},$ and that this presheaf admits a monic natural transformation $S_{β²}βͺγ(c).$ The functor determined by a sieve $S$ sends each object $d$ to the set of arrows $dfβc$ s.t. $fβS;$ The functorial action is given by composition, as with the $Hom$ 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

to-presheaf sieve .F-id = funext Ξ» _ β Ξ£-prop-path! (C.idr _) to-presheaf sieve .F-β f g = funext Ξ» _ β Ξ£-prop-path! (C.assoc _ _ _)

That this functor is a subobject of $γ$ follows straightforwardly: The injection map $S_{β²}βͺγ(c)$ 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)