open import Cat.Prelude

module Cat.Functor.Base where

FunctorsπŸ”—

This module defines the most important clases of functors: Full, faithful, fully faithful (abbreviated ff), split essentially surjective and (β€œmerely”) essentially surjective.

A functor is full when its action on hom-sets is surjective:

is-full : Functor C D β†’ Type _
is-full {C = C} {D = D} F =
  βˆ€ {x y} (g : D .Hom (Fβ‚€ F x) (Fβ‚€ F y)) β†’ βˆƒ[ f ∈ C .Hom x y ] (F₁ F f ≑ g)

A functor is faithful when its action on hom-sets is injective:

is-faithful : Functor C D β†’ Type _
is-faithful F = βˆ€ {x y} β†’ injective (F₁ F {x = x} {y})

ff FunctorsπŸ”—

A functor is fully faithful (abbreviated ff) when its action on hom-sets is an equivalence. Since Hom-sets are sets, it suffices for the functor to be full and faithful; Rather than taking this conjunction as a definition, we use the more directly useful data as a definition and prove the conjunction as a theorem.

is-fully-faithful : Functor C D β†’ Type _
is-fully-faithful F = βˆ€ {x y} β†’ is-equiv (F₁ F {x = x} {y})

fully-faithful→faithful : {F : Functor C D} → is-fully-faithful F → is-faithful F
fully-faithful→faithful {F = F} ff {_} {_} {x} {y} p =
  x                         β‰‘βŸ¨ sym (equivβ†’unit ff x) βŸ©β‰‘
  equivβ†’inverse ff (F₁ F x) β‰‘βŸ¨ ap (equivβ†’inverse ff) p βŸ©β‰‘
  equivβ†’inverse ff (F₁ F y) β‰‘βŸ¨ equivβ†’unit ff y βŸ©β‰‘
  y                         ∎

full+faithful→ff
  : (F : Functor C D) β†’ is-full F β†’ is-faithful F β†’ is-fully-faithful F
full+faithful→ff {C = C} {D = D} F surj inj .is-eqv = p where
  img-is-prop : βˆ€ {x y} f β†’ is-prop (fibre (F₁ F {x = x} {y}) f)
  img-is-prop f (g , p) (h , q) = Ξ£-prop-path (Ξ» _ β†’ D .Hom-set _ _ _ _) (inj (p βˆ™ sym q))

  p : βˆ€ {x y} f β†’ is-contr (fibre (F₁ F {x = x} {y}) f)
  p f .centre = βˆ₯-βˆ₯-elim (Ξ» _ β†’ img-is-prop f) (Ξ» x β†’ x) (surj f)
  p f .paths = img-is-prop f _

A very important property of fully faithful functors (like FF) is that they are conservative: If the image of f:x→yf : x \to y under FF is an isomorphism Fx≅FyFx \cong Fy, then ff was really an isomorphism f:x≅yf : x \cong y.

module _ {C : Precategory o h} {D : Precategory o₁ h₁} where
  private
    module C = Precategory C
    module D = Precategory D

  import Cat.Morphism C as Cm
  import Cat.Morphism D as Dm

  is-ff→is-conservative
    : {F : Functor C D} β†’ is-fully-faithful F
    β†’ βˆ€ {X Y} (f : C.Hom X Y)  β†’ Dm.is-invertible (F₁ F f)
    β†’ Cm.is-invertible f
  is-ff→is-conservative {F = F} ff f isinv = i where
    open Cm.is-invertible
    open Cm.Inverses

Since the functor is ff, we can find a map β€œF1βˆ’1(f):yβ†’xF_1^{-1}(f) : y \to x” in the domain category to serve as an inverse for ff:

    g : C.Hom _ _
    g = equiv→inverse ff (isinv .Dm.is-invertible.inv)
    module ff {a} {b} = Equiv (_ , ff {a} {b})

    Ffog =
      F₁ F (f C.∘ g)    β‰‘βŸ¨ F-∘ F _ _ βŸ©β‰‘
      F₁ F f D.∘ F₁ F g β‰‘βŸ¨ apβ‚‚ D._∘_ refl (ff.Ξ΅ _) βˆ™ isinv .Dm.is-invertible.invl βŸ©β‰‘
      D.id              ∎

    Fgof =
      F₁ F (g C.∘ f)    β‰‘βŸ¨ F-∘ F _ _ βŸ©β‰‘
      F₁ F g D.∘ F₁ F f β‰‘βŸ¨ apβ‚‚ D._∘_ (ff.Ξ΅ _) refl βˆ™ isinv .Dm.is-invertible.invr βŸ©β‰‘
      D.id              ∎

    i : Cm.is-invertible _
    i .inv = g
    i .inverses .invl =
      f C.∘ g                    β‰‘βŸ¨ sym (ff.Ξ· _) βŸ©β‰‘
      ff.from ⌜ F₁ F (f C.∘ g) ⌝ β‰‘βŸ¨ ap! (Ffog βˆ™ sym (F-id F)) βŸ©β‰‘
      ff.from (F₁ F C.id)        β‰‘βŸ¨ ff.Ξ· _ βŸ©β‰‘
      C.id                       ∎
    i .inverses .invr =
      g C.∘ f                    β‰‘βŸ¨ sym (ff.Ξ· _) βŸ©β‰‘
      ff.from ⌜ F₁ F (g C.∘ f) ⌝ β‰‘βŸ¨ ap! (Fgof βˆ™ sym (F-id F)) βŸ©β‰‘
      ff.from (F₁ F C.id)        β‰‘βŸ¨ ff.Ξ· _ βŸ©β‰‘
      C.id                       ∎

  is-ff→essentially-injective
    : {F : Functor C D} β†’ is-fully-faithful F
    β†’ βˆ€ {X Y} β†’ Fβ‚€ F X Dm.β‰… Fβ‚€ F Y
    β†’ X Cm.β‰… Y
  is-ff→essentially-injective {F = F} ff
    record { to = to ; from = from ; inverses = inverses } =
    Cm.make-iso (equiv→inverse ff to) inv invl invr
    where
      D-inv : Dm.is-invertible to
      D-inv = record { inv = from ; inverses = inverses }
      open Cm.is-invertible
        (is-ff→is-conservative {F = F} ff
          (equiv→inverse ff to)
          (subst Dm.is-invertible (sym (equiv→counit ff _)) D-inv))

Essential FibresπŸ”—

The essential fibre of a functor F:C→DF : C \to D over an object y:Dy : D is the space of objects of CC which FF takes, up to isomorphism, to yy.

Essential-fibre : Functor C D β†’ D .Ob β†’ Type _
Essential-fibre {D = D} F y = Ξ£[ x ∈ _ ] (Fβ‚€ F x β‰… y)
  where open import Cat.Morphism D

A functor is split essentially surjective (abbreviated split eso) if there is a procedure for finding points in the essential fibre over any object. It’s essentially surjective if the this procedure merely, i.e.Β truncatedly, finds a point:

is-split-eso : Functor C D β†’ Type _
is-split-eso F = βˆ€ y β†’ Essential-fibre F y

is-eso : Functor C D β†’ Type _
is-eso F = βˆ€ y β†’ βˆ₯ Essential-fibre F y βˆ₯