module Cat.Instances.Slice where

Slice categoriesπŸ”—

When working in Sets\mathbf{Sets}, there is an evident notion of family indexed by a set: a family of sets (Fi)i∈I(F_i)_{i \in I} is equivalently a functor [Disc(I),Sets][\mathrm{Disc}(I), \mathbf{Sets}], where we have equipped the set II with the discrete category structure. This works essentially because of the discrete category-global sections adjunction, but in general this can not be applied to other categories, like Groups\mathrm{Groups}. How, then, should we work with β€œindexed families” in general categories?

The answer is to consider, rather than families themselves, the projections from their total spaces as the primitive objects. A family indexed by II, then, would consist of an object AA and a morphism t:Aβ†’It : A \to I, where AA is considered as the β€œtotal space” object and tt assigns gives the β€œtag” of each object. By analysing how tt pulls back along maps Bβ†’IB \to I, we recover a notion of β€œfibres”: the collection with index ii can be recovered as the pullback tβˆ—it^*i.

Note that, since the discussion in the preceding paragraph made no mention of the category of sets, it applies in any category! More generally, for any category C\mathcal{C} and object c:Cc : \mathcal{C}, we have a category of objects indexed by cc, the slice category C/c\mathcal{C}/c. An object of β€œthe slice over cc” is given by an object d:Cd : \mathcal{C} to serve as the domain, and a map f:dβ†’cf : d \to c.

  record /-Obj (c : C.Ob) : Type (o βŠ” β„“) where
    constructor cut
    field
      {domain} : C.Ob
      map      : C.Hom domain c

A map between f:aβ†’cf : a \to c and g:bβ†’cg : b \to c is given by a map h:aβ†’bh : a \to b such that the triangle below commutes. Since we’re thinking of ff and gg as families indexed by cc, commutativity of the triangle says that the map hh β€œrespects reindexing”, or less obliquely β€œpreserves fibres”.

  record /-Hom (a b : /-Obj c) : Type β„“ where
    no-eta-equality
    private
      module a = /-Obj a
      module b = /-Obj b
    field
      map      : C.Hom a.domain b.domain
      commutes : b.map C.∘ map ≑ a.map

The slice category C/c\mathcal{C}/c is given by the /-Obj and /-Homs.

Slice : (C : Precategory o β„“) β†’ Precategory.Ob C β†’ Precategory _ _
Slice C c = precat where
  import Cat.Reasoning C as C
  open Precategory
  open /-Hom
  open /-Obj

  precat : Precategory _ _
  precat .Ob = /-Obj {C = C} c
  precat .Hom = /-Hom
  precat .Hom-set x y = /-Hom-is-set
  precat .id .map      = C.id
  precat .id .commutes = C.idr _

For composition in the slice over cc, note that if the triangle (the commutativity condition for ff) and the rhombus (the commutativity condition for gg) both commute, then so does the larger triangle (the commutativity for g∘fg \circ f).

  precat ._∘_ {x} {y} {z} f g = fog where
    module f = /-Hom f
    module g = /-Hom g
    fog : /-Hom _ _
    fog .map = f.map C.∘ g.map
    fog .commutes =
      z .map C.∘ f.map C.∘ g.map β‰‘βŸ¨ C.pulll f.commutes βŸ©β‰‘
      y .map C.∘ g.map           β‰‘βŸ¨ g.commutes βŸ©β‰‘
      x .map                     ∎
  precat .idr f = /-Hom-path (C.idr _)
  precat .idl f = /-Hom-path (C.idl _)
  precat .assoc f g h = /-Hom-path (C.assoc _ _ _)

LimitsπŸ”—

We discuss some limits in the slice of C\mathcal{C} over cc. First, every slice category has a terminal object, given by the identity map id:c→c\mathrm{id}_{} : c \to c.

