module Cat.Instances.Functor.Limits where
Limits in functor categoriesπ
Let be a category admitting -shaped limits. Then the functor category , for any category, also admits -shaped limits. In particular, if is -complete, then so is .
module _ {oβ ββ} {C : Precategory oβ ββ} {oβ ββ} {D : Precategory oβ ββ} {oβ ββ} {E : Precategory oβ ββ} (has-D-lims : β (F : Functor D C) β Limit F) (F : Functor D Cat[ E , C ]) where
open Terminal open Functor open _=>_ import Cat.Reasoning C as C import Cat.Reasoning D as D import Cat.Reasoning E as E private module F = Functor F
Let be a diagram, and suppose admits limits of -shaped diagrams; We wish to compute the limit . First, observe that we can Uncurry to obtain a functor ; By fixing the value of the coordinate (say, to ), we obtain a family of -shaped diagrams in , which, by assumption, all have limits.
F-uncurried : Functor (D ΓαΆ E) C F-uncurried = Uncurry {C = D} {D = E} {E = C} F import Cat.Functor.Bifunctor {C = D} {D = E} {E = C} F-uncurried as Fβ² module D-lim x = Limit (has-D-lims (Fβ².Left x))
Let us call the limit of
β taken in
β lim-for
, and similarly the
unique, βterminatingβ cone homomorphism
will be called !-for.
!-for : β {x y} (f : E.Hom x y) β C.Hom (D-lim.apex x) (D-lim.apex y) !-for {x} {y} f = D-lim.universal y (Ξ» j β Fβ².Right j .Fβ f C.β D-lim.Ο x j) (Ξ» g β C.extendl Fβ².firstβsecond β apβ C._β_ refl (D-lim.commutes x g)) functor-apex : Functor E C functor-apex .Fβ x = D-lim.apex x functor-apex .Fβ {x} {y} f = !-for f functor-apex .F-id = sym $ D-lim.unique _ _ _ _ Ξ» j β C.idr _ β sym (D-lim.commutes _ _) functor-apex .F-β f g = sym $ D-lim.unique _ _ _ _ Ξ» j β C.pulll (D-lim.factors _ _ _) β C.pullr (D-lim.factors _ _ _) β C.pulll (sym (Fβ².Right _ .F-β _ _)) functor-limit : Limit F functor-limit = to-limit $ to-is-limit ml where open make-is-limit ml : make-is-limit F functor-apex ml .Ο j .Ξ· x = D-lim.Ο x j ml .Ο j .is-natural x y f = D-lim.factors _ _ _ β apβ C._β_ (C.eliml (F.F-id Ξ·β _)) refl ml .commutes f = Nat-path Ξ» j β C.pushr (C.introl (F.β _ .F-id)) β D-lim.commutes j f ml .universal eta p .Ξ· x = D-lim.universal x (Ξ» j β eta j .Ξ· x) (Ξ» f β apβ C._β_ (C.elimr (F.β _ .F-id)) refl β p f Ξ·β x) ml .universal eta p .is-natural x y f = D-lim.uniqueβ y _ (Ξ» g β C.pulll (apβ C._β_ (C.elimr (F.β _ .F-id)) refl β p g Ξ·β y)) (Ξ» j β C.pulll (D-lim.factors _ _ _)) (Ξ» j β C.pulll (D-lim.factors _ _ _) β C.pullr (D-lim.factors _ _ _) β apβ C._β_ (C.eliml (F.F-id Ξ·β _)) refl β sym (eta j .is-natural x y f)) ml .factors eta p = Nat-path Ξ» j β D-lim.factors j _ _ ml .unique eta p other q = Nat-path Ξ» x β D-lim.unique _ _ _ _ Ξ» j β q j Ξ·β x
As a corollary, if is an -complete category, then so is .
Functor-cat-is-complete : β {o β} {oβ ββ} {C : Precategory oβ ββ} {oβ ββ} {D : Precategory oβ ββ} β is-complete o β D β is-complete o β Cat[ C , D ] Functor-cat-is-complete D-complete = functor-limit D-complete
module _ {oβ ββ} {C : Precategory oβ ββ} {oβ ββ} {D : Precategory oβ ββ} {oβ ββ} {E : Precategory oβ ββ} (has-D-colims : β (F : Functor D C) β Colimit F) (F : Functor D Cat[ E , C ]) where functor-colimit : Colimit F functor-colimit = colim where Fβ² : Functor (D ^op) Cat[ E ^op , C ^op ] Fβ² = op-functorβ Fβ Functor.op F Fβ²-lim : Limit Fβ² Fβ²-lim = functor-limit (Ξ» f β subst Limit F^op^opβ‘F (ColimitβCo-limit _ (has-D-colims (Functor.op f)))) Fβ² LFβ²β² : Limit (op-functorβ {C = E} {D = C} Fβ (op-functorβ Fβ Functor.op F)) LFβ²β² = right-adjoint-limit (is-equivalence.Fβ£Fβ»ΒΉ op-functor-is-equiv) Fβ²-lim LFop : Limit (Functor.op F) LFop = subst Limit (Fβ-assoc β ap (_Fβ Functor.op F) op-functorββ β Fβ-idl) LFβ²β² colim : Colimit F colim = Co-limitβColimit _ LFop Functor-cat-is-cocomplete : β {o β} {oβ ββ} {C : Precategory oβ ββ} {oβ ββ} {D : Precategory oβ ββ} β is-cocomplete o β D β is-cocomplete o β Cat[ C , D ] Functor-cat-is-cocomplete D-cocomplete = functor-colimit D-cocomplete