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 ) is that they are conservative: If the image of under is an isomorphism , then was really an isomorphism .
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 ββ in the domain category to serve as an inverse for :
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 over an object is the space of objects of which takes, up to isomorphism, to .
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 β₯