Sieves in categories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-13.
Last modified on 2023-09-27.

module category-theory.sieves-in-categories where
open import category-theory.categories

open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels


A sieve S on an object X in a category C is a collection of morphisms into X which is closed under precomposition by arbitrary morphisms of C. In other words, for any morphism f : Y → X in S and any morphism g : Z → Y in C, the morphism f ∘ g : Z → X is in S.

The notion of sieve generalizes simultaneously the notion of right ideal in a monoid (a one-object category) and a lower set in a poset (a category with at most one morphism between any two objects).


module _
  {l1 l2 : Level} (C : Category l1 l2) (A : obj-Category C)

  is-sieve-prop-Category :
    { l3 : Level}
    ( S : (X Y : obj-Category C) 
    subtype l3 (hom-Category C X Y))  Prop (l1  l2  l3)
  is-sieve-prop-Category S =
      ( obj-Category C)
      ( λ X 
          ( obj-Category C)
          ( λ Y 
              ( obj-Category C)
              ( λ Z 
                  ( type-subtype (S Y X))
                  ( λ f 
                      ( hom-Category C Z Y)
                      ( λ g 
                        S Z X
                          ( comp-hom-Category
                              C (inclusion-subtype (S Y X) f) g))))))

  is-sieve-Category :
    { l3 : Level}
    ( S : (X Y : obj-Category C) 
    subtype l3 (hom-Category C X Y))  UU (l1  l2  l3)
  is-sieve-Category S = type-Prop (is-sieve-prop-Category S)

  is-prop-is-sieve-Category :
    { l3 : Level}
    ( S : (X Y : obj-Category C)  subtype l3 (hom-Category C X Y)) 
    is-prop (is-sieve-Category S)
  is-prop-is-sieve-Category S = is-prop-type-Prop (is-sieve-prop-Category S)

Recent changes