Faithful functors between precategories

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-26.
Last modified on 2024-01-27.

module category-theory.faithful-functors-precategories where
Imports 
open import category-theory.faithful-maps-precategories
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.embeddings
open import foundation.equivalences
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

Idea

A functor between precategories C and D is faithful if it's an embedding on hom-sets.

Note that embeddings on sets happen to coincide with injections. However, we define faithful functors in terms of embeddings because this is the notion that generalizes.

Definition

The predicate on functors between precategories of being faithful

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

  is-faithful-functor-Precategory : UU (l1 ⊔ l2 ⊔ l4)
  is-faithful-functor-Precategory =
    is-faithful-map-Precategory C D (map-functor-Precategory C D F)

  is-prop-is-faithful-functor-Precategory :
    is-prop is-faithful-functor-Precategory
  is-prop-is-faithful-functor-Precategory =
    is-prop-is-faithful-map-Precategory C D (map-functor-Precategory C D F)

  is-faithful-prop-functor-Precategory : Prop (l1 ⊔ l2 ⊔ l4)
  is-faithful-prop-functor-Precategory =
    is-faithful-prop-map-Precategory C D (map-functor-Precategory C D F)

The type of faithful functors between two precategories

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

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

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

  is-faithful-faithful-functor-Precategory :
    is-faithful-functor-Precategory C D functor-faithful-functor-Precategory
  is-faithful-faithful-functor-Precategory = pr2 F

  obj-faithful-functor-Precategory : obj-Precategory C → obj-Precategory D
  obj-faithful-functor-Precategory =
    obj-functor-Precategory C D functor-faithful-functor-Precategory

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

The predicate on functors between precategories of being injective on hom-sets

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

  is-injective-hom-functor-Precategory : UU (l1 ⊔ l2 ⊔ l4)
  is-injective-hom-functor-Precategory =
    is-injective-hom-map-Precategory C D (map-functor-Precategory C D F)

  is-prop-is-injective-hom-functor-Precategory :
    is-prop is-injective-hom-functor-Precategory
  is-prop-is-injective-hom-functor-Precategory =
    is-prop-is-injective-hom-map-Precategory C D
      ( map-functor-Precategory C D F)

  is-injective-hom-prop-functor-Precategory : Prop (l1 ⊔ l2 ⊔ l4)
  is-injective-hom-prop-functor-Precategory =
    is-injective-hom-prop-map-Precategory C D
      ( map-functor-Precategory C D F)

Properties

A functor of precategories is faithful if and only if it is injective on hom-sets

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

  is-injective-hom-is-faithful-functor-Precategory :
    is-faithful-functor-Precategory C D F →
    is-injective-hom-functor-Precategory C D F
  is-injective-hom-is-faithful-functor-Precategory =
    is-injective-hom-is-faithful-map-Precategory C D
      ( map-functor-Precategory C D F)

  is-faithful-is-injective-hom-functor-Precategory :
    is-injective-hom-functor-Precategory C D F →
    is-faithful-functor-Precategory C D F
  is-faithful-is-injective-hom-functor-Precategory =
    is-faithful-is-injective-hom-map-Precategory C D
      ( map-functor-Precategory C D F)

  is-equiv-is-injective-hom-is-faithful-functor-Precategory :
    is-equiv is-injective-hom-is-faithful-functor-Precategory
  is-equiv-is-injective-hom-is-faithful-functor-Precategory =
    is-equiv-is-injective-hom-is-faithful-map-Precategory C D
      ( map-functor-Precategory C D F)

  is-equiv-is-faithful-is-injective-hom-functor-Precategory :
    is-equiv is-faithful-is-injective-hom-functor-Precategory
  is-equiv-is-faithful-is-injective-hom-functor-Precategory =
    is-equiv-is-faithful-is-injective-hom-map-Precategory C D
      ( map-functor-Precategory C D F)

  equiv-is-injective-hom-is-faithful-functor-Precategory :
    is-faithful-functor-Precategory C D F ≃
    is-injective-hom-functor-Precategory C D F
  equiv-is-injective-hom-is-faithful-functor-Precategory =
    equiv-is-injective-hom-is-faithful-map-Precategory C D
      ( map-functor-Precategory C D F)

  equiv-is-faithful-is-injective-hom-functor-Precategory :
    is-injective-hom-functor-Precategory C D F ≃
    is-faithful-functor-Precategory C D F
  equiv-is-faithful-is-injective-hom-functor-Precategory =
    equiv-is-faithful-is-injective-hom-map-Precategory C D
      ( map-functor-Precategory C D F)

Faithful functors are faithful on isomorphisms

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

  is-faithful-on-isos-is-faithful-functor-Precategory :
    (x y : obj-Precategory C) →
    is-emb (preserves-iso-functor-Precategory C D F {x} {y})
  is-faithful-on-isos-is-faithful-functor-Precategory x y =
    is-emb-right-factor _ _
      ( is-emb-inclusion-subtype (is-iso-prop-Precategory D))
      ( is-emb-comp _ _
        ( is-faithful-F x y)
        ( is-emb-inclusion-subtype (is-iso-prop-Precategory C)))

Recent changes