Conservative functors between precategories

Content created by Fredrik Bakke.

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

module category-theory.conservative-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.iterated-dependent-product-types
open import foundation.propositions
open import foundation.universe-levels


A functor F : C → D between precategories is conservative if every morphism that is mapped to an isomorphism in D is an isomorphism in C.


The predicate on functors of being conservative

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

  is-conservative-functor-Precategory : UU (l1  l2  l4)
  is-conservative-functor-Precategory =
    {x y : obj-Precategory C} (f : hom-Precategory C x y) 
    is-iso-Precategory D (hom-functor-Precategory C D F f) 
    is-iso-Precategory C f

  is-prop-is-conservative-functor-Precategory :
    is-prop is-conservative-functor-Precategory
  is-prop-is-conservative-functor-Precategory =
    is-prop-iterated-implicit-Π 2
      ( λ x y  is-prop-iterated-Π 2  f _  is-prop-is-iso-Precategory C f))

  is-conservative-prop-functor-Precategory : Prop (l1  l2  l4)
  pr1 is-conservative-prop-functor-Precategory =
  pr2 is-conservative-prop-functor-Precategory =

The type of conservative functors

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

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

  functor-conservative-functor-Precategory :
    functor-Precategory C D
  functor-conservative-functor-Precategory = pr1 F

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

  obj-conservative-functor-Precategory :
    obj-Precategory C  obj-Precategory D
  obj-conservative-functor-Precategory =
    obj-functor-Precategory C D
      ( functor-conservative-functor-Precategory)

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

See also

Recent changes