Double slice is iso to single slice

Question

We are in the following context: let $C$ be a category and $v: x \to y$ an arrow of $C$. Then there is an equivalence of categories $(C/y)/v \simeq C/x$. This is easily proven by hand.

Now, my problem is the following: is there a purely formal way to prove this? For instance, just using the characterisation of the slice as the pullback

$$\require{AMScd} \begin{CD} C/x @>{}>> \mathrm{Fun}(I, C)\\ @VVV @VVV{\mathrm{ev}_1} \\ \ast @>{x}>>C \end{CD}$$

where $I$ is the category with two elements $0$ and $1$ and just one non-trivial map from $0$ to $1$.

Answer 1

People have approached this from a comma category perspective. Another possible approach is that $C_{/y}$ is the category of elements of the Yoneda embedding of $y$. This uses the correspondence between presheaves on $C$ and discrete fibrations over $C$. $\newcommand\hatC{\widehat{C}}$Let $\hatC$ be the presheaf category of $C$.

A discrete fibration $F:C\to D$ is a functor such that squares of the form $$ \begin{CD} * @>>> C \\ @V\iota_1VV @VVFV\\ 2 @>>> D \end{CD} $$ admit unique lifts $2\to C$, where $\iota_1$ is the inclusion of the object $1$ into the category $2 = 0\to 1$.

Let's first workout how this all plays out concretely to get a sense for what's going on.

Concretely:

