module Cat.Instances.Slice where
private variable o β oβ² ββ² : Level open Functor open _=>_ module _ {o β} {C : Precategory o β} where private module C = Cat.Reasoning C variable a b c : C.Ob
Slice categoriesπ
When working in , there is an evident notion of family indexed by a set: a family of sets is equivalently a functor , where we have equipped the set 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 . 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 , then, would consist of an object and a morphism , where is considered as the βtotal spaceβ object and assigns gives the βtagβ of each object. By analysing how pulls back along maps , we recover a notion of βfibresβ: the collection with index can be recovered as the pullback .
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 and object , we have a category of objects indexed by , the slice category . An object of βthe slice over β is given by an object to serve as the domain, and a map .
record /-Obj (c : C.Ob) : Type (o β β) where constructor cut field {domain} : C.Ob map : C.Hom domain c
A map between and is given by a map such that the triangle below commutes. Since weβre thinking of and as families indexed by , commutativity of the triangle says that the map β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
/-Obj-path : β {c} {x y : /-Obj c} β (p : x ./-Obj.domain β‘ y ./-Obj.domain) β PathP (Ξ» i β C.Hom (p i) c) (x ./-Obj.map) (y ./-Obj.map) β x β‘ y /-Obj-path p q i ./-Obj.domain = p i /-Obj-path p q i ./-Obj.map = q i /-Hom-pathp : β {c a aβ² b bβ²} (p : a β‘ aβ²) (q : b β‘ bβ²) {x : /-Hom {c = c} a b} {y : /-Hom aβ² bβ²} β PathP (Ξ» i β C.Hom (p i ./-Obj.domain) (q i ./-Obj.domain)) (x ./-Hom.map) (y ./-Hom.map) β PathP (Ξ» i β /-Hom (p i) (q i)) x y /-Hom-pathp p q {x} {y} r = path where open /-Hom path : PathP (Ξ» i β /-Hom (p i) (q i)) x y path i .map = r i path i .commutes = is-propβpathp (Ξ» i β C.Hom-set (p i ./-Obj.domain) _ (q i ./-Obj.map C.β r i) (p i ./-Obj.map)) (x .commutes) (y .commutes) i /-Hom-path : β {c a b} {x y : /-Hom {c = c} a b} β x ./-Hom.map β‘ y ./-Hom.map β x β‘ y /-Hom-path = /-Hom-pathp refl refl private unquoteDecl eqv = declare-record-iso eqv (quote /-Hom) abstract /-Hom-is-set : β {c a b} β is-set (/-Hom {c = c} a b) /-Hom-is-set {a = a} {b} = hl where abstract open C.HLevel-instance hl : is-set (/-Hom a b) hl = Isoβis-hlevel 2 eqv (hlevel 2)
The slice category 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 , note that if the triangle (the commutativity condition for ) and the rhombus (the commutativity condition for ) both commute, then so does the larger triangle (the commutativity for ).
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 over . First, every slice category has a terminal object, given by the identity map .
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 and is exactly the product of those maps in the slice over .
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 private variable a b : C.Ob f g Οβ Οβ : C.Hom a b open /-Hom open /-Obj
Suppose we have a pullback diagram like the one below, i.e., a limit of the diagram , in the category . Weβll show that itβs also a limit of the (discrete) diagram consisting of and , but now in the slice category .
For starters, note that we have seemingly βtwoβ distinct choices for maps , but since the square above commutes, either one will do. For definiteness, we go with the composite .
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 and in the diagram above extend to maps and in . 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 and in the category , we see that it is exactly the data of the pullback of and in , 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 do not correspond to those in , pullbacks (and equalisers) are precisely equivalent. A square is a pullback in iff. the square consisting of their underlying objects and maps is a square in .
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
may be tested in
,
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 and functor categories into , 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 to the first projection map .
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 and , we recover a natural transformation between and . 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
linv : is-left-inverse (Fβ Total-space) from linv x = /-Hom-path (funext (Ξ» y β Ξ£-path (sym (happly (x .commutes) _)) ( sym (transport-β (ap (β£_β£ β Fβ f2) (happly (x .commutes) y)) (sym (ap (β£_β£ β Fβ f2) (happly (x .commutes) y))) _) Β·Β· apβ transport (β-inv-r (ap (β£_β£ β Fβ f2) (happly (x .commutes) y))) refl Β·Β· transport-refl _)))
For essential surjectivity, given a map , we recover a family of sets by taking the fibre of 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 is a univalent category, then let be some objects, with the pairs and objects in the slice . An isomorphism induces an identification , which extends to an identification since .
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 , 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 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.
module _ {C : Precategory o β} {J : Precategory oβ² ββ²} {o : Precategory.Ob C} (F : Functor J (Slice C o)) where open Terminal open /-Obj open /-Hom private module C = Cat.Reasoning C module J = Cat.Reasoning J module C/o = Cat.Reasoning (Slice C o) module F = Functor F
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 = /-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 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 _)