Essentially surjective functors between precategories

Content created by Fredrik Bakke.

Created on 2023-11-01.
Last modified on 2023-11-09.

module category-theory.essentially-surjective-functors-precategories where
open import category-theory.functors-precategories
open import category-theory.isomorphisms-in-precategories
open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.propositions
open import foundation.universe-levels


A functor F : C → D between precategories is essentially surjective if there for every object y : D merely exists an object x : C such that F x ≅ y.


The predicate of being essentially surjective

module _
  {l1 l2 l3 l4 : Level}
  (C : Precategory l1 l2) (D : Precategory l3 l4)
  (F : functor-Precategory C D)

  is-essentially-surjective-prop-functor-Precategory : Prop (l1  l3  l4)
  is-essentially-surjective-prop-functor-Precategory =
      ( obj-Precategory D)
      ( λ y 
          ( obj-Precategory C)
          ( λ x  iso-Precategory D (obj-functor-Precategory C D F x) y))

  is-essentially-surjective-functor-Precategory : UU (l1  l3  l4)
  is-essentially-surjective-functor-Precategory =
    ( y : obj-Precategory D) 
     ( obj-Precategory C)
      ( λ x  iso-Precategory D (obj-functor-Precategory C D F x) y)

  is-prop-is-essentially-surjective-functor-Precategory :
    is-prop is-essentially-surjective-functor-Precategory
  is-prop-is-essentially-surjective-functor-Precategory =
    is-prop-type-Prop is-essentially-surjective-prop-functor-Precategory

The type of essentially surjective functors

essentially-surjective-functor-Precategory :
  {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) 
  UU (l1  l2  l3  l4)
essentially-surjective-functor-Precategory C D =
  Σ ( functor-Precategory C D)
    ( is-essentially-surjective-functor-Precategory C D)

module _
  {l1 l2 l3 l4 : Level}
  (C : Precategory l1 l2) (D : Precategory l3 l4)
  (F : essentially-surjective-functor-Precategory C D)

  functor-essentially-surjective-functor-Precategory :
    functor-Precategory C D
  functor-essentially-surjective-functor-Precategory = pr1 F

  is-essentially-surjective-essentially-surjective-functor-Precategory :
    is-essentially-surjective-functor-Precategory C D
      ( functor-essentially-surjective-functor-Precategory)
  is-essentially-surjective-essentially-surjective-functor-Precategory = pr2 F

  obj-essentially-surjective-functor-Precategory :
    obj-Precategory C  obj-Precategory D
  obj-essentially-surjective-functor-Precategory =
    obj-functor-Precategory C D
      ( functor-essentially-surjective-functor-Precategory)

  hom-essentially-surjective-functor-Precategory :
    {x y : obj-Precategory C} 
    hom-Precategory C x y 
    hom-Precategory D
      ( obj-essentially-surjective-functor-Precategory x)
      ( obj-essentially-surjective-functor-Precategory y)
  hom-essentially-surjective-functor-Precategory =
    hom-functor-Precategory C D
      ( functor-essentially-surjective-functor-Precategory)


Precomposing by essentially surjective functors define fully faithful functors

This remains to be shown. This is Lemma 8.2 of Univalent Categories and the Rezk completion.

See also


  1. Benedikt Ahrens and Krzysztof Kapulkin and Michael Shulman, Univalent Categories and the Rezk completion (2015) (arXiv:1303.0584, DOI:10.1017/S0960129514000486)

Recent changes