module _ {o β„“} {C : Precategory o β„“} {c : Precategory.Ob C} where
  import Cat.Reasoning C as C
  import Cat.Reasoning (Slice C c) as C/c
  open /-Hom
  open /-Obj

  Slice-terminal-object : is-terminal (Slice C c) (cut C.id)
  Slice-terminal-object obj .centre .map = obj .map
  Slice-terminal-object obj .centre .commutes = C.idl _
  Slice-terminal-object obj .paths other =
    /-Hom-path (sym (other .commutes) βˆ™ C.idl _)

Products in a slice category are slightly more complicated, but recall that another word for pullback is β€œfibred product”. Indeed, in the pullback page we noted that the pullback of Xβ†’ZX \to Z and Yβ†’ZY \to Z is exactly the product of those maps in the slice over ZZ.

Suppose we have a pullback diagram like the one below, i.e., a limit of the diagram aβ†’fc←gba \xrightarrow{f} c \xleftarrow{g} b, in the category C\mathcal{C}. We’ll show that it’s also a limit of the (discrete) diagram consisting of ff and gg, but now in the slice category C/c\mathcal{C}/c.

For starters, note that we have seemingly β€œtwo” distinct choices for maps aΓ—cbβ†’ca \times_c b \to c, but since the square above commutes, either one will do. For definiteness, we go with the composite fβˆ˜Ο€1f \circ \pi_1.

  module
    _ {f g : /-Obj c} {Pb : C.Ob} {π₁ : C.Hom Pb (f .domain)}
                                  {Ο€β‚‚ : C.Hom Pb (g .domain)}
      (pb : is-pullback C {X = f .domain} {Z = c} {Y = g .domain} {P = Pb}
        π₁ (map {_} {_} {C} {c} f) Ο€β‚‚ (map {_} {_} {C} {c} g))
    where
    private module pb = is-pullback pb

    is-pullback→product-over : C/c.Ob
    is-pullbackβ†’product-over = cut (f .map C.∘ π₁)

Now, by commutativity of the square, the maps Ο€1\pi_1 and Ο€2\pi_2 in the diagram above extend to maps (fβˆ˜Ο€1)β†’f(f \circ \pi_1) \to f and (fβˆ˜Ο€1)β†’g(f \circ \pi_1) \to g in C/c\mathcal{C}/c. Indeed, note that by scribbling a red line across the diagonal of the diagram, we get the two needed triangles as the induced subdivisions.

    is-pullback→π₁ : C/c.Hom is-pullbackβ†’product-over f
    is-pullback→π₁ .map      = π₁
    is-pullback→π₁ .commutes i = f .map C.∘ π₁

    is-pullback→π₂ : C/c.Hom is-pullback→product-over g
    is-pullback→π₂ .map        = π₂
    is-pullback→π₂ .commutes i = pb.square (~ i)

    open is-product

Unfolding what it means for a diagram to be a universal cone over the discrete diagram consisting of ff and gg in the category C/c\mathcal{C}/c, we see that it is exactly the data of the pullback of ff and gg in C\mathcal{C}, as below:

    is-pullback→is-fibre-product
      : is-product (Slice C c) is-pullback→π₁ is-pullbackβ†’Ο€β‚‚
    is-pullbackβ†’is-fibre-product .⟨_,_⟩ {Q} /f /g = factor
      where
        module f = /-Hom /f
        module g = /-Hom /g

        factor : C/c.Hom Q _
        factor .map = pb.universal (f.commutes βˆ™ sym g.commutes)
        factor .commutes =
          (f .map C.∘ π₁) C.∘ pb.universal _ β‰‘βŸ¨ C.pullr pb.pβ‚βˆ˜universal βŸ©β‰‘
          f .map C.∘ f.map                  β‰‘βŸ¨ f.commutes βŸ©β‰‘
          Q .map                            ∎

    is-pullbackβ†’is-fibre-product .Ο€β‚βˆ˜factor = /-Hom-path pb.pβ‚βˆ˜universal
    is-pullbackβ†’is-fibre-product .Ο€β‚‚βˆ˜factor = /-Hom-path pb.pβ‚‚βˆ˜universal
    is-pullback→is-fibre-product .unique other p q =
      /-Hom-path (pb.unique (ap map p) (ap map q))

  Pullback→Fibre-product
    : βˆ€ {f g : /-Obj c}
    β†’ Pullback C (f .map) (g .map) β†’ Product (Slice C c) f g
  Pullback→Fibre-product pb .Product.apex = _
  Pullbackβ†’Fibre-product pb .Product.π₁ = _
  Pullback→Fibre-product pb .Product.π₂ = _
  Pullback→Fibre-product pb .Product.has-is-product =
    is-pullback→is-fibre-product (pb .Pullback.has-is-pb)

