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β.
We define colimits in a similar way to limits; the only difference being that we define a colimits of a diagram as left Kan extensions instead of right Kan extensions. This gives us the expected βmapping outβ universal property, as opposed to the βmapping inβ property associated to limits.
Note that approach to colimits is not what normally presented in introductory material. Instead, most books opt to define colimits via cocones, as they are less abstract, though harder to work with in the long run.
module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} (Diagram : Functor J C) where private module C = Precategory C coconeβunit : β {x : C.Ob} β (Diagram => Const x) β Diagram => const! x Fβ !F unquoteDef coconeβunit = define-coherence coconeβunit is-colimit : (x : C.Ob) β Diagram => Const x β Type _ is-colimit x cocone = is-lan !F Diagram (const! x) (coconeβunit cocone) Colimit : Type _ Colimit = Lan !F Diagram
Concretelyπ
As mentioned, our definition is very abstract, meaning we can directly re-use definitions and theorems about Kan extensions in the setting of colimits. The trade-off is that while working with colimits in general is easier, working with specific colimits becomes more difficult, as the data we actually care about has been obfuscated.
One particularly egregious failure is⦠actually constructing colimits. The definition in terms of Lan hides the concrete data behind a few abstractions, which would be very tedious to write out each time. To work around this, we provide an auxiliary record type, make-is-colimit, as an intermediate step in constructing left extensions.
module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} where private module J = Precategory J module C = Cat.Reasoning C record make-is-colimit (Diagram : Functor J C) (coapex : C.Ob) : Type (oβ β hβ β oβ β hβ) where no-eta-equality open Functor Diagram
First, we require morphisms from the every value of the diagram to the coapex; taken as a family, we call it . Moreover, if is a morphism in the βshapeβ category , we require , which encodes the relevant naturality.
field Ο : (j : J.Ob) β C.Hom (Fβ j) coapex commutes : β {x y} (f : J.Hom x y) β Ο y C.β Fβ f β‘ Ο x
The rest of the data ensures that is the universal family of maps with this property; if is another natural family, then each factors through the coapex by a unique universal morphism:
universal : β {x : C.Ob} β (eps : β j β C.Hom (Fβ j) x) β (β {x y} (f : J.Hom x y) β eps y C.β Fβ f β‘ eps x) β C.Hom coapex x factors : β {j : J.Ob} {x : C.Ob} β (eps : β j β C.Hom (Fβ j) x) β (p : β {x y} (f : J.Hom x y) β eps y C.β Fβ f β‘ eps x) β universal eps p C.β Ο j β‘ eps j unique : β {x : C.Ob} β (eps : β j β C.Hom (Fβ j) x) β (p : β {x y} (f : J.Hom x y) β eps y C.β Fβ f β‘ eps x) β (other : C.Hom coapex x) β (β j β other C.β Ο j β‘ eps j) β other β‘ universal eps p
uniqueβ : β {x : C.Ob} β (eps : β j β C.Hom (Fβ j) x) β (p : β {x y} (f : J.Hom x y) β eps y C.β Fβ f β‘ eps x) β β {o1} β (β j β o1 C.β Ο j β‘ eps j) β β {o2} β (β j β o2 C.β Ο j β‘ eps j) β o1 β‘ o2 uniqueβ eps p q r = unique eps p _ q β sym (unique eps p _ r)
Once we have this data, we can use it to construct a value of type is-colimit. The naturality condition we required above may seem too weak, but the full naturality condition can be derived from it and the rest of the data.
open _=>_ to-cocone : β {D : Functor J C} {coapex} β make-is-colimit D coapex β D => Const coapex to-cocone ml .Ξ· = ml .make-is-colimit.Ο to-cocone ml .is-natural x y f = (ml .make-is-colimit.commutes f) β sym (C.idl _)
to-is-colimit : β {Diagram : Functor J C} {coapex} β (mc : make-is-colimit Diagram coapex) β is-colimit Diagram coapex (to-cocone mc) to-is-colimit {Diagram} {coapex} mkcolim = colim where open make-is-colimit mkcolim open is-lan open Functor colim : is-colimit Diagram coapex (to-cocone mkcolim) colim .Ο {M = M} Ξ± .Ξ· _ = universal (Ξ± .Ξ·) (Ξ» f β Ξ± .is-natural _ _ f β C.eliml (M .F-id)) colim .Ο {M = M} Ξ± .is-natural _ _ _ = C.idr _ β C.introl (M .F-id) colim .Ο-comm {Ξ± = Ξ±} = Nat-path Ξ» j β factors (Ξ± .Ξ·) _ colim .Ο-uniq {Ξ± = Ξ±} {Οβ² = Οβ²} p = Nat-path Ξ» _ β sym $ unique (Ξ± .Ξ·) _ (Οβ² .Ξ· _) (Ξ» j β sym (p Ξ·β j))
-- We often find ourselves working with something that isn't a colimit -- on the nose due to some annoying extensionality reasons involving -- functors 'β€Cat β C' -- We could use some general theorems of Kan extensions to adjust the -- colimit, but this has better definitional behaviour. generalize-colimitp : β {D : Functor J C} {K : Functor β€Cat C} β {eta : D => (const! (Functor.Fβ K tt)) Fβ !F} {eta' : D => K Fβ !F} β is-lan !F D (const! (Functor.Fβ K tt)) eta β (β {j} β eta .Ξ· j β‘ eta' .Ξ· j) β is-lan !F D K eta' generalize-colimitp {D} {K} {eta} {eta'} lan q = lan' where module lan = is-lan lan open is-lan open Functor lan' : is-lan !F D K eta' lan' .Ο Ξ± = homββ€-natural-trans (lan.Ο Ξ± .Ξ· tt) lan' .Ο-comm {M} {Ξ±} = Nat-path Ξ» j β ap (_ C.β_) (sym q) β lan.Ο-comm {Ξ± = Ξ±} Ξ·β _ lan' .Ο-uniq {M} {Ξ±} {Οβ²} r = Nat-path Ξ» j β lan.Ο-uniq {Οβ² = homββ€-natural-trans (Οβ² .Ξ· tt)} (Nat-path (Ξ» j β r Ξ·β j β ap (_ C.β_) (sym q))) Ξ·β j to-is-colimitp : β {D : Functor J C} {K : Functor β€Cat C} {eta : D => K Fβ !F} β (mk : make-is-colimit D (Functor.Fβ K tt)) β (β {j} β to-cocone mk .Ξ· j β‘ eta .Ξ· j) β is-lan !F D K eta to-is-colimitp {D} {K} {eta} mkcolim p = generalize-colimitp (to-is-colimit mkcolim) p
The concrete interface of make-is-colimit is also handy for consuming specific colimits. To enable this use case, we provide a function which unmakes a colimit.
unmake-colimit : β {D : Functor J C} {F : Functor β€Cat C} {eta} β is-lan !F D F eta β make-is-colimit D (Functor.Fβ F tt) unmake-colimit {D} {F} {eta} colim = mc module unmake-colimit where coapex = Functor.Fβ F tt module eta = _=>_ eta open is-lan colim open Functor D open make-is-colimit open _=>_ module _ {x} (eps : β j β C.Hom (Fβ j) x) (p : β {x y} (f : J.Hom x y) β eps y C.β Fβ f β‘ eps x) where eps-nt : D => const! x Fβ !F eps-nt .Ξ· = eps eps-nt .is-natural _ _ f = p f β sym (C.idl _) hom : C.Hom coapex x hom = Ο {M = const! x} eps-nt .Ξ· tt mc : make-is-colimit D coapex mc .Ο = eta.Ξ· mc .commutes f = eta.is-natural _ _ f β C.eliml (Functor.F-id F) mc .universal = hom mc .factors e p = Ο-comm {Ξ± = eps-nt e p} Ξ·β _ mc .unique {x = x} eta p other q = sym $ Ο-uniq {Οβ² = other-nt} (Nat-path Ξ» j β sym (q j)) Ξ·β tt where other-nt : F => const! x other-nt .Ξ· _ = other other-nt .is-natural _ _ _ = C.elimr (Functor.F-id F) β sym (C.idl _)
to-colimit : β {D : Functor J C} {K : Functor β€Cat C} {eta : D => K Fβ !F} β is-lan !F D K eta β Colimit D to-colimit c .Lan.Ext = _ to-colimit c .Lan.eta = _ to-colimit c .Lan.has-lan = c
module is-colimit {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Functor J C} {F : Functor β€Cat C} {eta : D => F Fβ !F} (t : is-lan !F D F eta) where open make-is-colimit (unmake-colimit {F = F} t) public
We also provide a similar interface for the bundled form of colimits.
module Colimit {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Functor J C} (L : Colimit D) where
private import Cat.Reasoning J as J import Cat.Reasoning C as C module Diagram = Functor D open Lan L open Functor open _=>_
The coapex of the colimit can be obtained by applying the extension functor to the single object of β€Cat.
coapex : C.Ob coapex = Ext .Fβ tt
Furthermore, we can show that the apex is the colimit, in the sense
of is-colimit, of the diagram. Youβd think this
is immediate, but unfortunately, proof assistants: is-colimit asks for the constant
functor functor
with value coapex
to be a Kan extension, but Colimit, being an instance of Lan, packages an arbitrary functor
.
Since Agda does not compare functors for -equality, we have to shuffle our data around manually. Fortunately, this isnβt a very long computation.
cocone : D => Const coapex cocone .Ξ· = eta .Ξ· cocone .is-natural x y f = eta .is-natural x y f β ap (C._β _) (Ext .F-id) has-colimit : is-colimit D coapex cocone has-colimit .is-lan.Ο Ξ± .Ξ· = Ο Ξ± .Ξ· has-colimit .is-lan.Ο Ξ± .is-natural x y f = ap (_ C.β_) (sym (Ext .F-id)) β Ο Ξ± .is-natural tt tt tt has-colimit .is-lan.Ο-comm = Nat-path (Ξ» _ β Ο-comm Ξ·β _) has-colimit .is-lan.Ο-uniq {M = M} {Οβ² = Οβ²} p = Nat-path (Ξ» _ β Ο-uniq {Οβ² = nt} (Nat-path (Ξ» j β p Ξ·β j)) Ξ·β _) where nt : Ext => M nt .Ξ· = Οβ² .Ξ· nt .is-natural x y f = ap (_ C.β_) (Ext .F-id) β Οβ² .is-natural x y f open is-colimit has-colimit public
Uniquenessπ
Much like limits, colimits are unique up to isomorphism. This all follows from general properties of Kan extensions, combined with the fact that natural isomorphisms between functors correspond with isomorphisms in .
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {Diagram : Functor J C} {x y} {etay : Diagram => Const y} {etax : Diagram => Const x} (Cy : is-colimit Diagram y etay) (Cx : is-colimit Diagram x etax) where private module J = Precategory J module C = Cat.Reasoning C module Diagram = Functor Diagram open is-lan open _=>_ module Cy = is-colimit Cy module Cx = is-colimit Cx
colimitsβinversesp : β {f : C.Hom x y} {g : C.Hom y x} β (β {j : J.Ob} β f C.β Cx.Ο j β‘ Cy.Ο j) β (β {j : J.Ob} β g C.β Cy.Ο j β‘ Cx.Ο j) β C.Inverses f g colimitsβinvertiblep : β {f : C.Hom x y} β (β {j : J.Ob} β f C.β Cx.Ο j β‘ Cy.Ο j) β C.is-invertible f colimits-unique : x C.β y colimitsβinvertible : C.is-invertible (Cx.universal Cy.Ο Cy.commutes) colimitsβinverses : C.Inverses (Cx.universal Cy.Ο Cy.commutes) (Cy.universal Cx.Ο Cx.commutes)
colimitsβinversesp {f = f} {g = g} f-factor g-factor = natural-inversesβinverses {Ξ± = homββ€-natural-trans f} {Ξ² = homββ€-natural-trans g} (Lan-unique.Ο-inversesp Cx Cy (Nat-path Ξ» j β f-factor {j}) (Nat-path Ξ» j β g-factor {j})) tt colimitsβinvertiblep {f = f} f-factor = is-natural-invertibleβinvertible {Ξ± = homββ€-natural-trans f} (Lan-unique.Ο-is-invertiblep Cx Cy (Nat-path Ξ» j β f-factor {j})) tt colimitsβinverses = colimitsβinversesp (Cx.factors Cy.Ο Cy.commutes) (Cy.factors Cx.Ο Cx.commutes) colimitsβinvertible = colimitsβinvertiblep (Cx.factors Cy.Ο Cy.commutes) colimits-unique = Nat-isoβIso (Lan-unique.unique Cx Cy) tt
Furthermore, if the universal map is invertible, then that means its domain is also a colimit of the diagram. This also follows from a general theorem of Kan extensions, though some golfin is required to obtain the correct inverse definitionally.
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Functor J C} {K : Functor β€Cat C} {etay : D => Const (Functor.Fβ K tt)} (Cy : is-colimit D (Functor.Fβ K tt) etay) where private module J = Precategory J module C = Cat.Reasoning C module D = Functor D open is-ran open Functor open _=>_ module Cy = is-colimit Cy familyβcocone : β {x} β (eps : β j β C.Hom (D.β j) x) β (β {x y} (f : J.Hom x y) β eps y C.β D.β f β‘ eps x) β D => Const x familyβcocone eta p .Ξ· = eta familyβcocone eta p .is-natural _ _ _ = p _ β sym (C.idl _)
is-invertibleβis-colimitp : β {K' : Functor β€Cat C} {eta : D => K' Fβ !F} β (eps : β j β C.Hom (D.β j) (K' .Fβ tt)) β (p : β {x y} (f : J.Hom x y) β eps y C.β D.β f β‘ eps x) β (β {j} β eps j β‘ eta .Ξ· j) β C.is-invertible (Cy.universal eps p) β is-lan !F D K' eta is-invertibleβis-colimitp {K' = K'} {eta = eta} eps p q invert = generalize-colimitp (is-invertibleβis-lan Cy $ componentwise-invertibleβinvertible _ Ξ» _ β invert) q
Another useful fact is that if is a colimit of some diagram , and is naturally isomorphic to some other diagram , then the coapex of is also a colimit of .
natural-iso-diagramβis-colimitp : β {Dβ² : Functor J C} {eta : Dβ² => K Fβ !F} β (isos : natural-iso D Dβ²) β (β {j} β Cy.Ο j C.β natural-iso.from isos .Ξ· j β‘ eta .Ξ· j) β is-lan !F Dβ² K eta natural-iso-diagramβis-colimitp {Dβ² = Dβ²} isos q = generalize-colimitp (natural-iso-ofβis-lan Cy isos) q
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D Dβ² : Functor J C} where natural-isoβcolimit : natural-iso D Dβ² β Colimit D β Colimit Dβ² natural-isoβcolimit isos C .Lan.Ext = Lan.Ext C natural-isoβcolimit isos C .Lan.eta = Lan.eta C βnt natural-iso.from isos natural-isoβcolimit isos C .Lan.has-lan = natural-iso-ofβis-lan (Lan.has-lan C) isos
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {Diagram : Functor J C} {x} {eta : Diagram => Const x} where private module J = Precategory J module C = Cat.Reasoning C module Diagram = Functor Diagram open is-lan open _=>_ is-colimit-is-prop : is-prop (is-colimit Diagram x eta) is-colimit-is-prop = is-lan-is-prop
Since is-colimit is a proposition, and the colimiting cocones are all unique (βup to isomorphismβ), if weβre talking about univalent categories, then Colimit itself is a proposition. This is also an instance of the more general uniqueness of Kan extensions.
module _ {oβ hβ oβ hβ : _} {J : Precategory oβ hβ} {C : Precategory oβ hβ} {Diagram : Functor J C} where
Colimit-is-prop : is-category C β is-prop (Colimit Diagram) Colimit-is-prop cat = Lan-is-prop cat
Preservation of Colimitsπ
The definitions here are the same idea as preservation of limits, just dualized.
module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} (F : Functor C D) (Diagram : Functor J C) where private module D = Precategory D module C = Precategory C module J = Precategory J module F = Func F
preserves-colimit : Type _ preserves-colimit = β {K : Functor β€Cat C} {eta : Diagram => K Fβ !F} β (colim : is-lan !F Diagram K eta) β preserves-lan F colim reflects-colimit : Type _ reflects-colimit = β {K : Functor β€Cat C} {eps : Diagram => K Fβ !F} β (lan : is-lan !F (F Fβ Diagram) (F Fβ K) (nat-assoc-to (F βΈ eps))) β reflects-lan F lan
module preserves-colimit {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} {F : Functor C D} {Dia : Functor J C} (preserves : preserves-colimit F Dia) where private module D = Precategory D module C = Precategory C module J = Precategory J module F = Func F module Dia = Func Dia universal : {x : C.Ob} β {K : Functor β€Cat C} {eta : Dia => K Fβ !F} β {eps : (j : J.Ob) β C.Hom (Dia.Fβ j) x} β {p : β {i j} (f : J.Hom i j) β eps j C.β Dia.Fβ f β‘ eps i} β (colim : is-lan !F Dia K eta) β F.Fβ (is-colimit.universal colim eps p) β‘ is-colimit.universal (preserves colim) (Ξ» j β F.Fβ (eps j)) (Ξ» f β F.collapse (p f)) universal colim = is-colimit.unique (preserves colim) _ _ _ (Ξ» j β F.collapse (is-colimit.factors colim _ _)) colimit : Colimit Dia β Colimit (F Fβ Dia) colimit colim = to-colimit (preserves (Colimit.has-colimit colim)) module _ {J : Precategory oβ hβ} {C : Precategory oβ hβ} {D : Precategory oβ hβ} {F F' : Functor C D} {Dia : Functor J C} where private module D = Cat.Reasoning D open Func open _=>_ natural-isoβpreserves-colimits : natural-iso F F' β preserves-colimit F Dia β preserves-colimit F' Dia natural-isoβpreserves-colimits Ξ± F-preserves {K = K} {eps} colim = natural-isosβis-lan idni (Ξ± βni Dia) (Ξ± βni K) (Nat-path Ξ» j β β F' .Fβ (K .Fβ tt) D.β Ξ±.to .Ξ· _ β D.β (F .Fβ (eps .Ξ· j) D.β Ξ±.from .Ξ· _) β‘β¨ ap! (eliml F' (K .F-id)) β©β‘ Ξ±.to .Ξ· _ D.β (F .Fβ (eps .Ξ· j) D.β Ξ±.from .Ξ· _) β‘β¨ D.pushr (sym (Ξ±.from .is-natural _ _ _)) β©β‘ ((Ξ±.to .Ξ· _ D.β Ξ±.from .Ξ· _) D.β F' .Fβ (eps .Ξ· j)) β‘β¨ D.eliml (Ξ±.invl Ξ·β _) β©β‘ F' .Fβ (eps .Ξ· j) β) (F-preserves colim) where module Ξ± = natural-iso Ξ±
Cocontinuityπ
is-cocontinuous : β (oshape hshape : Level) {C : Precategory oβ hβ} {D : Precategory oβ hβ} β Functor C D β Type _
A cocontinuous functor is one that, for every shape of diagram
J
, and every diagram diagram
of shape J
in
C
, preserves the colimit for that diagram.
is-cocontinuous oshape hshape {C = C} F = β {J : Precategory oshape hshape} {Diagram : Functor J C} β preserves-colimit F Diagram
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