open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Base
open import Cat.Morphism.Duality
open import Cat.Morphism
open import Cat.Prelude hiding (J)

import Cat.Functor.Reasoning as Func
import Cat.Reasoning as Cat

module Cat.Functor.Conservative where

private variable
  o h o₁ h₁ : Level
  C D J : Precategory o h
open Precategory
open Functor

Conservative functors🔗

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

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 $\mathcal{C}$ such that $F(K)$ is a limit in $\mathcal{D}\text{,}$ and $L$ a limit in $\mathcal{C}$ of the same diagram that is preserved by $F\text{.}$ By the universal property of $L\text{,}$ there exists a map $\eta$ from the apex of $K$ to the apex of $L$ in $\mathcal{C}\text{.}$ Furthermore, as $F(K)$ is a limit in $\mathcal{D}\text{,}$ $F(\eta )$ becomes an isomorphism in $\mathcal{D}\text{.}$ The situation is summarised by the following diagram, which shows how $F$ maps cones in $\mathcal{C}$ to cones in $\mathcal{D}$ (the coloured cones are assumed to be limiting).

However, $F$ is conservative, which implies that $\eta$ was an isomorphism in $\mathcal{C}$ all along! This means that $K$ must be a limit in $\mathcal{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 _))

  conservative→equiv :
    ∀ {A B} {f : C .Hom A B}
    → C.is-invertible f ≃ D.is-invertible (F .F₁ f)
  conservative→equiv = prop-ext! F.F-map-invertible conservative

  conservative^op : is-conservative F.op
  conservative^op inv
    = invertible→co-invertible C
    $ conservative
    $ co-invertible→invertible D inv

  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 _))