module Cat.Functor.Properties 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} â is-surjective (F .Fâ {x = x} {y})
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})
module _ {C : Precategory o h} {D : Precategory oâ hâ} where private module _ where module C = Cat.Reasoning C module D = Cat.Reasoning D open Cat.Reasoning using (_â _ ; Inverses) open _â _ public open Inverses public faithfulâiso-fibre-prop : â (F : Functor C D) â is-faithful F â â {x y} â (f : F # x D.â F # y) â is-prop (ÎŁ[ g â x C.â y ] (F-map-iso F g ⥠f)) faithfulâiso-fibre-prop F faithful f (g , p) (g' , q) = ÎŁ-prop-path! $ ext (faithful (ap D.to (p â sym q))) is-faithful-â : â {F : Functor C D} {G : Functor B C} â is-faithful F â is-faithful G â is-faithful (F Fâ G) is-faithful-â Ff Gf p = Gf (Ff p)
Fully faithful 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}) ffâfaithful : {F : Functor C D} â is-fully-faithful F â is-faithful F ffâfaithful f = Equiv.injective (_ , f) ffâfull : {F : Functor C D} â is-fully-faithful F â is-full F ffâfull {F = F} ff g = inc (equivâinverse ff g , equivâcounit ff g) 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 .F-id)) â©âĄ 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 .F-id)) â©âĄ 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 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 {C = C} {D = D} F y = ÎŁ[ x â C ] (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 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 â„
module _ {C : Precategory o h} {D : Precategory oâ hâ} where import Cat.Reasoning C as C import Cat.Reasoning D as D private module _ where open import Cat.Reasoning using (_â _ ; Inverses) open _â _ public open Inverses public is-ffâF-map-iso-is-equiv : {F : Functor C D} â is-fully-faithful F â â {X Y} â is-equiv (F-map-iso F {x = X} {Y}) is-ffâF-map-iso-is-equiv {F = F} ff = is-isoâis-equiv isom where isom : is-iso _ isom .is-iso.inv = is-ffâessentially-injective {F = F} ff isom .is-iso.rinv x = ext (equivâcounit ff _) isom .is-iso.linv x = ext (equivâunit ff _)
If a functor is essentially surjective, then the precomposition functor is faithful for every precategory
is-esoâprecompose-is-faithful : â {oa âa} {A : Precategory oa âa} â (F : Functor C D) â is-eso F â is-faithful (precompose F {D = A})
This is rather abstract, so letâs unfold the statement a bit. If precomposition by is fully faithful, then we can determine equality of natural transformations between functors by only looking at the components of the form for every
Intuitively, this should be true for essentially surjective functors, as doesnât miss out on any objects of but the actual proof involves some rather tedious calculations.
is-esoâprecompose-is-faithful {A = A} F F-eso {G} {H} {α} {ÎČ} αL=ÎČL = ext λ d â â„-â„-out! do (c , Fcâ d) â F-eso d let module Fcâ d = D._â _ Fcâ d pure $ α.η d âĄâš A.intror (G.annihilate (D.invl Fcâ d)) â©âĄ α.η d A.â G.â Fcâ d.to A.â G.â Fcâ d.from âĄâš A.extendl (α.is-natural _ _ _) â©âĄ H.â Fcâ d.to A.â â α.η (F.â c) â A.â G.â Fcâ d.from âĄâš ap! (unext αL=ÎČL c) â©âĄ H.â Fcâ d.to A.â ÎČ.η (F.â c) A.â G.â Fcâ d.from âĄâš A.extendl (sym (ÎČ.is-natural _ _ _)) â©âĄ ÎČ.η d A.â G.â Fcâ d.to A.â G.â Fcâ d.from âĄâš A.elimr (G.annihilate (D.invl Fcâ d)) â©âĄ ÎČ.η d â where module A = Cat.Reasoning A module F = Cat.Functor.Reasoning F module G = Cat.Functor.Reasoning G module H = Cat.Functor.Reasoning H module α = _=>_ α module ÎČ = _=>_ ÎČ
Another way of viewing this result is that it is a higher-dimensional
analog of the fact that precomposition with an epi is an embedding
.
Additionally, precomposition with an essentially surjective functor is conservative.
esoâprecompose-conservative : â {oa âa} {A : Precategory oa âa} â (F : Functor C D) â is-eso F â {G H : Functor D A} {α : G => H} â is-invertibleâż (α â F) â is-invertible⿠α
The proof follows the same plan as the previous theorem: natural transformations are invertible when they are invertible objectwise, and covers every object of
esoâprecompose-conservative {A = A} F F-eso {G} {H} {α} αâ»Âč = invertibleâinvertible⿠α λ d â â„-â„-out! do (c , Fcâ d) â F-eso d let module Fcâ d = D._â _ Fcâ d pure $ A.make-invertible (G.â Fcâ d.to A.â αâ»Âč.η c A.â H.â Fcâ d.from) (α.pulll (A.cancell (αâ»Âč.invl #â c)) â H.annihilate Fcâ d.invl) (A.pullr (α.cancelr (αâ»Âč.invr #â c)) â G.annihilate Fcâ d.invl) where module A = Cat.Reasoning A module F = Cat.Functor.Reasoning F module G = Cat.Functor.Reasoning G module H = Cat.Functor.Reasoning H module α = Cat.Natural.Reasoning α module αâ»Âč where open is-invertible⿠αâ»Âč public open Cat.Natural.Reasoning inv hiding (op) public
Pseudomonic functorsđ
A functor is pseudomonic if it is faithful and full on isomorphisms. Pseudomonic functors are arguably the correct notion of subcategory, as they ensure that we are not able to distinguish between isomorphic objects when creating a subcategory.
module _ {C : Precategory o h} {D : Precategory oâ hâ} where import Cat.Reasoning C as C import Cat.Reasoning D as D
is-full-on-isos : Functor C D â Type (o â h â hâ) is-full-on-isos F = â {x y} â (f : F .Fâ x D.â F .Fâ y) â â[ g â x C.â y ] (F-map-iso F g ⥠f) record is-pseudomonic (F : Functor C D) : Type (o â h â hâ) where no-eta-equality field faithful : is-faithful F isos-full : is-full-on-isos F open is-pseudomonic
Somewhat surprisingly, pseudomonic functors are conservative. As is full on isos, there merely exists some iso in the fibre of However, invertibility is a property of morphisms, so we can untruncate the mere existence. Once we have our hands on the isomorphism, we perform a simple calculation to note that it yields an inverse to
pseudomonicâconservative : â {F : Functor C D} â is-pseudomonic F â â {x y} (f : C.Hom x y) â D.is-invertible (F .Fâ f) â C.is-invertible f pseudomonicâconservative {F = F} pseudo {x} {y} f inv = â„-â„-rec C.is-invertible-is-prop (λ (g , p) â C.make-invertible (C.from g) (sym (ap (C._â _) (pseudo .faithful (ap D.to p))) â C.invl g) (sym (ap (_ C.â_) (pseudo .faithful (ap D.to p))) â C.invr g)) (pseudo .isos-full (D.invertibleâiso _ inv))
In a similar vein, pseudomonic functors are essentially injective. The proof follows a similar path to the prior one, hinging on the fact that faithful functors are an embedding on isos.
pseudomonicâessentially-injective : â {F : Functor C D} â is-pseudomonic F â â {x y} â F .Fâ x D.â F .Fâ y â x C.â y pseudomonicâessentially-injective {F = F} pseudo f = â„-â„-rec (faithfulâiso-fibre-prop F (pseudo .faithful) f) (λ x â x) (pseudo .isos-full f) .fst
Fully faithful functors are pseudomonic, as they are faithful and essentially injective.
ffâpseudomonic : â {F : Functor C D} â is-fully-faithful F â is-pseudomonic F ffâpseudomonic {F} ff .faithful = ffâfaithful {F = F} ff ffâpseudomonic {F} ff .isos-full f = inc (is-ffâessentially-injective {F = F} ff f , ext (equivâcounit ff (D.to f)))
Equivalence on objects functorsđ
A functor is an equivalence on objects if its action on objects is an equivalence.
is-equiv-on-objects : (F : Functor C D) â Type _ is-equiv-on-objects F = is-equiv (F .Fâ)
If is an equivalence-on-objects functor, then it is (split) essentially surjective.
equiv-on-objectsâsplit-eso : â (F : Functor C D) â is-equiv-on-objects F â is-split-eso F equiv-on-objectsâsplit-eso {D = D} F eqv y = equivâinverse eqv y , pathâiso (equivâcounit eqv y) equiv-on-objectsâeso : â (F : Functor C D) â is-equiv-on-objects F â is-eso F equiv-on-objectsâeso F eqv y = inc (equiv-on-objectsâsplit-eso F eqv y)