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