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: What is a fibration?

Ignat Insarov (May 07 2023 at 14:08):

So, I wanted to understand categorial models of dependent types, and I went like [[categorical semantics of dependent type theory]] → [[bundle]] → [[codomain fibration]] → [[Grothendieck fibration]], at which point I found hardship going forward.

I think I understand the concrete example where we have the functors $\text{target}: ℂ^I → ℂ$ and $\text{slice}: ℂ → \textbf{categories} = (ℂ↓–)$. It seems to say that the category of arrows and equations (commuting squares) of $ℂ$ is a fiber bundle of slice categories $(ℂ↓–)$ over the base category $ℂ$. For every object $c ∈ ℂ$ we can take the pullback of the functor $c: 1 → ℂ$ along the fibration $\text{target}$ to get the category $ℂ^I_c = (ℂ↓c)$.

I technically understand the definition of [[Grothendieck fibration]]#definition but I do not understand why it is needed.

• What is a Cartesian arrow good for?
• What are Cartesian arrows practically?
• What do they have to do with Renatus Cartesius?
• Does this stuff have any relation to homotopy lifting properties and Hurewicz fibrations?
• Given a fibration $p: E → B$, is a Cartesian arrow a universal arrow to the functor $p$ in the sense of Saunders Mac Lane?

I cannot understand the definition of the functor described at [[Grothendieck+fibration]]#fibrations_versus_pseudofunctors. They say:

To obtain the action on morphisms, given an $f:a→b$ in $B$ and an object $e∈E_b$, we choose a cartesian arrow $ϕ:e′→e$ over $f$ and call its source $f^*(e)$.

This does not makes sense. What is a Cartesian arrow over $f$? The definition of a Cartesian arrow requires two premises: an object $e$ in the total category $E$ and an arrow $f: b → e$ in the base category $B$. They only name an arrow — this is not enough to apply the definition of a Cartesian arrow. I tried to guess what they want me to do but nothing works.

They later go on to say that $\text{target}$ is indeed a fibration and its Cartesian arrows are pullbacks, but by then I am so lost this statement, that must have been easy and illuminating, goes altogether over my head. What makes pullbacks Cartesian arrows?

David Egolf (May 07 2023 at 15:21):

I would like to learn some of these things as well! I wonder if chapter 1 of "Categorical Logic and Type Theory" by Jacobs might be a helpful reference for clarifying what the nLab is saying. For example, it introduces and discusses Cartesian morphisms.

The first chapter of Jacobs starts out like this:
start of Jacobs chapter 1

And regarding the name "Cartesian arrow", there is some discussion here you might find helpful.

David Egolf (May 07 2023 at 16:14):

