open import Cat.Diagram.Initial open import Cat.Prelude import Cat.Functor.Reasoning as Func import Cat.Morphism module Cat.Diagram.Colimit.Base where
Ideaπ
Colimits are dual to limits limit; much like their cousins, they generalize constructions in several settings to arbitrary categories. A colimit (if it exists), is the βbest solutionβ to an βidentification problemβ. This is in contrast to the limit, which acts as a solution to an βequational problemβ.
Constructionπ
Every concrete colimit (coproducts, coequalisers, initial objects) we have seen so far consists of roughly the same data. We begin with some collection of objects and morphisms, and then state that the colimit of that collection is some object with a universal property relating all of those objects and morphisms.
It would be convenient to be able to talk about all of these situations at once, as opposed to on a case-by-case basis. To do this, we need to introduce a bit of categorical machinery: the Cocone.
The first step is to generalize the βcollection of objects and morphismsβ involved. Luckily, this step involves no new ideas, just a change in perspective. We already have a way of describing a collection of objects and morphisms: itβs a category! As an example, the starting data of a coproduct is a pair of objects, which can be thought of as a very simple category, with only identity morphisms.
The next step also involves nothing more than a change in perspective. Letβs denote our βdiagramβ category from earlier as . Then, a means of picking out a shaped figure in isβ¦ a functor ! Going back to the coproduct example, a functor from our 2 object category into selects 2 (not necessarily distinct!) objects in . We this pair of category and functor a diagram in .
module _ {J : Precategory o β} {C : Precategory oβ² ββ²} (F : Functor J C) where private import Cat.Reasoning J as J import Cat.Reasoning C as C module F = Functor F record Cocone : Type (o β β β oβ² β ββ²) where no-eta-equality constructor cocone
Now, for the actual machinery! If we want to capture the essence of all of our concrete examples of colimits, we a notion of an object equipped with maps from every object in our diagram. We call this designated object the βcoapexβ of the cocone.
field coapex : C.Ob Ο : (x : J.Ob) β C.Hom (F.β x) coapex
If our diagram consisted of only objects, we would be done! However, some diagrams contain non-identity morphisms, so we need to take those into account as well. This bit is best understood through the lens of the coequaliser: in order to describe the commuting condition there, we want every injection map from the codomain of a morphism to factor through that morphism.
commutes : β {x y} (f : J.Hom x y) β Ο y C.β F.β f β‘ Ο x
As per usual, we define a helper lemma charaterizing the path space of cones:
open Cocone Cocone-path : {x y : Cocone} β (p : coapex x β‘ coapex y) β (β o β PathP (Ξ» i β C.Hom (F.β o) (p i)) (Ο x o) (Ο y o)) β x β‘ y Cocone-path p q i .coapex = p i Cocone-path p q i .Ο o = q o i Cocone-path {x = x} {y = y} p q i .commutes {x = a} {y = b} f = is-propβpathp (Ξ» i β C.Hom-set _ _ (q b i C.β F.β f) (q a i)) (x .commutes f) (y .commutes f) i
Cocone Mapsπ
Now that weβve defined cocones, we need a way to figure out how to express universal properties. Like most things categorical, we begin by considering a βcocone morphismβ, which will give us a category that we can work within. The idea here is that a morphism of cocones is a morphism in between the coapicies, such that all of the injection maps commute.
record Cocone-hom (x y : Cocone) : Type (o β ββ²) where no-eta-equality constructor cocone-hom field hom : C.Hom (x .coapex) (y .coapex) commutes : β o β hom C.β x .Ο o β‘ y .Ο o
We define yet another helper lemma that describes the path space of cocone morphisms.
open Cocone-hom Cocone-hom-path : β {x y} {f g : Cocone-hom x y} β f .hom β‘ g .hom β f β‘ g Cocone-hom-path p i .hom = p i Cocone-hom-path {x = x} {y = y} {f = f} {g = g} p i .commutes o j = is-setβsquarep (Ξ» i j β C.Hom-set _ _) (Ξ» j β p j C.β x .Ο o) (f .commutes o) (g .commutes o) refl i j
Now, we can define the category of cocones over a given diagram:
Cocones : Precategory _ _ Cocones = cat where open Precategory compose : β {x y z} β Cocone-hom y z β Cocone-hom x y β Cocone-hom x z compose K L .hom = K .hom C.β L .hom compose {x = x} {y = y} {z = z} K L .commutes o = (K .hom C.β L .hom) C.β x .Ο o β‘β¨ C.pullr (L .commutes o) β©β‘ K .hom C.β y .Ο o β‘β¨ K .commutes o β©β‘ z .Ο o β cat : Precategory _ _ cat .Ob = Cocone cat .Hom = Cocone-hom cat .id = cocone-hom C.id (Ξ» _ β C.idl _) cat ._β_ = compose cat .idr f = Cocone-hom-path (C.idr (f .hom)) cat .idl f = Cocone-hom-path (C.idl (f .hom)) cat .assoc f g h = Cocone-hom-path (C.assoc (f .hom) (g .hom) (h .hom))
Colimitsπ
We now have all of the machinery in place! What remains is the universal property, which expresses that a particular cocone is universal, in the sense that it has a unique map to any other cocone. However, we already have something that captures this idea, itβs the initial object! This leads to the following terse definition: A colimit over a diagram is an initial object in the category of cocones over that diagram.is-colimit : Cocone β Type _ is-colimit K = is-initial Cocones K Colimit : Type _ Colimit = Initial Cocones Colimit-apex : Colimit β C.Ob Colimit-apex x = coapex (Initial.bot x)
Preservation of Colimitsπ
Because a cocone is a commutative diagram, any given functor takes cocones in to cocones in , as functors preserve commutative diagrams.
F-map-cocone : Cocone Dia β Cocone (F Fβ Dia) F-map-cocone x .Cocone.coapex = F.β (Cocone.coapex x) F-map-cocone x .Cocone.Ο f = F.β (Cocone.Ο x f) F-map-cocone x .Cocone.commutes {y = y} f = F.β (Cocone.Ο x y) D.β F .Fβ _ β‘β¨ F.collapse (Cocone.commutes x _) β©β‘ F.β (Cocone.Ο x _) β
Though functors must take cocones to cocones, they may not necessarily take colimiting cocones to colimiting cocones! When a functor does, we say that it preserves colimits.
Preserves-colimit : Cocone Dia β Type _ Preserves-colimit K = is-colimit Dia K β is-colimit (F Fβ Dia) (F-map-cocone K)
Cocompletenessπ
A category is cocomplete if admits for limits of arbitrary shape. However, in the presence of excluded middle, if a category admits coproducts indexed by its class of morphisms, then it is automatically [thin]. Since excluded middle is independent of type theory, we can not prove that any non-thin categories have arbitrary colimits.
Instead, categories are cocomplete with respect to a pair of universes: A category is -cocomplete if it has colimits for any diagram indexed by a precategory with objects in and morphisms in .
is-cocomplete : β {oc βc} o β β Precategory oc βc β Type _ is-cocomplete o β C = β {D : Precategory o β} (F : Functor D C) β Colimit F