module Cat.Diagram.Sieve where

Sieves🔗

Given a category $\mathcal{C}\text{,}$ a sieve on an object $c$ Is a subset of the maps $a\to c$ closed under composition: If $f\in S\text{,}$ then $(f\circ g)\in S\text{.}$ The data of a sieve on $c$ corresponds to the data of a subobject of $よ(c)\text{,}$ considered as an object of $\mathrm{PSh}(\mathcal{C})\text{.}$

Here, the subset is represented as the function arrows, which, given an arrow $f:a\to c$ (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 $a\to c\text{;}$ It represents the identity map $よ(c)\to よ(c)$ as a subfunctor. A $\kappa \text{-small}$ family of sieves can be intersected (the underlying predicate is the “$\kappa \text{-ary}$ conjunction” $\Pi$ — 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 $S$ be a sieve on $\mathcal{C}\text{.}$ We show that it determines a presheaf $S^{\prime }\text{,}$ and that this presheaf admits a monic natural transformation $S^{\prime }\hookrightarrow よ(c)\text{.}$ The functor determined by a sieve $S$ sends each object $d$ to the set of arrows $d\stackrel{f}{\to }c$ s.t. $f\in S\text{;}$ The functorial action is given by composition, as with the $\mathbf{Hom}$ 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 $S^{\prime }\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↪よ : ∀ {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 $R$ on $U\text{,}$ and any morphism $f:V\to U\text{,}$ then there is a natural way to restrict the $h_i$ to a sieve on $V\text{:}$ a morphism $g:V_i\to V$ belongs to the restriction if the composite $fg:V_i\to V\to U$ belongs to $R\text{.}$ We refer to the resulting sieve as the pullback of $R$ along $f$, and write it $f^{\ast }(R)\text{.}$

  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 $U$” as varying along $U$ as a parameter, the pullback operation becomes functorial. Since it is contravariant, this means that the assignment $U\mapsto \mathrm{Sieves}(U)$ is itself a presheaf on $U\text{.}$

  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 $X\to \mathrm{Sieves}$ correspond naturally to the subobjects of $X\text{.}$ Categorically, we say that $\mathrm{Sieves}$ is a subobject classifier in the category $\mathrm{PSh}(\mathcal{C})\text{.}$

  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 $(f_i:V_i\to U{)}_{i:I}$ is the collection of maps that factor through at least one of the $f_i\text{,}$ i.e., for a map $g:W\to U\text{,}$ it is the proposition $$\exists (i:I)(h:W\to V_i).f_i\circ h=g\text{.}$$

  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.