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.
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
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)