module Cat.Functor.Conservative where

Conservative functors🔗

We say a functor is conservative if it reflects isomorphisms. More concretely, if $f : A \to B$ is some morphism $C,$ and if $F (f)$ is an iso in $D,$ then $f$ must have already been an iso in $C!$

is-conservative : Functor C D → Type _
is-conservative {C = C} {D = D} F =
  ∀ {A B} {f : C .Hom A B}
  → is-invertible D (F .F₁ f) → is-invertible C f

As a general fact, conservative functors reflect limits and colimits that they preserve (given those (co)limits exist in the first place!).

The rough proof sketch is as follows: let $K$ be some cone in $C$ such that $F (K)$ is a limit in $D,$ and $L$ a limit in $C$ of the same diagram that is preserved by $F .$ By the universal property of $L,$ there exists a map $η$ from the apex of $K$ to the apex of $L$ in $C .$ Furthermore, as $F (K)$ is a limit in $D,$ $F (η)$ becomes an isomorphism in $D .$ The situation is summarised by the following diagram, which shows how $F$ maps cones in $C$ to cones in $D$ (the coloured cones are assumes to be limiting).

However, $F$ is conservative, which implies that $η$ was an isomorphism in $C$ all along! This means that $K$ must be a limit in $C$ as well (see is-invertible→is-limitp).

module _ {F : Functor C D} (conservative : is-conservative F) where
  private
    open _=>_
    module C = Cat C
    module D = Cat D
    module F = Func F

  conservative-reflects-limits
    : ∀ {Dia : Functor J C}
    → Limit Dia
    → preserves-limit F Dia
    → reflects-limit F Dia
  conservative-reflects-limits L-lim preservesa {K} {eps} FK-lim =
    is-invertible→is-limitp
      {K = Limit.Ext L-lim} {epsy = Limit.cone L-lim} (Limit.has-limit L-lim)
      (eps .η) (λ f → sym (eps .is-natural _ _ f) ∙ C.elimr (K .F-id)) refl
      $ conservative
      $ invert

    where
      module L-lim = Limit L-lim
      module FL-lim = is-limit (preservesa L-lim.has-limit)
      module FK-lim = is-limit FK-lim

      uinv : D.Hom (F .F₀ L-lim.apex) (F .F₀ (K .F₀ tt))
      uinv =
        FK-lim.universal
          (λ j → F .F₁ (L-lim.ψ j))
          (λ f → sym (F .F-∘ _ _) ∙ ap (F .F₁) (L-lim.commutes f))

      invert : D.is-invertible (F .F₁ (L-lim.universal (eps .η) _))
      invert =
        D.make-invertible uinv
          (FL-lim.unique₂ _ (λ j → FL-lim.commutes j)
            (λ j → F.pulll (L-lim.factors _ _) ∙ FK-lim.factors _ _)
            (λ j → D.idr _))
          (FK-lim.unique₂ _ (λ j → FK-lim.commutes j)
            (λ j → D.pulll (FK-lim.factors _ _) ∙ F.collapse (L-lim.factors _ _))
            (λ j → D.idr _))

Clearly, if $F$ is conservative then so is $F^{op},$ so the statement about colimits follows by duality.

  conservative-reflects-colimits
    : ∀ {Dia : Functor J C}
    → Colimit Dia
    → preserves-colimit F Dia
    → reflects-colimit F Dia

  conservative-reflects-colimits C-colim preservesa {K} {eta} FK-colim =
    is-invertible→is-colimitp
      {K = Colimit.Ext C-colim} {etay = Colimit.cocone C-colim} (Colimit.has-colimit C-colim)
      (eta .η) (λ f → eta .is-natural _ _ f ∙ C.eliml (K .F-id)) refl
      $ conservative
      $ invert

    where
      module C-colim = Colimit C-colim
      module FC-colim = is-colimit (preservesa C-colim.has-colimit)
      module FK-colim = is-colimit FK-colim

      uinv : D.Hom (F .F₀ (K .F₀ tt)) (F .F₀ C-colim.coapex)
      uinv =
        FK-colim.universal
          (λ j → F .F₁ (C-colim.ψ j))
          (λ f → sym (F .F-∘ _ _) ∙ ap (F .F₁) (C-colim.commutes f))

      invert : D.is-invertible (F .F₁ (C-colim.universal (eta .η) _))
      invert =
        D.make-invertible uinv
          (FK-colim.unique₂ _ (λ j → FK-colim.commutes j)
            (λ j → D.pullr (FK-colim.factors _ _) ∙ F.collapse (C-colim.factors _ _))
            (λ j → D.idl _))
          (FC-colim.unique₂ _ (λ j → FC-colim.commutes j)
            (λ j → F.pullr (C-colim.factors _ _) ∙ FK-colim.factors _ _)
            (λ j → D.idl _))