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 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 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.!) β