open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Terminal
open import Cat.Functor.Base
open import Cat.Morphism
open import Cat.Prelude hiding (J)

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\ca{C}, and if F(f)F(f) is an iso in D\ca{D}, then ff must have already been an iso in C\ca{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 apex-iso→is-limit).

module _ {F : Functor C D} (conservative : is-conservative F) where
  conservative-reflects-limits : βˆ€ {Dia : Functor J C} β†’ (L : Limit Dia)
                               β†’ (βˆ€ (K : Cone Dia) β†’ Preserves-limit F K)
                               β†’ (βˆ€ (K : Cone Dia) β†’ Reflects-limit F K)
  conservative-reflects-limits {Dia = Dia} L-lim preserves K limits =
    apex-iso→is-limit Dia K L-lim
      $ conservative
      $ subst (Ξ» Ο• β†’ is-invertible D Ο•) F-preserves-universal
      $ Cone-invertibleβ†’apex-invertible (F F∘ Dia)
      $ !-invertible (Cones (F F∘ Dia)) F∘L-lim K-lim
    where
      F∘L-lim : Limit (F F∘ Dia)
      F∘L-lim .Terminal.top = F-map-cone F (Terminal.top L-lim)
      F∘L-lim .Terminal.has⊀ = preserves (Terminal.top L-lim) (Terminal.has⊀ L-lim)

      K-lim : Limit (F F∘ Dia)
      K-lim .Terminal.top = F-map-cone F K
      K-lim .Terminal.has⊀ = limits

      module L-lim = Terminal L-lim
      module F∘L-lim = Terminal F∘L-lim
      open Cone-hom

      F-preserves-universal
        : hom F∘L-lim.! ≑ F .F₁ (hom {x = K} L-lim.!)
      F-preserves-universal =
        hom F∘L-lim.!                             β‰‘βŸ¨ ap hom (F∘L-lim.!-unique (F-map-cone-hom F L-lim.!)) βŸ©β‰‘
        hom (F-map-cone-hom F (Terminal.! L-lim)) β‰‘βŸ¨βŸ©
        F .F₁ (hom L-lim.!)                       ∎