While products and terminal objects in C/X\mathcal{C}/X do not correspond to those in C\mathcal{C}, pullbacks (and equalisers) are precisely equivalent. A square is a pullback in C/X\mathcal{C}/X iff. the square consisting of their underlying objects and maps is a square in C\mathcal{C}.

The β€œif” direction (what is pullback-aboveβ†’pullback-below) in the code is essentially an immediate consequence of the fact that equality of morphisms in C/X\mathcal{C}/X may be tested in C\mathcal{C}, but we do have to take some care when extending the β€œuniversal” morphism back down to the slice category (see the calculation marked {- * -}).

module _ where
  open /-Obj
  open /-Hom

  pullback-above→pullback-below
    : βˆ€ {o β„“} {C : Precategory o β„“} {X : Precategory.Ob C}
    β†’ βˆ€ {P A B c} {p1 f p2 g}
    β†’ is-pullback C (p1 .map) (f .map) (p2 .map) (g .map)
    β†’ is-pullback (Slice C X) {P} {A} {B} {c} p1 f p2 g
  pullback-above→pullback-below {C = C} {P = P} {a} {b} {c} {p1} {f} {p2} {g} pb
    = pbβ€² where
      open is-pullback
      open Cat.Reasoning C

      pbβ€² : is-pullback (Slice _ _) _ _ _ _
      pbβ€² .square = /-Hom-path (pb .square)
      pbβ€² .universal p .map = pb .universal (ap map p)
      pbβ€² .universal {P'} {p₁' = p₁'} p .commutes =
        (c .map ∘ pb .universal (ap map p))           β‰‘Λ˜βŸ¨ (pulll (p1 .commutes)) βŸ©β‰‘Λ˜
        (P .map ∘ p1 .map ∘ pb .universal (ap map p)) β‰‘βŸ¨ ap (_ ∘_) (pb .pβ‚βˆ˜universal) βŸ©β‰‘
        (P .map ∘ p₁' .map)                          β‰‘βŸ¨ p₁' .commutes βŸ©β‰‘
        P' .map                                      ∎ {- * -}
      pbβ€² .pβ‚βˆ˜universal = /-Hom-path (pb .pβ‚βˆ˜universal)
      pbβ€² .pβ‚‚βˆ˜universal = /-Hom-path (pb .pβ‚‚βˆ˜universal)
      pbβ€² .unique p q = /-Hom-path (pb .unique (ap map p) (ap map q))

  pullback-below→pullback-above
    : βˆ€ {o β„“} {C : Precategory o β„“} {X : Precategory.Ob C}
    β†’ βˆ€ {P A B c} {p1 f p2 g}
    β†’ is-pullback (Slice C X) {P} {A} {B} {c} p1 f p2 g
    β†’ is-pullback C (p1 .map) (f .map) (p2 .map) (g .map)
  pullback-below→pullback-above {C = C} {P = P} {p1 = p1} {f} {p2} {g} pb = pb′ where
    open Cat.Reasoning C
    open is-pullback
    pbβ€² : is-pullback _ _ _ _ _
    pbβ€² .square = ap map (pb .square)
    pbβ€² .universal {Pβ€² = P'} {p₁'} {pβ‚‚'} p =
      pb .universal {Pβ€² = cut (P .map ∘ p₁')}
        {p₁' = record { map = p₁' ; commutes = refl }}
        {pβ‚‚' = record { map = pβ‚‚' ; commutes = sym (pulll (g .commutes))
                                             βˆ™ sym (ap (_ ∘_) p)
                                             βˆ™ pulll (f .commutes)
                      }}
        (/-Hom-path p)
        .map
    pbβ€² .pβ‚βˆ˜universal = ap map $ pb .pβ‚βˆ˜universal
    pbβ€² .pβ‚‚βˆ˜universal = ap map $ pb .pβ‚‚βˆ˜universal
    pbβ€² .unique p q = ap map $ pb .unique
      {lim' = record { map = _ ; commutes = sym (pulll (p1 .commutes)) βˆ™ ap (_ ∘_) p }}
      (/-Hom-path p) (/-Hom-path q)

Slices of SetsπŸ”—

We now prove the correspondence between slices of Sets\mathbf{Sets} and functor categories into Sets\mathbf{Sets}, i.e.Β the corresponding between indexing and slicing mentioned in the first paragraph.

module _ {I : Set β„“} where
  open /-Obj
  open /-Hom

We shall prove that the functor Total-space, defined below, is an equivalence of categories, i.e.Β that it is fully faithful and essentially surjective. But first, we must define the functor! Like its name implies, it maps the functor F:Iβ†’SetsF : I β†’ \mathbf{Sets} to the first projection map fst:βˆ‘Fβ†’I\mathrm{fst} : \sum F \to I.

  Total-space : Functor Cat[ Discβ€² I , Sets β„“ ] (Slice (Sets β„“) I)
  Total-space .Fβ‚€ F .domain = el (Ξ£ _ (∣_∣ βŠ™ Fβ‚€ F)) hlevel!
  Total-space .Fβ‚€ F .map = fst

  Total-space .F₁ nt .map (i , x) = i , nt .Ξ· _ x
  Total-space .F₁ nt .commutes    = refl

  Total-space .F-id    = /-Hom-path refl
  Total-space .F-∘ _ _ = /-Hom-path refl

To prove that the Total-space functor is fully faithful, we will exhibit a quasi-inverse to its action on morphisms. Given a fibre-preserving map between fst:βˆ‘Fβ†’I\mathrm{fst} : \sum F \to I and fst:βˆ‘Gβ†’I\mathrm{fst} : \sum G \to I, we recover a natural transformation between FF and GG. The hardest part is showing naturality, where we use path induction.

  Total-space-is-ff : is-fully-faithful Total-space
  Total-space-is-ff {f1} {f2} = is-iso→is-equiv
    (iso from linv (Ξ» x β†’ Nat-path (Ξ» x β†’ funext (Ξ» _ β†’ transport-refl _))))
    where
      from : /-Hom (Total-space .Fβ‚€ f1) (Total-space .Fβ‚€ f2) β†’ f1 => f2
      from mp = nt where
        eta : βˆ€ i β†’ ∣ Fβ‚€ f1 i ∣ β†’ ∣ Fβ‚€ f2 i ∣
        eta i j =
          subst (∣_∣ βŠ™ Fβ‚€ f2) (happly (mp .commutes) _) (mp .map (i , j) .snd)

        nt : f1 => f2
        nt .Ξ· = eta
        nt .is-natural _ _ f =
          J (Ξ» _ p β†’ eta _ βŠ™ F₁ f1 p ≑ F₁ f2 p βŠ™ eta _)
            (ap (eta _ βŠ™_) (F-id f1) βˆ™ sym (ap (_βŠ™ eta _) (F-id f2)))
            f

For essential surjectivity, given a map f:Xβ†’If : X \to I, we recover a family of sets (fβˆ—i)i∈I(f^*i)_{i \in I} by taking the fibre of ff over each point, which cleanly extends to a functor. To show that the Total-space of this functor is isomorphic to the map we started with, we use one of the auxiliary lemmas used in the construction of an object classifier: Total-equiv. This is cleaner than exhibiting an isomorphism directly, though it does involve an appeal to univalence.

  Total-space-is-eso : is-split-eso Total-space
  Total-space-is-eso fam = functor , path→iso path
    where
      functor : Functor _ _
      functor .Fβ‚€ i = el! (fibre (fam .map) i)
      functor .F₁ p = subst (fibre (fam .map)) p
      functor .F-id = funext transport-refl
      functor .F-∘ f g = funext (subst-βˆ™ (fibre (fam .map)) _ _)

      path : Fβ‚€ Total-space functor ≑ fam
      path = /-Obj-path (n-ua (Total-equiv _  e⁻¹)) (uaβ†’ Ξ» a β†’ sym (a .snd .snd))

Slices preserve univalenceπŸ”—

An important property of slice categories is that they preserve univalence. This can be seen intuitively: If C\mathcal{C} is a univalent category, then let a,b,ca, b, c be some objects, with the pairs (a,f)(a, f) and (b,g)(b, g) objects in the slice C/c\mathcal{C}/c. An isomorphism h:(a,f)β‰…(b,g)h : (a, f) \cong (b, g) induces an identification a≑ba \equiv b, which extends to an identification (a,f)≑(b,g)(a, f) \equiv (b, g) since h∘g=fh \circ g = f.

module _ {C : Precategory o β„“} {o : Precategory.Ob C} (isc : is-category C) where
  private
    module C   = Cat.Reasoning C
    module C/o = Cat.Reasoning (Slice C o)

    open /-Obj
    open /-Hom
    open C/o._β‰…_
    open C._β‰…_

  slice-is-category : is-category (Slice C o)
  slice-is-category .to-path x = /-Obj-path (isc .to-path $
    C.make-iso (x .to .map) (x .from .map)
      (ap map (C/o._β‰…_.invl x)) (ap map (C/o._β‰…_.invr x)))
    (Univalent.Hom-pathp-refll-iso isc (x .from .commutes))
  slice-is-category .to-path-over x = C/o.β‰…-pathp refl _ $
    /-Hom-pathp _ _ (Univalent.Hom-pathp-reflr-iso isc (C.idr _))

Arbitrary limits in slicesπŸ”—

Suppose we have some really weird diagram F:Jβ†’C/cF : \mathcal{J} \to \mathcal{C}/c, 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 it.

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 (a,f)(a, f) and (b,g)(b, g), we had to pass to a pullback of aβ†’fc←ba \xrightarrow{f} c \xleftarrow{b} in C\mathcal{C} β€” which we had assumed exists. But! Take a look at what that diagram looks like:

We β€œexploded” a diagram of shape βˆ™βˆ™\bullet \quad \bullet to one of shape βˆ™β†’βˆ™β†βˆ™\bullet \to \bullet \leftarrow \bullet. This process can be described in a way easier to generalise: We β€œexploded” our diagram F:{βˆ—,βˆ—}β†’C/cF : \{*,*\} \to \mathcal{C}/c 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 F:Jβ†’C/cF : J \to \mathcal{C}/c, we can β€œexplode” this into a diagram Fβ€²:(J⋆{βˆ—})β†’CF' : (J \star \{*\}) \to \mathcal{C}, compute the limit in C\mathcal{C}, 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 =
      /-Hom-path (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 =
      /-Hom-path (lims.factors _ _)
    lim .unique eta p other q =
      /-Hom-path $ lims.unique _ _ (other .map) (Cone.Ο•-factor eta p other q)

In particular, if a category C\mathcal{C} is complete, then so are its slices:

is-complete→slice-is-complete
  : βˆ€ {β„“ o β„“β€²} {C : Precategory o β„“} {c : Precategory.Ob 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 _)