Regarding a connection between pullbacks and Cartesian arrows, this at least seems closely related (following Jacobs page 25):
(I don't know if you'll find any of this useful. But I'll post it just in case!)

In the category of sets, a pullback is a morphism in the arrow category $\mathsf{Arr(Set)}$:
pullback

This pullback square describes a morphism $(f,u)$ from $\varphi: X \to I$ to $\psi: Y \to J$.

We can then ask, given another object $\chi: Z \to K$ and a morphism from it to $\psi: Y \to J$ as follows
other morphism

where $w$ is such so that $v = u \circ w$, can we "complete" the square on the left uniquely with some $h: Z \to X$ to obtain a unique morphism from $\chi: Z \to K$ to $\varphi: X \to I$, so that we get the morphism $(g,v)$ by composition of $(f,u)$ after $(h,w)$? This is related to starting with the 2/3 of a triangle (a "horn"?) defined by $u$ and $v$, and if we can complete it to a commutative triangle with some $w$, then we want to know if we can uniquely "lift" that whole resulting commutative triangle up to the commutative triangle $g = f \circ h$. That starts to sound reminiscent of the definition of a Cartesian arrow, I think.

In this case, we can find such a unique $h$, I think using the fact that the square on the right is a pullback square.

John Baez (May 07 2023 at 17:37):

The usual definition of fibration is technical and scary, so I think it's important to start by learning a bunch of examples of fibrations that let you see what this concept is good for. The examples that work for you will depend on who you are.

John Baez (May 07 2023 at 17:39):

For example, I find it easy to visualize graphs (in the category theorist's sense, also called [[quivers]] and the forgetful functor from graphs to sets, which forgets the edges and remembers only the set of vertices. This is both a fibration and an opfibration.

John Baez (May 07 2023 at 17:39):

Because this functor $U : \mathsf{Grph} \to \mathsf{Set}$ is a fibration, we get this:

John Baez (May 07 2023 at 17:40):

Suppose I have a function between sets $f: S \to T$ and a way to make $T$ into the vertices of a graph: $T = U(G)$.

John Baez (May 07 2023 at 17:40):

Then there's a god-given best way to make $S$ into the vertices of a graph!

John Baez (May 07 2023 at 17:42):

You can guess what this best way is. Then you can think about why it's "best", while staring at the definition of Grothendick fibration... and you'll see that the definition captures how this way is the "best".

John Baez (May 07 2023 at 17:46):

This is how I managed to first understand the definition of Grothendieck fibration. Then I learned about other examples from logic, and topology, and algebra, and they reinforced my understanding.

John Baez (May 07 2023 at 17:48):

For me, it was hopeless to understand fibrations by only thinking about the definition without the help of any examples.

Evan Patterson (May 07 2023 at 19:49):

Nice example! It's closely related to the example that helped me understand (a little bit about) fibrations: the fibration that defines an equipment. In the case of the equipment of spans, there is a forgetful functor $\mathsf{Span} \to \mathsf{Set}^2$ that sends a span to its pair of feet. (Here $\mathsf{Span}$ is the copresheaf category on the walking span $\{\bullet \leftarrow \bullet \rightarrow \bullet\}$, not some higher-dimensional structure.)

This functor is a fibration. It generalizes the example of graphs if we think that a graph is an "endospan".

John Baez (May 07 2023 at 20:13):

So yeah, the basic moral here is: you get a fibration when you have a functor $U: D \to C$ that "forgets extra structure", turning objects of $D$ into their underlying $C$-objects, and - here's the key point - a god-given best way to pull back tha extra structure, so if you have extra structure on $c' \in C$ and a morphism $f: c \to c'$, you can get extra structure on $c$.

John Baez (May 07 2023 at 20:15):

(And although I said "structure" above, it's actually typical in examples for $U$ to be forgetting extra stuff, in the technical sense of "stuff". That is, $U$ is often not faithful. It's not in the two examples we've just looked at. The edges of a graph are extra stuff, when we use the category theorists' definition of "graph". In other words, what a graph morphism does to the vertices does not determine what it does to the edges.)

Josselin Poiret (May 08 2023 at 13:44):

Conceptually, from the point of view of type theory, I think it can be helpful to understand a grothendieck fibration $E → B$ as a dependent type $B^{op} \vdash E$ where your types are synthetic categories (ie. directed 1-types). Now, in the case that the fibers are small enough, the grothendieck construction tells you exactly that dependent types $B^{op} \vdash E$ correspond exactly to pseudofunctors $B^{op} → Cat$, the latter being the universe of suitably small categories. Now, the dependent directed 1-types can be seen as an apparatus where types over the base have some directed transport structure, ie. an arrow in the base category lets you transport things in the fibers over the arrow.

Josselin Poiret (May 08 2023 at 13:49):

in that sense it looks a lot like a fibration, in that fibrations can be seen as "dependent types with extra operations on it from the base". However the definition as-is doesn't really correspond to a right class of a WFS on $Cat$, but you could argue that this is because this is a 2-category of things with a quite complex structure, and that one should instead investigate a 1-categorical presentation of it... I'm no specialist of those questions though, so I'd appreciate input from people who may have thought about that last part more

Josselin Poiret (May 08 2023 at 15:27):

to expand a bit on the above, I can give you some type-theoretic-flavored examples: the type $c : C \vdash \Sigma (d : C) Hom(d, c)$ is the codomain opfibration $C^\to \to C$ that was mentioned above, which can be made into a fibration if the category has all pullbacks (ie. to get the contravariant $C$-action). The fibration $c : C \vdash Hom(c, a)$, the "directed identity type with a fixed endpoint", is actually $C/a → C$, which under the grothendieck construction corresponds to the presheaf $y(a)$.

Josselin Poiret (May 08 2023 at 15:38):

note though that if you're familiar with HoTT, being a Grothendieck fibration is actually the propositional truncation of the structure of cleavage, a cleavage being a choice of cartesian lifts!

John Baez (May 08 2023 at 16:27):

This type-theoretic explanation of Grothendieck fibrations is helpful for people who feel comfortable with "dependent types". I was giving an explanation aimed at being helpful to people who feel comfortable with graphs and how a graph can seen as a set of vertices together with extra stuff. There would be another explanation helpful for people who feel comfortable with rings and their modules - this is close to Grothendieck's original application of fibrations. And also other explanations, I'm sure. So the people who asked the original question should tell us which explanation they want to dive into!

Josselin Poiret (May 08 2023 at 17:09):

Since OP wanted to know about categorical models of dependent types, I thought this would be an approach they could be familiar with, but there are definitely a lot of ways of looking at grothendieck fibrations (and fibrations in general!)

Josselin Poiret (May 08 2023 at 17:10):

(although I would argue that the dependent types one is the "right" as in most general view, but now that's just my personal opinion :p)

Ignat Insarov (May 08 2023 at 17:17):

Thank you @David Egolf @John Baez @Evan Patterson @Josselin Poiret for your fantastic suggestions! This is enough homework to keep me busy for a while!

David Egolf (May 08 2023 at 17:55):

John Baez said:

Suppose I have a function between sets $f: S \to T$ and a way to make $T$ into the vertices of a graph: $T = U(G)$.

Then there's a god-given best way to make $S$ into the vertices of a graph!

Let $\ell(S)$ be the "best" graph that has $S$ as its vertices. It has $|S|$ vertices, and so it remains to figure out what its edges should be.

I don't know if this is the "best" way, but this is what comes to mind. If there is an edge $e: a \to b$ in $G$, then for each $(a',b')$ in $S$ so that $f(a')=a$ and $f(b') = b$, add in an edge in $\ell(S)$ from $a'$ to $b'$.

I'm not sure how this relates to more general ideas just yet, though.

David Egolf (May 08 2023 at 19:39):

I'm thinking about how we can induce edges in $\ell(S)$ from edges in $G$. Let $2$ denote the graph with vertices $v_1$ and $v_2$ with an edge from $v_1$ to $v_2$. Then, a graph homorphism from $2$ to $G$ specifies an edge of $G$. So, given a morphism $e: 2 \to G$, we would like to find a morphism $e': 2 \to \ell(S)$, using the fact that we have a morphism $f: S \to T$ where $T = U(G)$.

One way to induce such a morphism would be by composition. If we could find some morphism $h$ from $G$ to $\ell(S)$ compatible in an appropriate way with $f$, then we could try setting $e' = h \circ e$. However, we don't have such a morphism, and the morphism we do have $f: S \to T$ runs in the opposite direction.

David Egolf (May 08 2023 at 19:39):

We might want a different way to induce a morphism $e': 2 \to \ell(S)$ from a morphism $e: 2 \to G$, then. Imagine that we have some way of "lifting" our function $f: S \to T$ to a graph homomorphism $\ell(f): \ell(S) \to G$, so that $U(\ell(f)) = f$. We can ask about which morphisms $e': 2 \to \ell(S)$ make the resulting diagram with $e$ and $\ell(f)$ commute, so $\ell(f) \circ e' = e$. Asking this diagram to commute involves requiring $e'$ to pick out an edge in $\ell(S)$ that is in the preimage of $e$ in $G$ under the mapping $\ell(f)$. So, for each edge $e$ in $G$, we induce up to several "analogous" edges in $\ell(S)$.

There can indeed be multiple of these edges $e'$ so that $\ell(f) \circ e' = e$. This can happen because $f$ may map multiple elements of $S$ to the same element of $T$. There is a second analogous diagram in the category of sets relating to this: we have a function $f: S \to T$ and a function $U(e): U(2) \to T$. A function $g: U(2) \to S$ so that $f \circ g = U(e)$ corresponds to a choice of an ordered pair of vertices in $S$ so that the chosen pair lands on the ordered pair of vertices in $T$ corresponding to the edge $e'$. Again, there can be multiple such functions $g$, with each choice for $g$ specifying a single pair of vertices in $S$.

Once we pick a specific ordered pair of vertices in $S$ that map onto the edge $e$, then we hope that this will induce a unique edge $e'$ in $\ell(S)$. That is, once we pick a $g$ so that $f \circ g = U(e')$, we hope there is a unique $e': 2 \to \ell(S)$ so that $\ell(f) \circ e' = e$. This edge connects the ordered pair of vertices selected by $g$, I think.

We can then repeat this process of choosing $e: 2 \to G$ and choosing $g: U(2) \to S$ to get all the edges of $\ell(S)$, I think.

I tried to imitate above the definition of a Cartesian arrow. If $\ell(f)$ is a Cartesian arrow with $U(\ell(f))=f$, then I think we are ensured that the process described above does indeed induce a unique $e'$ from each choice for $e$ and $g$. And if $U$ is a fibration, then I think we are ensured that there is indeed a Cartesian $\ell(f)$ so that $U(\ell(f)) = f$.

David Egolf (May 08 2023 at 19:57):

So, how can we determine $\ell(S)$? I think each allowed choice - so the appropriate diagram commutes, as discussed above - of $g: U(2) \to S$ gives us an edge of $\ell(S)$. (Without checking carefully, I suspect this results in the approach I described in my first post above.) And this really induces a unique edge of the graph $\ell(S)$ compatible with $f$ because there exists a Cartesian $\ell(f)$ with $U(\ell(f)) = f$. Presumably we then take $\ell(S)$ to be the graph with all the edges that can be induced in this way.

Although, I suppose this only describes a unique graph $\ell(S)$ for a given choice of $\ell(f)$. I don't know if there can be multiple such $\ell(f)$.

John Baez (May 08 2023 at 21:27):

David Egolf said:

John Baez said:

Suppose I have a function between sets $f: S \to T$ and a way to make $T$ into the vertices of a graph: $T = U(G)$.

Then there's a god-given best way to make $S$ into the vertices of a graph!

Let $\ell(S)$ be the "best" graph that has $S$ as its vertices. It has $|S|$ vertices, and so it remains to figure out what its edges should be.

I don't know if this is the "best" way, but this is what comes to mind. If there is an edge $e: a \to b$ in $G$, then for each $(a',b')$ in $S$ so that $f(a')=a$ and $f(b') = b$, add in an edge in $\ell(S)$ from $a'$ to $b'$.

Yes, that's the best way.

John Baez (May 08 2023 at 21:34):

I didn't follow all your further comments, but to make precise one sense in which it's the "best" way, you can show that this method exhibits the forgetful functor $U : \mathsf{Grph} \to \mathsf{Set}$ as a fibration.

John Baez (May 08 2023 at 21:35):

What you're doing is taking a morphism $f: S \to T$ and a graph $G$ with $U(G) = T$, and finding a graph, say $F$, with $U(F) = S$.

John Baez (May 08 2023 at 21:36):

But you're doing more, because this graph $F$ comes with a map of graphs, say $\tilde{f} : F \to G$ which "lifts" the morphism $f: S \to T$. That's jargon for

$U(\tilde{f}) = f$

John Baez (May 08 2023 at 21:39):

And it's not just any old lift: it's a cartesian lift! That is, it has a universal property which is described here: [[cartesian morphism]].

John Baez (May 08 2023 at 21:40):

The fact that every morphism in $\mathsf{Set}$ has a cartesian lift is what makes $U : \mathsf{Grph} \to \mathsf{Set}$ a Grothendieck fibration.

John Baez (May 08 2023 at 21:41):

I'm too lazy to work through the definition of "cartesian morphism" in this example and check that $\tilde{f}$ is a cartesian morphism, mainly because it's tiring to draw diagrams here on Zulip. But this is a good thing to do. (Maybe you've already done it.)

David Egolf (May 08 2023 at 21:53):

That's making sense, and it's sounding familiar after I typed out the stuff above!
(If there are any comments I made above you would like me to clarify, I'd be happy to do so. Basically, I was trying to use the existence of a Cartesian arrow $\tilde{f}$ to figure out the edges in $F$.)

I did not show that some particular $\tilde{f}$ is a Cartesian morphism, though.

I was wondering if there could be more than one Cartesian lift of $f$ in the case of this example - probably not? Anyways, I feel like I've learned a lot about this stuff, and I'm happy with that for now!

John Baez (May 09 2023 at 00:29):

As usual with things defined by universal properties, there will be multiple Cartesian lifts, but they will all be isomorphic. You defined the set of edges in your graph $F$ in a reasonable way, but I could have chosen an isomorphic set of edges and used that!

Claudio Pisani (Jun 16 2023 at 22:45):

I'd like to add some remarks in the spirit of the good example above of graphs as a fibration.

1) Perhaps the simplest example of non-trivial (and non-discrete) fibration is the subset fibration $\bf {Sub} \to \bf{Set}$:
the objects of $\bf {Sub}$ are pairs $(X,A)$, where $X$ is a set and $A\subseteq X$ is a subset of $X$,
while its arrows $(X,A) \to (Y,B)$ are mappings $f:X\to Y$ such that $x\in A$ implies $fx \in B$,
and the functor $\bf {Sub} \to \bf{Set}$ is the obvious one.

Of course this is a both a fibration and an op-fibration via the inverse and direct image of a subset.
From the indexed category point of view, it is simply the subset functor $\bf{Set} \to \bf{Cat}$ given by $X\mapsto {\cal P}(X)$
and it is one of the main instances of Lawvere's hyperdoctrine in his 1969-70 papers.

2) By restricting (i.e. pulling back) $\bf {Sub} \to \bf{Set}$ along the product functor $\times: \bf{Set}\times \bf{Set} \to \bf{Set}$
one gets the fibration of binary relations, and by restricting further along the diagonal $\Delta: \bf{Set} \to \bf{Set}\times \bf{Set}$
one gets the fibration of endorelations.

3) $\bf {Sub} \to \bf{Set}$ may be seen as a restriction (in another sense) of the codomain fibration $\bf{Set}^\to \to \bf{Set}$,
by taking only injective mapping as objects (and quotienting out by the usual equivalence relation).

4) If we start from the codomain fibration itself and restrict it as in 2) we get respectively the fibrations of spans and of graphs
mentioned by Evan and John.

