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.

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))