module Cat.Functor.Conservative where

Conservative functorsπŸ”—

We say a functor is conservative if it reflects isomorphisms. More concretely, if is some morphism and if is an iso in then must have already been an iso in

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 be some cone in such that is a limit in and a limit in of the same diagram. By the universal property of there exists a map from the apex of to the apex of in Furthermore, as is a limit in becomes an isomorphism in However, is conservative, which implies that was an isomorphism in all along! This means that must be a limit in as well (see is-invertible→is-limitp).

module _ {F : Functor C D} (conservative : is-conservative F) where
    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 =
      {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

      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 =
            (Ξ» j β†’ F .F₁ (L-lim.ψ j))
            (Ξ» f β†’ sym (F .F-∘ _ _) βˆ™ ap (F .F₁) (L-lim.commutes f)))

      invert : (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 _))