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
Imports
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

Idea

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.

Definitions

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)
  where

  is-essentially-surjective-prop-functor-Precategory : Prop (l1  l3  l4)
  is-essentially-surjective-prop-functor-Precategory =
    Π-Prop
      ( obj-Precategory D)
      ( λ y 
        ∃-Prop
          ( 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)
  where

  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)

Properties

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

References

  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