module Cat.Functor.Properties.FullyFaithful
  {oc od ℓc ℓd} {C : Precategory oc ℓc} {D : Precategory od ℓd}
  (F : Functor C D) (ff : is-fully-faithful F)
  where

Properties of fully faithful functors🔗

This module collects various properties of fully faithful functors.

Interaction with composition functors🔗

If $F$ is fully faithful, then we can “unwhisker” any natural transformation $θ : F \circ G \Rightarrow F \circ H$ to a natural transformation $F^{- 1} θ : G \Rightarrow H$ whose whiskering with $F$ on the left is $θ .$ This implies that the postcomposition functor $F \circ -$ is fully faithful.

module _ {oe ℓe} {E : Precategory oe ℓe} where
  unwhisker : ∀ {G H : Functor E C} → F F∘ G => F F∘ H → G => H
  unwhisker θ .η d = F.from (θ .η d)
  unwhisker θ .is-natural x y f = sym (F.ε-twist (sym (θ .is-natural x y f)))

  ff→postcompose-ff : is-fully-faithful (postcompose F {D = E})
  ff→postcompose-ff = is-iso→is-equiv $ iso unwhisker
    (λ _ → ext λ d → F.ε _) (λ _ → ext λ d → F.η _)

Fully faithful functors reflect (co)limits🔗

Fully faithful functors reflect both left and right Kan extensions, hence in particular limits and colimits. Thinking of such functors as full subcategory inclusions, this means that, if a (co)cone entirely contained within the subcategory is universal in the whole category, then it is also universal in the subcategory. The converse is not true: fully faithful functors do not preserve Kan extensions in general.

  ff→reflects-lan
    : ∀ {p : Functor J U} {G : Functor J C} {H : Functor U C} {eta : G => H F∘ p}
    → (lan : is-lan p (F F∘ G) (F F∘ H) (nat-assoc-to (F ▸ eta)))
    → reflects-lan F lan
  ff→reflects-lan lan .σ eta = unwhisker (lan .σ (nat-assoc-to (F ▸ eta)))
  ff→reflects-lan lan .σ-comm = ext λ j → F.whackl (lan .σ-comm ηₚ j)
  ff→reflects-lan lan .σ-uniq {σ' = σ'} com = ext λ u → sym $ F.adjunctl $ sym $
    lan .σ-uniq {σ' = F ▸ σ'} (ext λ j → F.expand (com ηₚ j)) ηₚ u

  ff→reflects-ran
    : ∀ {p : Functor J U} {G : Functor J C} {H : Functor U C} {eps : H F∘ p => G}
    → (ran : is-ran p (F F∘ G) (F F∘ H) (nat-assoc-from (F ▸ eps)))
    → reflects-ran F ran
  ff→reflects-ran ran .σ eps = unwhisker (ran .σ (nat-assoc-from (F ▸ eps)))
  ff→reflects-ran ran .σ-comm = ext λ j → F.whackr (ran .σ-comm ηₚ j)
  ff→reflects-ran ran .σ-uniq {σ' = σ'} com = ext λ u → sym $ F.adjunctl $ sym $
    ran .σ-uniq {σ' = F ▸ σ'} (ext λ j → F.expand (com ηₚ j)) ηₚ u

  ff→reflects-limit : reflects-limit F G
  ff→reflects-limit = ff→reflects-ran

  ff→reflects-colimit : reflects-colimit F G
  ff→reflects-colimit = ff→reflects-lan

We prove the following convenience lemma: given a Limit of $F \circ G$ whose apex is isomorphic to $F (o)$ for some object $o : C,$ we can lift it to a Limit of $G$ (and similarly for Colimits).

  ff→reflects-Limit
    : (Lim : Limit (F F∘ G))
    → ∀ {o} → apex Lim D.≅ F.₀ o
    → Limit G
  ff→reflects-Limit Lim {o} is = to-limit (ff→reflects-limit lim) where
    eps' : F F∘ !Const o F∘ !F => F F∘ G
    eps' = nat-unassoc-from
      (Lim .eps ∘nt (!constⁿ (is .D.from) ◂ !F))

    lim : is-ran !F (F F∘ G) (F F∘ !Const o) (nat-assoc-from (F ▸ unwhisker eps'))
    lim = natural-isos→is-ran idni idni
      (!const-isoⁿ is)
      (ext λ j → D.idl _ ·· (D.refl⟩∘⟨ D.eliml (Lim .Ext .F-id)) ·· sym (F.ε _))
      (Lim .has-ran)

  ff→reflects-Colimit
    : (Colim : Colimit (F F∘ G))
    → ∀ {o} → coapex Colim D.≅ F.₀ o
    → Colimit G
  ff→reflects-Colimit Colim {o} is = to-colimit (ff→reflects-colimit colim) where
    eta' : F F∘ G => F F∘ !Const o F∘ !F
    eta' = nat-unassoc-to
      ((!constⁿ (is .D.to) ◂ !F) ∘nt Colim .eta)

    colim : is-lan !F (F F∘ G) (F F∘ !Const o) (nat-assoc-to (F ▸ unwhisker eta'))
    colim = natural-isos→is-lan idni idni
      (!const-isoⁿ is)
      (ext λ j → (F.eliml refl D.⟩∘⟨ D.idr _) ∙ sym (F.ε _))
      (Colim .has-lan)