Fully faithful maps between precategories

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-20.

module category-theory.fully-faithful-maps-precategories where
Imports
open import category-theory.faithful-maps-precategories
open import category-theory.full-maps-precategories
open import category-theory.maps-precategories
open import category-theory.precategories

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.surjective-maps
open import foundation.universe-levels

Idea

A map between precategories C and D is fully faithful if it's an equivalence on hom-sets, or equivalently, a full and faithful map on precategories.

Definition

The predicate on maps between precategories of being fully faithful

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

is-fully-faithful-map-Precategory : UU (l1  l2  l4)
is-fully-faithful-map-Precategory =
(x y : obj-Precategory C)  is-equiv (hom-map-Precategory C D F {x} {y})

is-prop-is-fully-faithful-map-Precategory :
is-prop is-fully-faithful-map-Precategory
is-prop-is-fully-faithful-map-Precategory =
is-prop-iterated-Π 2
( λ x y  is-property-is-equiv (hom-map-Precategory C D F {x} {y}))

is-fully-faithful-prop-map-Precategory : Prop (l1  l2  l4)
pr1 is-fully-faithful-prop-map-Precategory = is-fully-faithful-map-Precategory
pr2 is-fully-faithful-prop-map-Precategory =
is-prop-is-fully-faithful-map-Precategory

equiv-hom-is-fully-faithful-map-Precategory :
is-fully-faithful-map-Precategory  {x y : obj-Precategory C}
hom-Precategory C x y
hom-Precategory D
( obj-map-Precategory C D F x)
( obj-map-Precategory C D F y)
pr1 (equiv-hom-is-fully-faithful-map-Precategory is-ff-F) =
hom-map-Precategory C D F
pr2 (equiv-hom-is-fully-faithful-map-Precategory is-ff-F {x} {y}) =
is-ff-F x y

inv-equiv-hom-is-fully-faithful-map-Precategory :
is-fully-faithful-map-Precategory  {x y : obj-Precategory C}
hom-Precategory D
( obj-map-Precategory C D F x)
( obj-map-Precategory C D F y)
hom-Precategory C x y
inv-equiv-hom-is-fully-faithful-map-Precategory is-ff-F =
inv-equiv (equiv-hom-is-fully-faithful-map-Precategory is-ff-F)

map-inv-hom-is-fully-faithful-map-Precategory :
is-fully-faithful-map-Precategory  {x y : obj-Precategory C}
hom-Precategory D
( obj-map-Precategory C D F x)
( obj-map-Precategory C D F y)
hom-Precategory C x y
map-inv-hom-is-fully-faithful-map-Precategory is-ff-F =
map-equiv (inv-equiv-hom-is-fully-faithful-map-Precategory is-ff-F)

The type of fully faithful maps between two precategories

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

fully-faithful-map-Precategory : UU (l1  l2  l3  l4)
fully-faithful-map-Precategory =
Σ (map-Precategory C D) (is-fully-faithful-map-Precategory C D)

map-fully-faithful-map-Precategory :
fully-faithful-map-Precategory  map-Precategory C D
map-fully-faithful-map-Precategory = pr1

is-fully-faithful-fully-faithful-map-Precategory :
(F : fully-faithful-map-Precategory)
is-fully-faithful-map-Precategory C D (map-fully-faithful-map-Precategory F)
is-fully-faithful-fully-faithful-map-Precategory = pr2

obj-fully-faithful-map-Precategory :
fully-faithful-map-Precategory  obj-Precategory C  obj-Precategory D
obj-fully-faithful-map-Precategory =
obj-map-Precategory C D  map-fully-faithful-map-Precategory

hom-fully-faithful-map-Precategory :
(F : fully-faithful-map-Precategory) {x y : obj-Precategory C}
hom-Precategory C x y
hom-Precategory D
( obj-fully-faithful-map-Precategory F x)
( obj-fully-faithful-map-Precategory F y)
hom-fully-faithful-map-Precategory =
hom-map-Precategory C D  map-fully-faithful-map-Precategory

