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 is fully faithful, then we can “unwhisker” any natural transformation to a natural transformation whose whiskering with on the left is This implies that the postcomposition functor 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 whose apex is isomorphic to for some object we can lift it to a Limit of (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)
ff→reflects-Terminal
  : (term : Terminal D)
  → ∀ {o} → term .Terminal.top D.≅ F.₀ o
  → Terminal C
ff→reflects-Terminal term is =
  Limit→Terminal C (ff→reflects-Limit _ (Terminal→Limit D term) is)

ff→reflects-Initial
  : (init : Initial D)
  → ∀ {o} → init .Initial.bot D.≅ F.₀ o
  → Initial C
ff→reflects-Initial init is =
  Colimit→Initial C (ff→reflects-Colimit _ (Initial→Colimit D init) is)

ff→reflects-Product
  : ∀ {a b} → (prod : Product D (F.₀ a) (F.₀ b))
  → ∀ {o} → prod .Product.apex D.≅ F.₀ o
  → Product C a b
ff→reflects-Product prod is =
  Limit→Product C (ff→reflects-Limit _ (Product→Limit D prod) is)

ff→reflects-Coproduct
  : ∀ {a b} → (coprod : Coproduct D (F.₀ a) (F.₀ b))
  → ∀ {o} → coprod .Coproduct.coapex D.≅ F.₀ o
  → Coproduct C a b
ff→reflects-Coproduct coprod is =
  Colimit→Coproduct C (ff→reflects-Colimit _ (Coproduct→Colimit D coprod) is)

ff→reflects-Equaliser
  : ∀ {a b} {f g : C.Hom a b} (eq : Equaliser D (F.₁ f) (F.₁ g))
  → ∀ {o} → eq .Equaliser.apex D.≅ F.₀ o
  → Equaliser C f g
ff→reflects-Equaliser eq is =
  Limit→Equaliser C (ff→reflects-Limit _ (Equaliser→Limit D eq) is)

ff→reflects-Coequaliser
  : ∀ {a b} {f g : C.Hom a b} (coeq : Coequaliser D (F.₁ f) (F.₁ g))
  → ∀ {o} → coeq .Coequaliser.coapex D.≅ F.₀ o
  → Coequaliser C f g
ff→reflects-Coequaliser coeq is =
  Colimit→Coequaliser C (ff→reflects-Colimit _ (Coequaliser→Colimit D coeq) is)