open import Cat.Prelude

module Cat.Functor.Base where


# Functorsđ

This module defines the most important clases of functors: Full, faithful, fully faithful (abbreviated ff), split essentially surjective and (âmerelyâ) essentially surjective.

A functor is full when its action on hom-sets is surjective:

is-full : Functor C D â Type _
is-full {C = C} {D = D} F =
â {x y} (g : D .Hom (Fâ F x) (Fâ F y)) â â[ f â C .Hom x y ] (Fâ F f âĄ g)


A functor is faithful when its action on hom-sets is injective:

is-faithful : Functor C D â Type _
is-faithful F = â {x y} â injective (Fâ F {x = x} {y})


## ff Functorsđ

A functor is fully faithful (abbreviated ff) when its action on hom-sets is an equivalence. Since Hom-sets are sets, it suffices for the functor to be full and faithful; Rather than taking this conjunction as a definition, we use the more directly useful data as a definition and prove the conjunction as a theorem.

is-fully-faithful : Functor C D â Type _
is-fully-faithful F = â {x y} â is-equiv (Fâ F {x = x} {y})

fully-faithfulâfaithful : {F : Functor C D} â is-fully-faithful F â is-faithful F
fully-faithfulâfaithful {F = F} ff {_} {_} {x} {y} p =
x                         âĄâš sym (equivâretraction ff x) â©âĄ
equivâinverse ff (Fâ F x) âĄâš ap (equivâinverse ff) p â©âĄ
equivâinverse ff (Fâ F y) âĄâš equivâretraction ff y â©âĄ
y                         â

full+faithfulâff
: (F : Functor C D) â is-full F â is-faithful F â is-fully-faithful F
full+faithfulâff {C = C} {D = D} F surj inj .is-eqv = p where
img-is-prop : â {x y} f â is-prop (fibre (Fâ F {x = x} {y}) f)
img-is-prop f (g , p) (h , q) = ÎŁ-prop-path (Î» _ â D .Hom-set _ _ _ _) (inj (p â sym q))

p : â {x y} f â is-contr (fibre (Fâ F {x = x} {y}) f)
p f .centre = â„-â„-elim (Î» _ â img-is-prop f) (Î» x â x) (surj f)
p f .paths = img-is-prop f _


A very important property of fully faithful functors (like $F$) is that they are conservative: If the image of $f : x \to y$ under $F$ is an isomorphism $Fx \cong Fy$, then $f$ was really an isomorphism $f : x \cong y$.

module _ {C : Precategory o h} {D : Precategory oâ hâ} where
private
module C = Precategory C
module D = Precategory D

import Cat.Morphism C as Cm
import Cat.Morphism D as Dm

is-ffâis-conservative
: {F : Functor C D} â is-fully-faithful F
â â {X Y} (f : C.Hom X Y)  â Dm.is-invertible (Fâ F f)
â Cm.is-invertible f
is-ffâis-conservative {F = F} ff f isinv = i where
open Cm.is-invertible
open Cm.Inverses


Since the functor is ff, we can find a map â$F_1^{-1}(f) : y \to x$â in the domain category to serve as an inverse for $f$:

    g : C.Hom _ _
g = equivâinverse ff (isinv .Dm.is-invertible.inv)

Ffog =
Fâ F (f C.â g)    âĄâš F-â F _ _ â©âĄ
Fâ F f D.â Fâ F g âĄâš apâ D._â_ refl (equivâsection ff _) â isinv .Dm.is-invertible.invl â©âĄ
D.id              â

Fgof =
Fâ F (g C.â f)    âĄâš F-â F _ _ â©âĄ
Fâ F g D.â Fâ F f âĄâš apâ D._â_ (equivâsection ff _) refl â isinv .Dm.is-invertible.invr â©âĄ
D.id              â

i : Cm.is-invertible _
i .inv = g
i .inverses .invl =
f C.â g                           âĄâš sym (equivâretraction ff _) â©âĄ
equivâinverse ff (Fâ F (f C.â g)) âĄâš ap (equivâinverse ff) (Ffog â sym (F-id F)) â©âĄ
equivâinverse ff (Fâ F C.id)      âĄâš equivâretraction ff _ â©âĄ
C.id                              â
i .inverses .invr =
g C.â f                           âĄâš sym (equivâretraction ff _) â©âĄ
equivâinverse ff (Fâ F (g C.â f)) âĄâš ap (equivâinverse ff) (Fgof â sym (F-id F)) â©âĄ
equivâinverse ff (Fâ F C.id)      âĄâš equivâretraction ff _ â©âĄ
C.id                              â

is-ffâessentially-injective
: {F : Functor C D} â is-fully-faithful F
â â {X Y} â Fâ F X Dm.â Fâ F Y
â X Cm.â Y
is-ffâessentially-injective {F = F} ff
record { to = to ; from = from ; inverses = inverses } =
Cm.make-iso (equivâinverse ff to) inv invl invr
where
D-inv : Dm.is-invertible to
D-inv = record { inv = from ; inverses = inverses }
open Cm.is-invertible
(is-ffâis-conservative {F = F} ff
(equivâinverse ff to)
(subst Dm.is-invertible (sym (equivâsection ff _)) D-inv))


## Essential Fibresđ

The essential fibre of a functor $F : C \to D$ over an object $y : D$ is the space of objects of $C$ which $F$ takes, up to isomorphism, to $y$.

Essential-fibre : Functor C D â D .Ob â Type _
Essential-fibre {D = D} F y = ÎŁ[ x â _ ] (Fâ F x â y)
where open import Cat.Morphism D


A functor is split essentially surjective (abbreviated split eso) if there is a procedure for finding points in the essential fibre over any object. Itâs essentially surjective if the this procedure merely, i.e.Â truncatedly, finds a point:

is-split-eso : Functor C D â Type _
is-split-eso F = â y â Essential-fibre F y

is-eso : Functor C D â Type _
is-eso F = â y â â„ Essential-fibre F y â„