Then we have the following situation: $x,y\in C$, $v:x\to y$, $$ \require{AMScd} \begin{CD} C_{/x} @>>>C_{/y}\\ @VVV @| \\ (C_{/y})_{/v} @>>> C_{/y} @>>> C \end{CD} $$ We want to show $C_{/x}\to (C_{/y})_{/v}$ is an equivalence of categories. (The map is the obvious one you get by looking at the details, not free from any formal property. We'll see if we can get it formally later.)

Note that $p_x : C_{/x}\to C$, $p_v:(C_{/y})_{/v}\to C_{/v}$, and $p_y:C_{/y}\to C$ are all discrete fibrations of categories and the square above is a commutative square of fibrations over $C$. In particular, the composite $p_y\circ p_v : (C_{/y})_{/v}\to C$ is also a discrete fibration, so it corresponds to a presheaf on $C$. We'll write this presheaf as $(p_y\circ p_v)^{-1}$, since the correspondence between discrete fibrations and presheaves is taking categories of elements in one direction and taking fibers of the fibration in the other direction.

So what is this presheaf? Well, we can just directly compute it. It's values on some object $z$ are commutative triangles $$ \begin{CD} z @>w>> y \\ @VaVV @| \\ x @>v>> y. \end{CD} $$

Then the functor $C_{/x}\to (C_{/y})_{/v}$ gives a map of presheaves $C(-,x)\to (p_y\circ p_v)^{-1}$, which correesponds to an element of $(p_y\circ p_v)^{-1}(x)$, or a commutative triangle $$ \begin{CD} x @>w>> y \\ @VaVV @| \\ x @>v>> y, \end{CD} $$ namely, the triangle given by $w=v$, $a=1_x$ (check where $1_x$ goes under the functor/take this as the definition of our functor).

Then to see concretely that this is a natural isomorphism, we just observe that our commutative triangles are in bijection with the $a:z\to x$ leg.

Formally

To do anything formally you need to first prove the general result that you want to use, so let's do that.

To turn this into something formal we just need to ask if it's possible to compute the presheaf corresponding to a composite of discrete fibrations (assuming one or both of the discrete fibrations are slice categories).

Suppose then that $F$ is a presheaf on $C$ with category of elements $p_F:C_{/F}\to C$ and $G$ is a presheaf on $C_{/F}$ with category of elements $p_G:C_{/F/G}\to C_{/F}$. (I don't think this notation for category of elements is particularly widespread, but it's sensible imo.) The question then is what is the presheaf on $C$ corresponding to $p_F\circ p_G$?

Well, a reasonable guess is that it should probably be a Kan extension of $G$ along $p_F$.

So let's look at what's going on with our Kan extensions. If $X$ is a presheaf on $C$, then we can pull $C_{/X}$ back to $C_{/F}$ to get $$ \begin{CD} C_{/X}\times_C C_{/F} @>>> C_{/X}\\ @VVV @VVp_XV \\ C_{/F} @>p_F>> C,\\ \end{CD} $$ which corresponds to the presheaf $X\circ p_f$ on $C_{/F}$. (Note that I'm identifying $p_F:C_{/F}\to C$ with the corresponding functor $C_{/F}^{\text{op}} \to C^{\text{op}}$.)

Then maps $\alpha: C_{/G} \to C_{/X}$ over $C$ factor through the pullback, and correspond to commutative diagrams $$ \begin{CD} C_{/F/G}@> (\alpha, p_G) >>C_{/X}\times_C C_{/F} @>>> C_{/X}\\ @| @VVV @VVp_XV \\ C_{/F/G}@>p_G >>C_{/F} @>p_F>> C,\\ \end{CD} $$

In other words, we have an adjunction $$\widehat{C_{/F}}(G, X\circ p_F) \simeq \hatC((p_F\circ p_G)^{-1}, X).$$

Or in the language of Kan extensions, $(p_F\circ p_G)^{-1} = \operatorname{Lan}_{p_F} G$.

Finally let's apply the result to give the slice category statement formally (in a sense).

The other key fact we need is that left Kan extensions of representable presheaves are representable. Specifically, for $F: D\to E$, $$\operatorname{Lan}_F D(-,d) = E(-,Fd).$$ To see that this is universal, suppose we had $D(-,d)\to XF$ for some presheaf $X$ on $E$. By Yoneda this corresponds to an element of $XFd$, which corresponds to natural transformation $E(-,Fd)\to X$, as required.

Thus, for any presheaf $F$, we conclude that if $(c,x)\in C_{/F}$, we have that the composite $$C_{/F/(c,x)} \to C_{/F}\to C$$ corresponds to the presheaf $$\operatorname{Lan}_{p_F} C_{/F}(-,(c,x)) \simeq C(-,c).$$ Thus there is an equivalence of categories (over $C$) $$C_{/F/(c,x)} \simeq C_{/c},$$ as desired.

Answer 2

$\require{AMScd}$Yes, there is a more formal approach, but it still requires that you prove the universal property by hand. Recall that the slice $C/y$ can also be described as the comma object

$$ \begin{CD} C/x @>>> C \\ @VVV \Downarrow\alpha_x @| \\ * @>>x> C\end{CD} $$

Given this, you are in the following situation:

$$ \begin{CD} (C/y)/v @>>> C/y \\ @VVV \Downarrow\beta @| \\ * @>>v> C/y \\ @. @VVv^*V\\ @. C/x@>>> C \\ @. @VVV \Downarrow\alpha_x@| \\ @. *@>>x> C \end{CD} $$

the whiskering and composition of these 2-cells defines a natural transformation $\gamma = \alpha_x \cdot v^* \cdot \beta$ ($v^*$ is precomposition with $v$) filling the square

$$ \begin{CD} (C/v)/y @>>> C \\ @VVV \Downarrow\gamma @| \\ * @>>x> C\end{CD} $$

From the universal property of the comma object then you have a unique $(C/y)/v\to C/x$ that can be whiskered with $\alpha_x$. Now proving that it is an equivalence is a matter of unwinding its definition, and for this I guess you need to unravel the same 3-simplex.

Answer 3

One formal approach I like is using the fibered Yoneda lemma. What we need is that fibered functors $C/x\to F$ for $p\colon F\to C$ a fibration (i.e. such that $C/x\to F\to C$ is the domain functor, and such that $C/x\to F$ sends cartesian morphisms to cartesian morhpisms) are the same data as a choice of object $a$ of $p^{-1}(x)$ (image of terminal object of $C/x$) and cartesian lifts of $y\to pa$ for each $y$ in $C$. Moreover such fibered functors are themselves fibrations.

Additionally, we only need the fact every functor $F\to C/x$ such that $F\to C/x\to C$ is the fibration $p\colon F\to C$ is fibered for fibrations over $C$ since every morphism in $C/x$ is cartesian. We can now argue as follows.

First, $C/x\to (C/y)/v$ is the fibered functor (for fibrations over $C$) preserving terminal objects. It is itself a fibration, hence composed with $(C/y)/v\to C/y$ gives a fibration over $C/y$. Then $C/x\to(C/y)/v$ is also fibered for fibrations over $C/y$.

Likewise, $(C/y)/v\to C/x$ is the fibered functor (for fibrations over $C/y$ and also over $C$) preserving terminal objects. Consequently, the composites of the two functors are fibered functors (for fibrations over $C$ and over $C/y$ respectively) from $C/x$ to itself and respectively from $(C/y)/v$ to itself. Morever, both preserve terminal objects, so by the fibered Yoneda lemma are determined by a choice of cartesian lifts. However, by definition of the representable fibrations, i.e. slice categories, cartesian lifts are unique, so the resulting composite functors are the identity functors.

---

Regarding the formal approach using the univeral properties of slice objects, I'm inclined to say the answer is no because the $2$-universal property of a slice object, or more generally comma object, asserts that certain comparison functors are equivalences (or isomorphisms in the case of a strict comma object). However, the targets of those functors are themselves slice categories, or more generally comma categories.

Consequently, the by-hand proof of $(C/y)/v\cong C/x$ also gives the formal result for slice objects. In other words, the formal result easily reduced to the by-hand result. The details are below.

---

For concreteness, recall the following construction in the case of categories. Given functors $f_i\colon D_i\to C$ for $i=1$, the objects of the comma category $f_1/f_2$ are triples consisting of an object $d_1$ of $D_1$, an object $d_2$ of $D_2$, and a morphism $f_1(d_1)\to f_2(d_2)$ of $C$. A morphism of $f_1/f_2$ from $f_1(d_1)\to f_2(d_2)$ to $f_1(d'_1)\to f_2(d'_2)$ is a pair of morphisms $d_i\to d'_i$ so that the composite $f(d_1)\to f_2(d_2)\to f_2(d'_2)$ equals the composite $f(d_1)\to f(d'_1)\to f(d'_2)$.

The particular case of the slice category is where $f_1=\mathrm{id}_C\colon C\to C$, and $f_2=x\colon *\to C$ where $*$ is the $1$-object category.

The $2$-categorical structure of the slice category consists of a pair of $1$-morphisms $\pi_i\colon f_1/f_2\to D_i$ and a $2$-morphism $\alpha_{f/g}\colon f_1\pi_1\Rightarrow f_2\pi_2\colon f_1/f_2\to C$.

What the $2$-universal property asserts is that the comparison functor from the category $[E,f_1/f_2]$ (of $1$-morpihsms $E\to f_1/f_2$ and $2$-morphisms between them) to the slice category is $[E,f_1]/[E,f_2]$ of the functors $[E,f_i]\colon [E,D_i]\to[E,C]$ is an equivalence of categories (an isomorphism if the comma object is strict). Explicitly, this comparison functor arises from the functors $[E,\pi_i]\colon[E,f_1/f_2]\to[E,D_i]$ and natural transformation $[E,\alpha]\colon [E,f_1][E,\pi_1]\Rightarrow[E,f_2][E,\pi_2]\colon[E,f_1/f_2]\to[E,C]$.

Note that if $D_2=*$ is a terminal object, then $[E,*]$ is a one-object category, so the resulting comma category $[E,f_1]/[E,f_2]$ is indeed a slice category. Thus we would have an isomorphism $([E,C]/[E,y])/[E,v]\cong[E,C]/[E,x]$ from the isomorphism $(C/y)/v\cong C/x$ in the case of categories.

Spelled out in detail, an object in $(C/y)/v$ is a morphism in $C/y$ to $v\colon x\to y$ as an object of $C/y$, which is a morphism $z\to y$ equpped with a factorization $z\to x\to y$ through $v\colon x\to y$. Evidently, the factorization $z\to x$ suffices to determine the object, whence we have a bijection on objects from $(C/y)/v$ to $C/x$.

A morphism is simply a morphism $z_1\to z_2$ such that $z_1\to y$ facotrs as $z_1\to z_2\to y$, which is the same data as a morphism $z_1\to z_2$ such that $z_1\to x$ factors as $z_1\to z_2\to x$. Thus we have a bijection on morphisms as well.

Plugging in either the slice object $(C/y)/v$ or $C/x$ for $E$ allow us to transport its identity $1$-morphism along the equivalences (isomorphism) $[C/\dots,C/\dots]\to[C/\dots..,C]/\dots$ and the isomorphism $([C/\dots,C]/[C/\dots,y])/[C/\dots,v]\cong[C/\dots,C]/[C/\dots,x]$ to obtain its structure as the other slice object.

---