Essentially surjective functors between precategories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-11-01.
Last modified on 2024-04-11.

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


Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25(5):1010–1039, 06 2015. arXiv:1303.0584, doi:10.1017/S0960129514000486.

Recent changes