5) Of course all the above can be generalized replacing $\bf Set$ with a category with suitable properties.

6) Another source of fibrations are 2-categories $\cal C$: fixing an object $C\in\cal C$ we get the "representable" indexed category
$X \mapsto {\cal C}(X,C)$ and the accompanying fibration (over the underlying category of $\cal C$)
whose objects are arrows $f:X\to C$, while its arrows from $(f:X\to C)$ to $(g:Y\to C)$ over $h:X\to Y$ are 2-cells $f\to gh$.

7) As an instance of 6), consider the 2-category of posets, and take $C = 2$, the usual 2-element poset.
We so get the fibration of posets $X$ with an order ideal $A\subseteq X$;
by restricting to discrete posets, we get again the example in 1).

8) As another instance of 6) consider the 2-category of categories and $C$ any category;
restricting along the discrete inclusion $\bf Set \to \bf Cat$ we get the usual family fibration of $C$.

9) Yet another instance of 6) with $\cal C = \bf Cat$ and $C = \bf Set$, is the indexed category of presheaves $X\mapsto \bf Set^{X^{op}}$,
also a main instance of Lawvere's hyperdoctrine.

10) The example in 9) above can be also obtained as a restriction of the codomain fibration $\bf{Cat}^\to \to \bf{Cat}$ by taking, as objects,
just those functors which are discrete fibrations (a sort of generalization of the relation between 1) and 3)).
Thus we have the "discrete fibration" fibration $\bf dfib \to \bf Cat$:
the objects of $\bf {dfib}$ are pairs $(X,a)$, where $X$ is a category and $a:A\to X$ is a discrete fibration over $X$
while its arrows $(X,a) \to (Y,b)$ are functors $f:X\to Y$ and $g:A\to B$ such that $fa = bg$,
and the functor $\bf {dfib} \to \bf{Cat}$ is the obvious one.

