module Cat.Functor.Conservative where

Conservative functorsπŸ”—

We say a functor is conservative if it reflects isomorphisms. More concretely, if f:A→Bf : A \to B is some morphism C\mathcal{C}, and if F(f)F(f) is an iso in D\mathcal{D}, then ff must have already been an iso in C\mathcal{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 that they preserve (given those limits exist in the first place!).

The rough proof sketch is as follows: Let KK be some cone in CC such that F(K)F(K) is a limit in DD, and LL a limit in CC of the same diagram. By the universal property of LL, there exists a map η\eta from the apex of KK to the apex of LL in CC. Furthermore, as F(K)F(K) is a limit in DD, F(η)F(\eta) becomes an isomorphism in DD. However, FF is conservative, which implies that η\eta was an isomorphism in CC all along! This means that KK must be a limit in CC 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}
                               β†’ (L : Limit Dia)
                               β†’ preserves-limit F Dia
                               β†’ reflects-limit F Dia
  conservative-reflects-limits L-lim preservesa {K} {eps} 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 lim = is-limit lim

      uinv : D.Hom (F .Fβ‚€ L-lim.apex) (F .Fβ‚€ (K .Fβ‚€ tt))
      uinv =
          (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 _ _) βˆ™ lim.factors _ _)
            (Ξ» j β†’ D.idr _))
          (lim.uniqueβ‚‚ _ (Ξ» j β†’ lim.commutes j)
            (Ξ» j β†’ D.pulll (lim.factors _ _) βˆ™ F.collapse (L-lim.factors _ _))
            (Ξ» j β†’ D.idr _))