open import Cat.Diagram.Colimit.Base
open import Cat.Functor.Conservative
open import Cat.Functor.Kan.Unique
open import Cat.Functor.Kan.Base
open import Cat.Instances.Slice
open import Cat.Prelude

import Cat.Reasoning

open Functor
open /-Obj
open /-Hom
open _=>_

module Cat.Instances.Slice.Colimit
{o β} {C : Precategory o β} {c : β C β}
where


# Colimits in slicesπ

Unlike limits in slice categories, colimits in a slice category are computed just like colimits in the base category. That is, if we are given a diagram such that has a colimit in (where is the forgetful functor we can conclude:

• that has a colimit in
• that this colimit is preserved by
• and that reflects colimits of

In summary, we say that creates the colimits that exist in To understand why the assumption that the colimit exists in is necessary, consider the case where is a poset, and weβre interested in computing bottom elements (initial objects, i.e. colimits of the empty diagram). Note that the existence of a bottom element in only means that there is a least element that is less than , but does not imply the existence of a global bottom element. For example, the poset pictured below has an initial object in the slice over but no global initial object.

private
module C   = Cat.Reasoning C
module C/c = Cat.Reasoning (Slice C c)

U : Functor (Slice C c) C
U = Forget/

module
_ {o' β'} {J : Precategory o' β'} (F : Functor J (Slice C c))
where
open make-is-colimit

private
module J = Cat.Reasoning J
module F = Functor F


Back to categories, letβs consider the case of coproducts, as in the diagram below. We are given a binary diagram in and a colimiting cocone in

The first observation is that there is a unique map that turns this into a cocone in

  Forget/-lifts-colimits : Colimit (U Fβ F) β Colimit F
Forget/-lifts-colimits UF-colim = to-colimit K-colim
module Forget/-lifts where
module UF-colim = Colimit UF-colim
K : C/c.Ob
K .domain = UF-colim.coapex
K .map = UF-colim.universal (Ξ» j β F.β j .map) (Ξ» f β F.β f .commutes)

mk : make-is-colimit F K
mk .Ο j .map = UF-colim.cocone .Ξ· j
mk .Ο j .commutes = UF-colim.factors _ _
mk .commutes f = ext (UF-colim.cocone .is-natural _ _ f β C.idl _)


All that remains is to show that this cocone is colimiting in Given another cocone with apex we get a map by the universal property of but we need to check that it commutes with the relevant maps into this follows from the uniqueness of the universal map.

      mk .universal eta comm .map = UF-colim.universal
(Ξ» j β eta j .map)
(Ξ» f β unext (comm f))
mk .universal eta comm .commutes = ext (UF-colim.unique _ _ _ Ξ» j β
C.pullr (UF-colim.factors _ _) β eta j .commutes)
mk .factors eta comm = ext (UF-colim.factors _ _)
mk .unique eta comm u fac = ext (UF-colim.unique _ _ _ Ξ» j β
unext (fac j))

K-colim : is-colimit F K (to-cocone mk)
K-colim = to-is-colimit mk

preserved : preserves-lan U K-colim
preserved = generalize-colimitp UF-colim.has-colimit refl


The colimit thus constructed is preserved by by construction, as we havenβt touched the βtopβ part of the diagram. We can generalise this to all colimits of

  Forget/-preserves-colimits : Colimit (U Fβ F) β preserves-colimit U F
Forget/-preserves-colimits UF-colim =
preserves-lanβpreserves-all U K-colim preserved
where open Forget/-lifts UF-colim


Finally, is conservative, hence it reflects the colimits that it preserves, provided they exist in We can use the fact that lifts limits to satisfy the hypotheses.

  Forget/-reflects-colimits : reflects-colimit U F
Forget/-reflects-colimits UK-colim = conservative-reflects-colimits
Forget/-is-conservative
(Forget/-lifts-colimits UF-colim)
(Forget/-preserves-colimits UF-colim)
UK-colim
where UF-colim = to-colimit UK-colim


In particular, if a category is cocomplete, then so are its slices:

is-cocompleteβslice-is-cocomplete
: β {o' β'}
β is-cocomplete o' β' C
β is-cocomplete o' β' (Slice C c)
is-cocompleteβslice-is-cocomplete colims F =
Forget/-lifts-colimits F (colims (U Fβ F))