module Cat.Instances.Slice.Limit where

Arbitrary limits in slicesπŸ”—

Suppose we have some really weird diagram like the one below. Well, alright, it’s not that weird, but it’s not a pullback or a terminal object, so we don’t a priori know how to compute its limit in the slice.

The observation that will let us compute a limit for this diagram is inspecting the computation of products in slice categories, above. To compute the product of and we had to pass to a pullback of in β€” which we had assumed exists. But! Take a look at what that diagram looks like:

We β€œexploded” a diagram of shape to one of shape This process can be described in a way easier to generalise: We β€œexploded” our diagram to one indexed by a category which contains contains an extra point, and has a unique map between each object of β€” the join of these categories.

Generically, if we have a diagram we can β€œexplode” this into a diagram compute the limit in then pass back to the slice category.

    F' : Functor (J ⋆ ⊀Cat) C
    F' .Fβ‚€ (inl x) = F.β‚€ x .domain
    F' .Fβ‚€ (inr x) = o
    F' .F₁ {inl x} {inl y} (lift f) = F.₁ f .map
    F' .F₁ {inl x} {inr y} _ = F.β‚€ x .map
    F' .F₁ {inr x} {inr y} (lift h) = C.id
    F' .F-id {inl x} = ap map F.F-id
    F' .F-id {inr x} = refl
    F' .F-∘ {inl x} {inl y} {inl z} (lift f) (lift g) = ap map (F.F-∘ f g)
    F' .F-∘ {inl x} {inl y} {inr z} (lift f) (lift g) = sym (F.F₁ g .commutes)
    F' .F-∘ {inl x} {inr y} {inr z} (lift f) (lift g) = C.introl refl
    F' .F-∘ {inr x} {inr y} {inr z} (lift f) (lift g) = C.introl refl

  limit-above→limit-in-slice : Limit F' → Limit F
  limit-above→limit-in-slice lims = to-limit (to-is-limit lim) where
    module lims = Limit lims
    open make-is-limit

    apex : C/o.Ob
    apex = cut (lims.ψ (inr tt))

    nadir : (j : J.Ob) β†’ /-Hom apex (F .Fβ‚€ j)
    nadir j .map = lims.ψ (inl j)
    nadir j .commutes = lims.commutes (lift tt)

    module Cone
      {x : C/o.Ob}
      (eta : (j : J.Ob) β†’ C/o.Hom x (F .Fβ‚€ j))
      (p : βˆ€ {i j : J.Ob} β†’ (f : J.Hom i j) β†’ F .F₁ f C/o.∘ eta i ≑ eta j)
      where

        Ο• : (j : J.Ob ⊎ ⊀) β†’ C.Hom (x .domain) (F' .Fβ‚€ j)
        Ο• (inl j) = eta j .map
        Ο• (inr _) = x .map

        Ο•-commutes
          : βˆ€ {i j : J.Ob ⊎ ⊀}
          β†’ (f : ⋆Hom J ⊀Cat i j)
          β†’ F' .F₁ f C.∘ Ο• i ≑ Ο• j
        Ο•-commutes {inl i} {inl j} (lift f) = ap map (p f)
        Ο•-commutes {inl i} {inr j} (lift f) = eta i .commutes
        Ο•-commutes {inr i} {inr x} (lift f) = C.idl _

        Ο•-factor
          : βˆ€ (other : /-Hom x apex)
          β†’ (βˆ€ j β†’ nadir j C/o.∘ other ≑ eta j)
          β†’ (j : J.Ob ⊎ ⊀)
          β†’ lims.ψ j C.∘ other .map ≑ Ο• j
        Ο•-factor other q (inl j) = ap map (q j)
        Ο•-factor other q (inr tt) = other .commutes

    lim : make-is-limit F apex
    lim .ψ = nadir
    lim .commutes f = ext (lims.commutes (lift f))
    lim .universal {x} eta p .map =
      lims.universal (Cone.Ο• eta p) (Cone.Ο•-commutes eta p)
    lim .universal eta p .commutes =
      lims.factors _ _
    lim .factors eta p = ext (lims.factors _ _)
    lim .unique eta p other q = ext $
      lims.unique _ _ (other .map) (Cone.Ο•-factor eta p other q)

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

is-complete→slice-is-complete
  : βˆ€ {β„“ o o' β„“'} {C : Precategory o β„“} {c : ⌞ C ⌟}
  β†’ is-complete o' β„“' C
  β†’ is-complete o' β„“' (Slice C c)
is-complete→slice-is-complete lims F = limit-above→limit-in-slice F (lims _)