open import Cat.Instances.Functor
open import Cat.Functor.Hom
open import Cat.Prelude

open import Data.Power

import Cat.Reasoning

module Cat.Diagram.Sieve {o ΞΊ : _} (C : Precategory o ΞΊ) (c : Precategory.Ob C) where


Given a category C\mathcal{C}, a sieve on an object cc Is a subset of the maps aβ†’ca \to c closed under composition: If f∈Sf \in S, then (f∘g)∈S(f \circ g) \in S. The data of a sieve on cc corresponds to the data of a subobject of γ‚ˆ(c){γ‚ˆ}(c), considered as an object of PSh(C){{\mathrm{PSh}}}(\mathcal{C}).

Here, the subset is represented as the function arrows, which, given an arrow f:a→cf : a \to c (and its domain), yields a proposition representing inclusion in the subset.

record Sieve : Type (o βŠ” lsuc ΞΊ) where
    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 aβ†’ca \to c; It represents the identity map γ‚ˆ(c)β†’γ‚ˆ(c){γ‚ˆ}(c) \to {γ‚ˆ}(c) as a subfunctor. A ΞΊ\kappa-small family of sieves can be intersected (the underlying predicate is the β€œΞΊ\kappa-ary conjunction” Ξ \Pi β€” 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 SS be a sieve on C\mathcal{C}. We show that it determines a presheaf Sβ€²S', and that this presheaf admits a monic natural transformation Sβ€²β†ͺγ‚ˆ(c)S' {\hookrightarrow}{γ‚ˆ}(c). The functor determined by a sieve SS sends each object dd to the set of arrows dβ†’fcd {\xrightarrow{f}} c s.t. f∈Sf \in S; The functorial action is given by composition, as with the Hom{\mathbf{Hom}} 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

That this functor is a subobject of γ‚ˆ{γ‚ˆ} follows straightforwardly: The injection map Sβ€²β†ͺγ‚ˆ(c)S' {\hookrightarrow}{γ‚ˆ}(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} β†’ 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)