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 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 and colimits that they preserve (given those (co)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 that is preserved by 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 The situation is summarised by the following diagram, which shows how maps cones in to cones in (the coloured cones are assumes to be limiting).

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


Clearly, if is conservative then so is 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 _))