open import Cat.Functor.Adjoint.Continuous open import Cat.Instances.Functor.Duality open import Cat.Diagram.Colimit.Base open import Cat.Functor.Equivalence open import Cat.Diagram.Limit.Base open import Cat.Diagram.Equaliser open import Cat.Instances.Functor open import Cat.Instances.Product open import Cat.Diagram.Pullback open import Cat.Diagram.Terminal open import Cat.Diagram.Product open import Cat.Diagram.Duals open import Cat.Prelude 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
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β²
Let us call the limit of β taken in β lim-for, and similarly the unique, βterminatingβ cone homomorphism will be called !-for.
lim-for : β x β _ lim-for x = has-D-lims (Fβ².Left x) .top !-for : β {x} K β _ !-for {x} K = has-D-lims (Fβ².Left x) .hasβ€ K .centre !-for-unique : β {x} {K} h β !-for K β‘ h !-for-unique {x} {K} = has-D-lims (Fβ².Left x) .hasβ€ K .paths
The two fundamental β and very similar looking! β constructions are Lift-cone and map-cone below. Lift-cone lets us take a component of a cone for β in the functor category β into a cone for , in . Furthermore, at the same time as we perform this lifting, we can βadjustβ the cone by a map .
Lift-cone : β {x y} (K : Cone F) (f : E.Hom x y) β Cone (Fβ².Left y) Lift-cone {x} {y} K f .apex = K .apex .Fβ x Lift-cone {x} {y} K f .Ο z = Fβ².second f C.β K .Ο z .Ξ· _ Lift-cone {x} {y} K g .commutes f = Fβ².first f C.β Fβ².second g C.β K .Ο _ .Ξ· x β‘β¨ C.extendl Fβ².firstβsecond β©β‘ Fβ².second g C.β Fβ².first f C.β K .Ο _ .Ξ· x β‘β¨ ap (Fβ².second _ C.β_) (apβ C._β_ (C.elimr (F-id (F.β _))) refl β K .commutes f Ξ·β x) β©β‘ Fβ².second g C.β K .Ο _ .Ξ· x β
The function map-cone is Lift-cone, but specialised to the case where is the lim-for a particular point in .
map-cone : β {x y} (f : E.Hom x y) β Cone (Fβ².Left y) map-cone {x} f .apex = lim-for x .apex map-cone {x} f .Ο z = Fβ².second f C.β lim-for x .Ο z map-cone {x} f .commutes g = Fβ².first g C.β Fβ².second f C.β lim-for x .Ο _ β‘β¨ C.extendl Fβ².firstβsecond β©β‘ Fβ².second f C.β Fβ².first g C.β lim-for x .Ο _ β‘β¨ ap (Fβ².second _ C.β_) (lim-for x .commutes _) β©β‘ Fβ².second f C.β lim-for x .Ο _ β
The coneπ
We are now ready to build a universal cone over , in the category , meaning the apex will be given by a functor . Using the fact that was assumed to have -shaped limits, the-apex will be given by . Similarly, the choice of map is essentially unique: we must map , but the space of maps is contractible.
functor-cone : Cone F functor-cone .apex = the-apex where the-apex : Functor E C the-apex .Fβ x = lim-for x .apex the-apex .Fβ {x} {y} f = !-for (map-cone f) .hom
We use that contractibility of mapping spaces to prove the-apex is actually a functor.
the-apex .F-id = ap hom (!-for-unique map) where map : Cone-hom _ _ _ map .hom = C.id map .commutes _ = C.idr _ β C.introl Fβ².second-id the-apex .F-β {x} {y} {z} f g = ap hom (!-for-unique map) where map : Cone-hom _ _ _ map .hom = the-apex .Fβ f C.β the-apex .Fβ g map .commutes o = (lim-for z .Ο o C.β _ C.β _) β‘β¨ C.extendl (!-for (map-cone f) .commutes _) β©β‘ (Fβ².second f C.β lim-for y .Ο o C.β _) β‘β¨ ap (Fβ².second f C.β_) (!-for (map-cone g) .commutes _) β©β‘ (Fβ².second f C.β Fβ².second g C.β lim-for x .Ο o) β‘β¨ C.pulll (sym Fβ².secondβsecond) β©β‘ (Fβ².second (f E.β g) C.β has-D-lims (Fβ².Left x) .top .Ο o) β
We must now give the construction of the actual cone, i.e.Β the natural transformations . The natural transformations are defined componentwise by taking to be the map underlying the cone homomorphism ; This is natural because is a family of cone homomorphisms, and the cone commutes since each limiting cone is indeed a cone.
functor-cone .Ο x .Ξ· y = lim-for y .Ο x functor-cone .Ο x .is-natural y z f = !-for (map-cone f) .commutes _ β apβ C._β_ (C.eliml (Ξ» i β F.F-id i .Ξ· z)) refl functor-cone .commutes f = Nat-path Ξ» x β apβ C._β_ (C.intror (F-id (F.β _))) refl β lim-for _ .commutes f
The mapsπ
For the functor-cone β our candidate for β to be limiting, we must, given some other cone , find a unique cone homomorphism . Weβll be fine, though: We can (using Lift-cone) explode into a bunch of cones , each lying over , and use the universal property of to find cone homs . Assuming these maps assemble to a natural transformation , we can show they commute with everything in sight:
functor-! : β K β Cone-hom F K functor-cone functor-! K = ch where map : β x β Cone-hom (Fβ².Left x) (Lift-cone K E.id) (lim-for x) map x = !-for (Lift-cone K E.id) ch : Cone-hom F K functor-cone ch .hom .Ξ· x = map _ .hom ch .commutes _ = Nat-path Ξ» x β map _ .commutes _ β C.eliml Fβ².second-id
The hard part, then, is showing that this is a natural transformation. Weβll do this in a roundabout way: Weβll show that both composites in the naturality square inhabit the same contractible space of cone homomorphisms, namely that of , and thus conclude that they are unique. This isnβt too hard, but it is quite tedious:
ch .hom .is-natural x y f = map y .hom C.β K .apex .Fβ f β‘β¨ (Ξ» i β is-contrβis-prop (has-D-lims (Fβ².Left y) .hasβ€ (Lift-cone K f)) h1 h2 i .hom) β©β‘ !-for (map-cone f) .hom C.β map x .hom β where h1 : Cone-hom (Fβ².Left y) (Lift-cone K f) (lim-for y) h1 .hom = map y .hom C.β K .apex .Fβ f h1 .commutes o = lim-for y .Ο o C.β map y .hom C.β K .apex .Fβ f β‘β¨ C.pulll (map y .commutes _ β C.eliml Fβ².second-id) β©β‘ K .Ο _ .Ξ· _ C.β K .apex .Fβ f β‘β¨ K .Ο _ .is-natural _ _ _ β©β‘ Fβ (F.β o) f C.β K .Ο o .Ξ· x β‘β¨ ap (C._β K .Ο o .Ξ· x) (C.introl (F-id F Ξ·β y)) β©β‘ Fβ².second f C.β K .Ο o .Ξ· x β h2 : Cone-hom (Fβ².Left y) (Lift-cone K f) (lim-for y) h2 .hom = has-D-lims (Fβ².Left y) .hasβ€ (map-cone f) .centre .hom C.β map x .hom h2 .commutes o = lim-for y .Ο o C.β !-for (map-cone f) .hom C.β map x .hom β‘β¨ C.pulll (has-D-lims (Fβ².Left y) .hasβ€ (map-cone f) .centre .commutes _) β©β‘ (Fβ².second f C.β lim-for x .Ο o) C.β map x .hom β‘β¨ C.pullr (map x .commutes _ β C.eliml Fβ².second-id) β©β‘ Fβ².second f C.β K .Ο o .Ξ· x β
Since we built the natural transformation underlying functor-! out of the unique maps !-for, we can appeal to that uniqueness here to conclude that functor-! is itself unique, showing that we put together a limit .
functor-!-unique : β {K} (h : Cone-hom F K functor-cone) β functor-! K β‘ h functor-!-unique h = Cone-hom-path _ (Nat-path Ξ» x β ap hom (!-for-unique hom')) where hom' : β {x} β Cone-hom (Fβ².Left x) _ _ hom' {x} .hom = h .hom .Ξ· x hom' {x} .commutes o = h .commutes o Ξ·β _ β C.introl Fβ².second-id functor-limit : Limit F functor-limit .top = functor-cone functor-limit .hasβ€ x .centre = functor-! x functor-limit .hasβ€ x .paths = functor-!-unique
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