module Cat.Functor.Morphism {o โ o' โ'} {๐ : Precategory o โ} {๐ : Precategory o' โ'} (F : Functor ๐ ๐) where
private module ๐ = Cat.Reasoning ๐ module ๐ = Cat.Reasoning ๐ open Cat.Functor.Reasoning F private variable A B C : ๐.Ob a b c d : ๐.Hom A B X Y Z : ๐.Ob f g h i : ๐.Hom X Y
Actions of functors on morphisms๐
This module describes how various classes of functors act on designated collections of morphisms.
First, some general definitions. Let be a collection of morphisms in A functor preserves if implies that
preserves-monos : Type _ preserves-monos = โ {a b : ๐.Ob} {f : ๐.Hom a b} โ ๐.is-monic f โ ๐.is-monic (Fโ f) preserves-epis : Type _ preserves-epis = โ {a b : ๐.Ob} {f : ๐.Hom a b} โ ๐.is-epic f โ ๐.is-epic (Fโ f)
preserves-strong-epis : Type _ preserves-strong-epis = โ {a b : ๐.Ob} {f : ๐.Hom a b} โ is-strong-epi ๐ f โ is-strong-epi ๐ (Fโ f)
Likewise, a functor reflects if implies that
reflects-monos : Type _ reflects-monos = โ {a b : ๐.Ob} {f : ๐.Hom a b} โ ๐.is-monic (Fโ f) โ ๐.is-monic f reflects-epis : Type _ reflects-epis = โ {a b : ๐.Ob} {f : ๐.Hom a b} โ ๐.is-epic (Fโ f) โ ๐.is-epic f
Functors that reflect invertible morphisms are called conservative, and are notable enough to deserve their own name and page!
Faithful functors๐
Faithful functors reflect monomorphisms and epimorphisms. We will only comment on the proof regarding monomorphisms, since the argument for epimorphisms is formally dual. Let be monic in and let be a pair of morphisms in such that Because preserves all commutative diagrams, is monic, so Finally, is faithful, so we can deduce
module _ (faithful : is-faithful F) where faithfulโreflects-mono : ๐.is-monic (Fโ a) โ ๐.is-monic a faithfulโreflects-mono {a = a} F[a]-monic b c p = faithful (F[a]-monic (Fโ b) (Fโ c) (weave p)) faithfulโreflects-epi : ๐.is-epic (Fโ a) โ ๐.is-epic a faithfulโreflects-epi {a = a} F[a]-epic b c p = faithful (F[a]-epic (Fโ b) (Fโ c) (weave p))
Likewise, faithful functors reflect all diagrams: this means that if and either form a section/retraction pair or an isomorphism, then it must have been the case that and already did.
faithfulโreflects-section-of : (Fโ a) ๐.section-of (Fโ b) โ a ๐.section-of b faithfulโreflects-section-of p = faithful (F-โ _ _ โ p โ sym F-id) faithfulโreflects-retract-of : (Fโ a) ๐.retract-of (Fโ b) โ a ๐.retract-of b faithfulโreflects-retract-of p = faithfulโreflects-section-of p faithfulโreflects-inverses : ๐.Inverses (Fโ a) (Fโ b) โ ๐.Inverses a b faithfulโreflects-inverses ab-inv .๐.Inverses.invl = faithfulโreflects-section-of (๐.Inverses.invl ab-inv) faithfulโreflects-inverses ab-inv .๐.Inverses.invr = faithfulโreflects-section-of (๐.Inverses.invr ab-inv)
Fully faithful, essentially surjective functors๐
If a functor is fully faithful and essentially surjective, then it preserves all mono- and epimorphisms. Keep in mind that, since we have not assumed that the categories involved are univalent, this condition is slightly weaker than being an equivalence of categories.
Let be a mono, and let be a pair of morphisms in satisfying that Since is eso, there merely exists a with Because is also full, there must merely exist a pair of morphisms satisfying and
module _ (ff : is-fully-faithful F) (eso : is-eso F) where ff+esoโis-monic : ๐.is-monic a โ ๐.is-monic (Fโ a) ff+esoโis-monic {a = a} a-monic {x} f g p = โฅ-โฅ-out! do (x* , i) โ eso x (f* , q) โ ffโfull {F = F} ff (f ๐.โ ๐.to i) (g* , r) โ ffโfull {F = F} ff (g ๐.โ ๐.to i)
Next, note that this follows from faithfulness of and our hypothesis that
let s = ffโfaithful {F = F} ff $ Fโ (a ๐.โ f*) โกโจ F-โ _ _ โ ๐.pushr q โฉโก (Fโ a ๐.โ f) ๐.โ ๐.to i โกโจ apโ ๐._โ_ p refl โฉโก (Fโ a ๐.โ g) ๐.โ ๐.to i โกโจ ๐.pullr (sym r) โ sym (F-โ _ _) โฉโก Fโ (a ๐.โ g*) โ
To wrap things up, recall that is monic, so and However, and by definition, so we can deduce that Finally, isomorphisms are epic, so we can cancel on the left, concluding that
pure $ ๐.isoโepic i f g $ f ๐.โ ๐.to i โกหโจ q โฉโกห Fโ f* โกโจ ap Fโ (a-monic f* g* s) โฉโก Fโ g* โกโจ r โฉโก g ๐.โ ๐.to i โ
As mentioned above, the same holds for epimorphisms. Since the proof is formally dual to the case above, we will not dwell on it.
ff+esoโis-epic : ๐.is-epic a โ ๐.is-epic (Fโ a) ff+esoโis-epic {a = a} a-epic {x} f g p = โฅ-โฅ-out! do (x* , i) โ eso x (f* , q) โ ffโfull {F = F} ff (๐.from i ๐.โ f) (g* , r) โ ffโfull {F = F} ff (๐.from i ๐.โ g) let s = F-โ _ _ โ ๐.pushl q โ apโ ๐._โ_ refl p โ ๐.pulll (sym r) โ sym (F-โ _ _) pure $ ๐.isoโmonic (i ๐.Isoโปยน) f g $ sym q โโ ap Fโ (a-epic f* g* (ffโfaithful {F = F} ff s)) โโ r
Left and right adjoints๐
If we are given an adjunction then the right adjoint preserves monomorphisms. Fix a mono and let satisfy We want to show and, by the adjunction, it will suffice to show that Since is a monomorphism, we can again reduce this to showing
which follows by a quick calculation.
module _ {L : Functor ๐ ๐} (LโฃF : L โฃ F) where private module L = Cat.Functor.Reasoning L open _โฃ_ LโฃF
right-adjointโis-monic : ๐.is-monic a โ ๐.is-monic (Fโ a) right-adjointโis-monic {a = a} a-monic f g p = R-adjunct.injective LโฃF $ a-monic _ _ $ a ๐.โ ฮต _ ๐.โ L.โ f โกโจ ๐.pulll (sym (counit.is-natural _ _ _)) โฉโก (ฮต _ ๐.โ L.โ (Fโ a)) ๐.โ L.โ f โกโจ L.extendr p โฉโก (ฮต _ ๐.โ L.โ (Fโ a)) ๐.โ L.โ g โกโจ ๐.pushl (counit.is-natural _ _ _) โฉโก a ๐.โ ฮต _ ๐.โ L.โ g โ
Dualizing this argument, we can show that left adjoints preserve epimorphisms.
module _ {R : Functor ๐ ๐} (FโฃR : F โฃ R) where private module R = Cat.Functor.Reasoning R open _โฃ_ FโฃR left-adjointโis-epic : ๐.is-epic a โ ๐.is-epic (Fโ a) left-adjointโis-epic {a = a} a-epic f g p = L-adjunct.injective FโฃR $ a-epic _ _ $ ๐.pullr (unit.is-natural _ _ _) โ R.extendl p โ ๐.pushr (sym (unit.is-natural _ _ _))