equiv-hom-fully-faithful-map-Precategory :
(F : fully-faithful-map-Precategory) {x y : obj-Precategory C}
hom-Precategory C x y
hom-Precategory D
( obj-fully-faithful-map-Precategory F x)
( obj-fully-faithful-map-Precategory F y)
equiv-hom-fully-faithful-map-Precategory F =
equiv-hom-is-fully-faithful-map-Precategory C D
( map-fully-faithful-map-Precategory F)
( is-fully-faithful-fully-faithful-map-Precategory F)

inv-equiv-hom-fully-faithful-map-Precategory :
(F : fully-faithful-map-Precategory) {x y : obj-Precategory C}
hom-Precategory D
( obj-fully-faithful-map-Precategory F x)
( obj-fully-faithful-map-Precategory F y)
hom-Precategory C x y
inv-equiv-hom-fully-faithful-map-Precategory F =
inv-equiv (equiv-hom-fully-faithful-map-Precategory F)

map-inv-hom-fully-faithful-map-Precategory :
(F : fully-faithful-map-Precategory) {x y : obj-Precategory C}
hom-Precategory D
( obj-fully-faithful-map-Precategory F x)
( obj-fully-faithful-map-Precategory F y)
hom-Precategory C x y
map-inv-hom-fully-faithful-map-Precategory F =
map-equiv (inv-equiv-hom-fully-faithful-map-Precategory F)

Properties

Fully faithful maps are the same as full and faithful maps

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

is-full-is-fully-faithful-map-Precategory :
is-fully-faithful-map-Precategory C D F  is-full-map-Precategory C D F
is-full-is-fully-faithful-map-Precategory is-ff-F x y =
is-surjective-is-equiv (is-ff-F x y)

full-map-is-fully-faithful-map-Precategory :
is-fully-faithful-map-Precategory C D F  full-map-Precategory C D
pr1 (full-map-is-fully-faithful-map-Precategory is-ff-F) = F
pr2 (full-map-is-fully-faithful-map-Precategory is-ff-F) =
is-full-is-fully-faithful-map-Precategory is-ff-F

is-faithful-is-fully-faithful-map-Precategory :
is-fully-faithful-map-Precategory C D F  is-faithful-map-Precategory C D F
is-faithful-is-fully-faithful-map-Precategory is-ff-F x y =
is-emb-is-equiv (is-ff-F x y)

faithful-map-is-fully-faithful-map-Precategory :
is-fully-faithful-map-Precategory C D F  faithful-map-Precategory C D
pr1 (faithful-map-is-fully-faithful-map-Precategory is-ff-F) = F
pr2 (faithful-map-is-fully-faithful-map-Precategory is-ff-F) =
is-faithful-is-fully-faithful-map-Precategory is-ff-F

is-fully-faithful-is-full-is-faithful-map-Precategory :
is-full-map-Precategory C D F
is-faithful-map-Precategory C D F
is-fully-faithful-map-Precategory C D F
is-fully-faithful-is-full-is-faithful-map-Precategory
is-full-F is-faithful-F x y =
is-equiv-is-emb-is-surjective (is-full-F x y) (is-faithful-F x y)

fully-faithful-map-is-full-is-faithful-map-Precategory :
is-full-map-Precategory C D F
is-faithful-map-Precategory C D F
fully-faithful-map-Precategory C D
pr1
( fully-faithful-map-is-full-is-faithful-map-Precategory
is-full-F is-faithful-F) =
F
pr2
( fully-faithful-map-is-full-is-faithful-map-Precategory
is-full-F is-faithful-F) =
is-fully-faithful-is-full-is-faithful-map-Precategory
( is-full-F) (is-faithful-F)

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

full-map-fully-faithful-map-Precategory : full-map-Precategory C D
full-map-fully-faithful-map-Precategory =
full-map-is-fully-faithful-map-Precategory C D
( map-fully-faithful-map-Precategory C D F)
( is-fully-faithful-fully-faithful-map-Precategory C D F)

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