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 $F : J \to C / c$ such that $U \circ F$ has a colimit in $C$ (where $U$ is the forgetful functor $C / c \to C),$ we can conclude:

that $F$ has a colimit in $C / c;$
that this colimit is preserved by $U;$
and that $U$ reflects colimits of $F .$

In summary, we say that $U$ creates the colimits that exist in $C .$ To understand why the assumption that the colimit exists in $C$ is necessary, consider the case where $C$ 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 $C / c$ only means that there is a least element that is less than $c$ , but does not imply the existence of a global bottom element. For example, the poset pictured below has an initial object $a$ in the slice over $c,$ but no global initial object.

Back to categories, let’s consider the case of coproducts, as in the diagram below. We are given a binary diagram $a \to c \leftarrow b$ in $C / c$ and a colimiting cocone $a \to a + b \leftarrow b$ in $C .$

The first observation is that there is a unique map $a + b \to c$ that turns this into a cocone in $C / c :$

  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 $C / c .$ Given another cocone with apex $z$ we get a map $a + b \to z$ by the universal property of $a + b,$ but we need to check that it commutes with the relevant maps into $c;$ 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 $U$ by construction, as we haven’t touched the “top” part of the diagram. We can generalise this to all colimits of $F .$

  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, $U$ is conservative, hence it reflects the colimits that it preserves, provided they exist in $C / c .$ We can use the fact that $U$ 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 $C$ 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))