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βunit ff x) β©β‘ equivβinverse ff (Fβ F x) β‘β¨ ap (equivβinverse ff) p β©β‘ equivβinverse ff (Fβ F y) β‘β¨ equivβunit 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) module ff {a} {b} = Equiv (_ , ff {a} {b}) Ffog = Fβ F (f C.β g) β‘β¨ F-β F _ _ β©β‘ Fβ F f D.β Fβ F g β‘β¨ apβ D._β_ refl (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._β_ (ff.Ξ΅ _) refl β isinv .Dm.is-invertible.invr β©β‘ D.id β i : Cm.is-invertible _ i .inv = g i .inverses .invl = f C.β g β‘β¨ sym (ff.Ξ· _) β©β‘ ff.from β Fβ F (f C.β g) β β‘β¨ ap! (Ffog β sym (F-id F)) β©β‘ ff.from (Fβ F C.id) β‘β¨ ff.Ξ· _ β©β‘ C.id β i .inverses .invr = g C.β f β‘β¨ sym (ff.Ξ· _) β©β‘ ff.from β Fβ F (g C.β f) β β‘β¨ ap! (Fgof β sym (F-id F)) β©β‘ ff.from (Fβ F C.id) β‘β¨ 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 im = imβ² where -- Cm.make-iso (equivβinverse ff to) inv invl invr open Dm._β _ im using (to ; from ; inverses) D-invβ² : Dm.is-invertible (Fβ F (equivβinverse ff to)) D-invβ² .Dm.is-invertible.inv = from D-invβ² .Dm.is-invertible.inverses = subst (Ξ» e β Dm.Inverses e from) (sym (equivβcounit ff _)) inverses open Cm.is-invertible (is-ffβis-conservative {F = F} ff (equivβinverse ff to) D-invβ²) imβ² : _ Cm.β _ imβ² .to = equivβinverse ff to imβ² .from = inv imβ² .inverses .Cm.Inverses.invl = invl imβ² .inverses .Cm.Inverses.invr = invr
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 β₯