Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: uniqueness of Cartesian maps

Olli (Apr 19 2021 at 19:39):

I am having trouble the very first exercise of the book Categorical Logic and Type Theory:

Prove: Cartesian liftings are unique up-to-isomorphism (in a slice): if $f$ and $f'$ with $cod(f) = cod(f')$ are both Cartesian over the same map, then there is a unique vertical isomorphism $\phi: X \simeq X'$ with $f' \circ \phi = f$.

So let $p : \mathbb{E} \to \mathbb{B}$ be a functor. To say that $f : X \to Y, f' : X' \to Y$ in $\mathbb{E}$ are both Cartesian over $u: \mathbb{B}(I,J)$ means that if:

$pf = pf' = u$ and $\forall g : \mathbb{E}(Z,Y), \forall w : \mathbb{B}(pZ, I)$ such that $pg = u \circ w$

then there exist uniquely determined maps $h: Z \to X, h': Z \to X'$ in $\mathbb{B}$ such that $ph = ph' = w$ and $f \circ h = g, f' \circ h' = g$

image.png

I don't know where to begin, so I specialize to the case where $p$ is the codomain fibration $cod : Set^{\to} \to Set$, and now I can think about how everything works inside $Set$:

image.png

The UP of Cartesian morphisms gives me two pullbacks over the same cospan $I \to J \leftarrow Y$ and pullbacks are unique up to isomorphism so this works.

So then this should also work for $cod : \mathbb{B}^{\to} \to \mathbb{B}$ assuming $\mathbb{B}$ has pullbacks, because I can again flatten things down to the base category and work there. Now the proposition mentions Cartesian liftings are unique up-to-isomorphism (in a slice).

Does this mean that just from knowing that a map is Cartesian means that the fibers of the functor are always in slice categories, in which case this same strategy should always work? I don't see how this follows just from the definition of a Cartesian map, although all the examples I have seen so far in the book do fit this pattern.

Matteo Capucci (he/him) (Apr 19 2021 at 21:31):

A cartesian lift is unique only once its codomain is fixed, and by unique we mean unique up to unique iso. But iso... in which category? In the slice of $\mathbb E$ over the chosen codomain. I believe this is what Jacobs means here, not that every fibration has slices as fibers :)
This is a general pattern in UP: the objects are determined by unique isomorphism but that iso is in a specific category, e.g. co/limits are determined up to unique iso of co/cones. Which category one has to look at is usually something one can infer from the rest of the definition, so hardly explicitly mentioned as here.

Matteo Capucci (he/him) (Apr 19 2021 at 21:33):

Re the specific exercise: the general tactic to prove such things is to pit the two UP of $f$ and $f'$ against each other, leveraging uniqueness to show that the two universal arrows you get are necessarily inverse to each other.

Matteo Capucci (he/him) (Apr 19 2021 at 21:34):

I'll leave it to you from here. If you want more hints/a detailed solution just ask.

Olli (Apr 20 2021 at 11:21):

Thanks for the reply. Think I need to spend a bit more time thinking about this, but I won't ask for any more hints for now.

Olli (Apr 21 2021 at 17:34):

I have a question about the term "lift".

As I understand, a regular lift is connecting a cospan into a commuting triangle, so for example if the result is $g = f \circ h$ then we say the lift is of $g$ along $h$ to $f$.

Are cartesian lifts a version of a lift as described here? I am confused because going with the names in my diagram, the terminology in the book says that a cartesian morphism $f : X \to Y$ is a cartesian lifting of $u$, but this doesn't look like the regular lift.

For consistency it seems it would be more appropriate to say that we are lifting $g$ along $w$ or I could even understand lifting $w$ "up" to $\mathbb{E}$, but not "of $u$ to $f$" because $u$ is just the image of $f$ under $p$. This is consistent with the book, but why are we calling lifting of $u$ to $Y$ as $f$ (translating "$f$ to $e$" from nLab to "$u$ to $Y$" with the names I used)?

Is the codomain of the lift the object $Y$ in my diagram? I think your hint is saying that the lift of $u$ is unique as it exists as an object of $\mathbb{E}/Y$? I still don't see how to get the proof from this right away, but it took me a while to clear my confusion about the lifting issue first, so it might be not that far from reach, assuming this is all correct now.

Reid Barton (Apr 21 2021 at 17:59):

It is also a lift, but at a higher level: lifting a functor between categories, rather than a morphism within a category.

Reid Barton (Apr 21 2021 at 18:02):

Putting aside the fibration condition, let's say $p : C \to D$ is any functor. There's a category called $[1]$ which consists of two objects $0$ and $1$ and a single nonidentity morphism $0 \to 1$. Giving a functor from $[1]$ to $D$ is the same as giving a morphism of $D$, namely, the image of the nonidentity morphism of $[1]$. So, we can identify a morphism $u$ of $D$ with a functor $u : [1] \to D$. Then finding a morphism $f$ of $C$ with $p(f) = u$ is the same as lifting $u : [1] \to D$ to a functor $f : [1] \to C$.

Olli (Apr 22 2021 at 07:45):

Think I need another hint

Olli (Apr 22 2021 at 16:24):

Actually I think this should work

Olli (Apr 22 2021 at 16:24):

20210422_232323.jpg

John Baez (Apr 22 2021 at 17:23):

That looks good! Whenever you have two things with a universal property you play them off against each other in this general way and show they're isomorphic. I always tell the story of the two cowboys who both claim to be the fastest gun in the West. To settle who is best they fight a duel. And if they both win, they're isomorphic!

Olli (Apr 22 2021 at 17:50):

Yeah it should have been more obvious after @Matteo Capucci (he/him) 's hint but I had to first work out a simpler example of this with pullbacks before it properly clicked what I was supposed to do