For instance, the fiber in $\bf {dfib}$ over the category $P$ with two parallel arrows is of course essentially the category of graphs,
but a morphism $G\to H$ in $\bf {dfib}$ over the endofunctor of $P$ which exchanges those arrows
is an contravariant morphism of graphs $G^{op}\to H$.

Claudio Pisani (Jun 16 2023 at 23:09):

11) The fact that $\bf dfib \to \bf Cat$ is in fact a bifibration (that is, it is also an op-fibration) subsumes in a sense the Yoneda lemma.
Indeed, let $a:A\to X$ a discrete fibration (that is, an object of $\bf dfib$ over $X$),
and let $1\in\bf dfib$ be the terminal object, which is the identity discrete fibration over the terminal category $1\in\bf Cat$.

Then it is clear that "points" $s:1\to a$ in $\bf dfib$, over a point/object $x:1\to X$ in $\bf Cat$
correspond to the objects of $A$ over $x$ (that is to elements of $a(x)$, if we see $a$ as a presheaf).
But since $\bf dfib \to \bf Cat$ is an opfibration, these correspond also to vertical arrows (natural transformation of presheaves) $\exists_x1\to a$
from the image/sum/existential quantification $\exists_x1$ of $1$ along $x$.

That is, the presheaf on $X$ represented by the object $x:1\to X$ is the existential quantification of the terminal object of $\bf dfib$ along the morphism $x$ in the base category $\bf Cat$.
(Of course, quantifications in this context are usually known as Kan extension...)