module Cat.Diagram.Sieve {o ΞΊ : _} (C : Precategory o ΞΊ) (c : Precategory.Ob C) where
private module C = Cat.Reasoning C module PSh = Cat.Reasoning (PSh ΞΊ C) open PSh._βͺ_ open _=>_ open Functor
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 β lsuc ΞΊ) where field arrows : {y : C.Ob} β β (C.Hom y c) closed : {y z : _} {f : _} (g : C.Hom y z) β f β arrows β (f C.β g) β arrows open Sieve
The maximal
sieve on an object
is the collection of all maps
;
It represents the identity map
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.
maximalβ² : Sieve maximalβ² .arrows x = el β€ hlevel! maximalβ² .closed g x = tt intersect : β {I : Type ΞΊ} (F : I β Sieve) β Sieve intersect {I = I} F .arrows h = elΞ© ((x : I) β h β F x .arrows) 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 β PSh.Ob to-presheaf sieve .Fβ d = el! (Ξ£[ f β C.Hom d c ] (f β sieve .arrows)) to-presheaf sieve .Fβ f (g , s) = g C.β f , sieve .closed _ s
to-presheaf sieve .F-id = funext Ξ» _ β Ξ£-prop-path (Ξ» _ β hlevel!) (C.idr _) to-presheaf sieve .F-β f g = funext Ξ» _ β Ξ£-prop-path (Ξ» _ β hlevel!) (C.assoc _ _ _)
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} β 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 = Nat-path Ξ» x β embeddingβmonic (Subset-proj-embedding (Ξ» _ β S .arrows _ .is-tr)) (g .Ξ· x) (h .Ξ· x) (path Ξ·β x)