open import Cat.Diagram.Colimit.Coequaliser
open import Cat.Diagram.Colimit.Coproduct
open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Colimit.Initial
open import Cat.Diagram.Limit.Equaliser
open import Cat.Diagram.Limit.Terminal
open import Cat.Diagram.Limit.Product
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Limit.Base
open import Cat.Functor.Kan.Unique
open import Cat.Functor.Naturality
open import Cat.Functor.Properties
open import Cat.Diagram.Coproduct
open import Cat.Diagram.Equaliser
open import Cat.Functor.Coherence
open import Cat.Diagram.Terminal
open import Cat.Functor.Kan.Base
open import Cat.Diagram.Initial
open import Cat.Diagram.Product
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning.FullyFaithful as FF
import Cat.Reasoning

open Functor
open _=>_

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

private
  module C = Cat.Reasoning C
  module D = Cat.Reasoning D
  module F = FF F ff

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.

module _ {oj ou hj hu} {J : Precategory oj hj} {U : Precategory ou hu} where
  open is-lan
  open is-ran

  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

_ = Limit
_ = Colimit
module _ {oj hj} {J : Precategory oj hj} (G : Functor J C) where
  open Limit
  open Colimit

  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)

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)