Precategory of elements of a presheaf

Content created by Daniel Gratzer, Egbert Rijke, Elisabeth Stenholm and Fredrik Bakke.

Created on 2023-11-27.
Last modified on 2024-03-11.

module category-theory.precategory-of-elements-of-a-presheaf where
Imports 
open import category-theory.functors-precategories
open import category-theory.opposite-precategories
open import category-theory.precategories
open import category-theory.presheaf-categories

open import foundation.action-on-identifications-functions
open import foundation.category-of-sets
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

Idea

Let F : Cᵒᵖ → Set be a presheaf on a precategory C. The precategory of elements of F consists of:

  • Objects are pairs (A , a) where A is an object in C and a : F A.
  • A morphism from (A , a) to (B , b) is a morphism f : hom A B in the precategory C equipped with an identification a = F f b.

Definitions

module _
  {l1 l2 l3} (C : Precategory l1 l2) (F : presheaf-Precategory C l3)
  where

  obj-precategory-of-elements-presheaf-Precategory : UU (l1 ⊔ l3)
  obj-precategory-of-elements-presheaf-Precategory =
    Σ (obj-Precategory C) (element-presheaf-Precategory C F)

  hom-set-precategory-of-elements-presheaf-Precategory :
    (A B : obj-precategory-of-elements-presheaf-Precategory) → Set (l2 ⊔ l3)
  hom-set-precategory-of-elements-presheaf-Precategory (A , a) (B , b) =
    set-subset
      ( hom-set-Precategory C A B)
      ( λ f →
        Id-Prop
          ( element-set-presheaf-Precategory C F A)
          ( a)
          ( action-presheaf-Precategory C F f b))

  hom-precategory-of-elements-presheaf-Precategory :
    (A B : obj-precategory-of-elements-presheaf-Precategory) → UU (l2 ⊔ l3)
  hom-precategory-of-elements-presheaf-Precategory A B =
    type-Set (hom-set-precategory-of-elements-presheaf-Precategory A B)

  eq-hom-precategory-of-elements-presheaf-Precategory :
    {X Y : obj-precategory-of-elements-presheaf-Precategory}
    (f g : hom-precategory-of-elements-presheaf-Precategory X Y) →
    (pr1 f ＝ pr1 g) → f ＝ g
  eq-hom-precategory-of-elements-presheaf-Precategory f g =
    eq-type-subtype
      ( λ h →
        Id-Prop
          ( element-set-presheaf-Precategory C F _)
          ( _)
          ( action-presheaf-Precategory C F h _))

  comp-hom-precategory-of-elements-presheaf-Precategory :
    {X Y Z : obj-precategory-of-elements-presheaf-Precategory} →
    hom-precategory-of-elements-presheaf-Precategory Y Z →
    hom-precategory-of-elements-presheaf-Precategory X Y →
    hom-precategory-of-elements-presheaf-Precategory X Z
  comp-hom-precategory-of-elements-presheaf-Precategory
    ( g , q)
    ( f , p) =
    ( comp-hom-Precategory C g f ,
      ( p) ∙
      ( ap (action-presheaf-Precategory C F f) q) ∙
      ( inv (preserves-comp-action-presheaf-Precategory C F g f _)))

  associative-comp-hom-precategory-of-elements-presheaf-Precategory :
    {X Y Z W : obj-precategory-of-elements-presheaf-Precategory} →
    (h : hom-precategory-of-elements-presheaf-Precategory Z W)
    (g : hom-precategory-of-elements-presheaf-Precategory Y Z)
    (f : hom-precategory-of-elements-presheaf-Precategory X Y) →
    comp-hom-precategory-of-elements-presheaf-Precategory
      ( comp-hom-precategory-of-elements-presheaf-Precategory h g)
      ( f) ＝
    comp-hom-precategory-of-elements-presheaf-Precategory
      ( h)
      ( comp-hom-precategory-of-elements-presheaf-Precategory g f)
  associative-comp-hom-precategory-of-elements-presheaf-Precategory h g f =
    eq-hom-precategory-of-elements-presheaf-Precategory
      ( comp-hom-precategory-of-elements-presheaf-Precategory
        ( comp-hom-precategory-of-elements-presheaf-Precategory h g)
        ( f))
      ( comp-hom-precategory-of-elements-presheaf-Precategory
        ( h)
        ( comp-hom-precategory-of-elements-presheaf-Precategory g f))
      ( associative-comp-hom-Precategory C (pr1 h) (pr1 g) (pr1 f))

  id-hom-precategory-of-elements-presheaf-Precategory :
    {X : obj-precategory-of-elements-presheaf-Precategory} →
    hom-precategory-of-elements-presheaf-Precategory X X
  pr1 id-hom-precategory-of-elements-presheaf-Precategory =
    id-hom-Precategory C
  pr2 id-hom-precategory-of-elements-presheaf-Precategory =
    inv (preserves-id-action-presheaf-Precategory C F _)

  left-unit-law-comp-hom-precategory-of-elements-presheaf-Precategory :
    {X Y : obj-precategory-of-elements-presheaf-Precategory} →
    (f : hom-precategory-of-elements-presheaf-Precategory X Y) →
    comp-hom-precategory-of-elements-presheaf-Precategory
      ( id-hom-precategory-of-elements-presheaf-Precategory)
      ( f) ＝
    f
  left-unit-law-comp-hom-precategory-of-elements-presheaf-Precategory f =
    eq-hom-precategory-of-elements-presheaf-Precategory
      ( comp-hom-precategory-of-elements-presheaf-Precategory
        ( id-hom-precategory-of-elements-presheaf-Precategory)
        ( f))
      ( f)
      ( left-unit-law-comp-hom-Precategory C (pr1 f))

  right-unit-law-comp-hom-precategory-of-elements-presheaf-Precategory :
    {X Y : obj-precategory-of-elements-presheaf-Precategory} →
    (f : hom-precategory-of-elements-presheaf-Precategory X Y) →
    comp-hom-precategory-of-elements-presheaf-Precategory
      ( f)
      ( id-hom-precategory-of-elements-presheaf-Precategory) ＝
    f
  right-unit-law-comp-hom-precategory-of-elements-presheaf-Precategory f =
    eq-hom-precategory-of-elements-presheaf-Precategory
      ( comp-hom-precategory-of-elements-presheaf-Precategory
        ( f)
        ( id-hom-precategory-of-elements-presheaf-Precategory))
      ( f)
      ( right-unit-law-comp-hom-Precategory C (pr1 f))

  precategory-of-elements-presheaf-Precategory : Precategory (l1 ⊔ l3) (l2 ⊔ l3)
  precategory-of-elements-presheaf-Precategory =
    make-Precategory
      ( obj-precategory-of-elements-presheaf-Precategory)
      ( hom-set-precategory-of-elements-presheaf-Precategory)
      ( comp-hom-precategory-of-elements-presheaf-Precategory)
      ( λ X → id-hom-precategory-of-elements-presheaf-Precategory {X})
      ( associative-comp-hom-precategory-of-elements-presheaf-Precategory)
      ( left-unit-law-comp-hom-precategory-of-elements-presheaf-Precategory)
      ( right-unit-law-comp-hom-precategory-of-elements-presheaf-Precategory)

The projection from the category of elements of a presheaf to the base category

module _ {l1 l2 l3} (C : Precategory l1 l2)
  (F : functor-Precategory (opposite-Precategory C) (Set-Precategory l3))
  where

  proj-functor-precategory-of-elements-presheaf-Precategory :
    functor-Precategory (precategory-of-elements-presheaf-Precategory C F) C
  pr1 proj-functor-precategory-of-elements-presheaf-Precategory X =
    pr1 X
  pr1 (pr2 proj-functor-precategory-of-elements-presheaf-Precategory) f =
    pr1 f
  pr1
    ( pr2
      ( pr2 proj-functor-precategory-of-elements-presheaf-Precategory)) g f =
    refl
  pr2
    ( pr2
      ( pr2 proj-functor-precategory-of-elements-presheaf-Precategory)) x =
    refl

Recent changes