open import Cat.Functor.Properties
open import Cat.Morphism.StrongEpi
open import Cat.Morphism.Duality
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

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


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βpreserves-mono : π.is-monic a β π.is-monic (Fβ a)
ff+esoβpreserves-mono {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βpreserves-epi : π.is-epic a β π.is-epic (Fβ a) ff+esoβpreserves-epi {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βpreserves-monos : π.is-monic a β π.is-monic (Fβ a) right-adjointβpreserves-monos {a = a} a-monic f g p = Equiv.injective (_ , R-adjunct-is-equiv 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βpreserves-epis : π.is-epic a β π.is-epic (Fβ a) left-adjointβpreserves-epis {a = a} a-epic f g p = Equiv.injective (_ , L-adjunct-is-equiv Fβ£R)$
a-epic _ _ \$
π.pullr (unit.is-natural _ _ _)
β R.extendl p
β π.pushr (sym (unit.is-natural _ _ _))