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: opfibrations/fibrations

Matteo Capucci (he/him) (Oct 06 2020 at 10:10):

I'm getting lost in terminology, so I'm here for a sanity check: is it true that a fibration $F: E \to B$ (of categories) is equivalent to a pseudofunctor $F' : B^\mathrm{op} \to \mathbf{Cat}$ given by the contravariant Grothendieck construction, while an opfibration $G: E \to B$ is equivalent to a pseudofunctor $G' : B \to \mathbf{Cat}$ given by the covariant Grothendieck construction?

Matteo Capucci (he/him) (Oct 06 2020 at 10:14):

Hence: given $H' : B^\mathrm{op} \to \mathbf{Cat}$, is it equivalent to an opfibration $H : E \to B^\mathrm{op}$?

Spencer Breiner (Oct 06 2020 at 13:43):

That's right. Fibrations allow you to pull back an object (or morphism) in $E$ along a morphism in $B$. Opfibrations push forward along maps in the base.

Reid Barton (Oct 06 2020 at 13:46):

If you're wondering why "fibration" involves an "op" while "opfibration" doesn't involve an "op", I think the reason is that "fibrations" came first, for basically the same reason that presheaves involve an "op".

Matteo Capucci (he/him) (Oct 06 2020 at 15:09):

Thanks people!

Matteo Capucci (he/him) (Oct 06 2020 at 15:09):

@Reid Barton my problems were mostly that different sources call them differently, especially the Grothendieck construction has quite a few different conventions

Matteo Capucci (he/him) (Oct 06 2020 at 15:12):

Since I'm here: do you know what happens when you compose an opfibration and its functor of fibers? That is, you have $G: E \to B$ and then $G' : B \to \mathbf{Cat}$, is $G'G : E \to \mathbf{Cat}$ of any interest? Given an object in $E$, it should return the fiber it lies in, and given a morphism, it should return the functor induced by its horizontal part

John Baez (Oct 06 2020 at 16:49):

I've never thought about that composite. I'd bet it is interesting. By the way, I guess you know this, but people would usually write $F : B \to \mathbf{Cat}$, $\int F : E \to B$, so you're talking about $F \circ \int F$.

Matteo Capucci (he/him) (Oct 06 2020 at 17:20):

Oh right! I didn't use that notation since usually people abuse notation/terminology and call 'Grothendieck construction' just the construction of the total category of the resulting fibration, and then the fibration itself is called something like $\pi_F$.

John Baez (Oct 06 2020 at 17:24):

Oh, you're right, even I usually use $\int F$ to mean the total category - I don't know what I was thinking just now.

Matteo Capucci (he/him) (Oct 06 2020 at 17:30):

I like your notation better since it stresses the fibration, though the total category is really the star of the construction, which makes you want to have a specific notation for that, which makes you regret using $\int F$ for the projection functor in the first place! :laughing:

Jade Master (Oct 06 2020 at 18:54):

It might be illuminating to think about this composite in the case of functions. For a function $f : X \to Y$ there is an inverse map

$f^{-1} : Y \to \mathsf{Set}$

It turns out that the grothendieck construction of $f^{-1}$ is the function $f$. To be completely honest I usually think of the usual Grothendieck construction as a fancier version of this. In this context the composite is

$f^{-1} \circ f : X \to \mathsf{Set}$

If $f$ is injective, then this composite is the identity. In general it is multi-valued. You can use this intuition in full-version of the Grothendieck construction as well. $F \circ \int F$ is like the multivalued result of a functor composed with its inverse.

John Baez (Oct 06 2020 at 18:58):

Everyone should think of the Grothendieck construction as a fancier version of what Jade just described.

Using $f^{-1}$ as a name for the map sending each point of $Y$ to its inverse image under $f$ may confuse some people here, so I hope they get the point: it's just the usual usage of $f^{-1}$ to mean "inverse image" (which confuses all beginners, since $f^{-1}$ has another meaning too, in which $f^{-1}$ exists iff $f$ is a bijection).

John Baez (Oct 06 2020 at 19:02):

Another nice way to think of the Grothendieck construction is that it's an analogue of this thing in topology:

If you have a fibration $p: E \to B$ where the fiber is $F$, it has a classifying map

$f: B \to B G$

where $G$ is the group of homotopy autoequivalences of $F$, and $BG$ is the classifying space of $G$. Conversely from the classifying map $f: B \to BG$ we can reconstruct the fibration $p: E \to B$ up to homotopy equivalence.

John Baez (Oct 06 2020 at 19:03):

So, we can ask Matteo's question in this context: what do you get if you compose $f$ and $p$? You get

$f \circ p: E \to BG$

John Baez (Oct 06 2020 at 19:04):

This is the classifying map for some fibration with $E$ as its base space! Call this fibration

$\tilde{p}: \tilde{E} \to E$

John Baez (Oct 06 2020 at 19:05):

The fiber of this fibration is still $F$ (since we got it from a classifying map to $B G$).

John Baez (Oct 06 2020 at 19:06):

What is it? Well, there's only one reasonable choice: it's the pullback of the fibration

$p: E \to B$

along itself!

John Baez (Oct 06 2020 at 19:07):

I'm too lazy to draw the pullback square. But this pullback will be a fibration over $E$ with the same fiber as our original fibration, namely $F$.

John Baez (Oct 06 2020 at 19:08):

If you draw pictures of everything here - drawing topological spaces as blobs in the usual way, with points as dots - and also draw pictures of what Matteo was asking about - drawing categories as blobs in the usual way, with points as objects - you'll see they're the exact same pictures.

John Baez (Oct 06 2020 at 19:09):

So, we're "pulling back a fibration along itself" - either in the categorical sense or the topological sense.

Dan Doel (Oct 06 2020 at 19:23):

I'm going to keep thinking of it as a fancier Σ type, and considering all this inverse image stuff as hacking elegant type theoretic presentations into other languages. :smile:

John Baez (Oct 06 2020 at 19:27):

Ooookay. Mathematicians learn inverse images in college so that's how we think.

Reid Barton (Oct 06 2020 at 19:27):

$\int F$ is certainly some kind of fancy version of a $\Sigma$ type, but categories don't form a topos and as far as I know we don't really have a type theoretic presentation of this yet--that's part of what directed type theory is supposed to, I think.

Dan Doel (Oct 06 2020 at 19:29):

Yeah, maybe.

sarahzrf (Oct 07 2020 at 01:09):

if i learned anything from shulman's sub-nlab, it's that when you have higher structure, many of the roles previously played by slices are now properly played by fibrational and/or opfibrational slices

sarahzrf (Oct 07 2020 at 01:09):

categories don't form a topos, but hopefully they form a 2-topos

sarahzrf (Oct 07 2020 at 01:11):

the correspondence between Set/B and Set^B for a set B is in some sense a kind of foundational principle showing why the slice over B is the category where type theory in a context "x : B" takes place

sarahzrf (Oct 07 2020 at 01:12):

and the categorification of that is the correspondence between the opfibrational slice over B and Cat^B, for a category B

sarahzrf (Oct 07 2020 at 01:13):

so presumably categorified type theory in a context "x : B" should happen in an opfibrational slice, rather than an ordinary slice—or something similar

sarahzrf (Oct 07 2020 at 01:14):

ugh i should probably read about stack semantics sometime

sarahzrf (Oct 07 2020 at 01:15):

...actually sorry iirc it's less about higher structure and more about invertibility or something?

sarahzrf (Oct 07 2020 at 01:16):

like, i seem to recall @Joe Moeller mentioning something way back about like, any functor between groupoids is equivalent to a fibration, or something like that—so the relevant fact about sets is not that they lack higher structure, but that they're groupoidal

sarahzrf (Oct 07 2020 at 01:18):

if you look at (0, 1)-categories, preordered sets, then despite the lack of higher structure, we once again have that PreOrd^P doesn't correspond to PreOrd/P—it corresponds to an opfibrational slice

sarahzrf (Oct 07 2020 at 01:18):

oo, sry, @Reid Barton is this what you meant about directed type theory :thinking:

Dan Doel (Oct 07 2020 at 01:19):

Oh right.

Dan Doel (Oct 07 2020 at 01:21):

Directed type theory has directed-identity/hom types, and tracks various sorts of variance for variables and whatnot.

Dan Doel (Oct 07 2020 at 01:21):

Depending on which one you're talking about.

Dan Doel (Oct 07 2020 at 01:22):

I'm not exactly sure how that fits into (op)fibrations.

Dan Doel (Oct 07 2020 at 01:25):

I guess the variance on a family of types would determine its status as a fibration?

sarahzrf (Oct 07 2020 at 01:25):

aaa there are too many things to learn >_<

Dan Doel (Oct 07 2020 at 01:27):

$x :^- A ⊢ B(x)\ \mathsf{type}$ is an opfibration, and $x :^+ A ⊢ B(x)\ \mathsf{type}$ is a fibration, maybe. But I've seen things that also have "invariant" and "Isovariant" things, so it can get quite complicated.

Dan Doel (Oct 07 2020 at 01:28):

Or is that backwards for the same reason that this thread started?

John Baez (Oct 07 2020 at 05:00):

sarahzrf said:

like, i seem to recall Joe Moeller mentioning something way back about like, any functor between groupoids is equivalent to a fibration, or something like that—so the relevant fact about sets is not that they lack higher structure, but that they're groupoidal

Yes, I think I taught him this! Given any functor between groupoids $p : E \to B$, you can "puff up" $E$ and get an equivalent groupoid $E'$ and a fibration $p': E' \to B$ that's equivalent to $p$, in the sense that the triangle made from $p : E \to B$, $p' : E' \to B$ and the equivalence commutes up to natural isomorphism.

John Baez (Oct 07 2020 at 05:02):

It's easy to cook up $E'$. An object of $E'$ is an object of $e \in E$ together with an isomorphism $f: p(e) \to b$ in $B$, where $b$ is any object of $B$.

John Baez (Oct 07 2020 at 05:02):

And it's easy to cook up $p': E' \to B$: it sends $f: p(e) \to b$ to $b$.

John Baez (Oct 07 2020 at 05:03):

The fibers of $p'$ are called the homotopy fibers of $p$.

John Baez (Oct 07 2020 at 05:03):

For example $p'$ is surjective on objects iff $p$ is essentially surjective on objects.

John Baez (Oct 07 2020 at 06:36):

I guess in homotopy theory this trick is called taking the "homotopy cocylinder" of $p: E \to B$.

Matteo Capucci (he/him) (Oct 07 2020 at 09:53):

Wow that's a lot of nice intuitions there! Thanks @John Baez and @Jade Master.
Lately I'm with @Reid Barton here, in that I think of $\int$ as a categorified version of $\Sigma$. The correct setting for this, I don't know.

Matteo Capucci (he/him) (Oct 07 2020 at 09:54):

Maybe it is correct for $\infty\mathrm{Grpd}$

sarahzrf (Oct 07 2020 at 14:49):

i just told you what it was :P

sarahzrf (Oct 07 2020 at 14:53):

John Baez said:

It's easy to cook up $E'$. An object of $E'$ is an object of $e \in E$ together with an isomorphism $f: p(e) \to b$ in $B$, where $b$ is any object of $B$.

is this some sort of comma construction?

sarahzrf (Oct 07 2020 at 14:53):

oh wait... commas are lax pullbacks, right?

sarahzrf (Oct 07 2020 at 14:53):

is this a pseudo pullback?

sarahzrf (Oct 07 2020 at 14:53):

:thinking:

Dan Doel (Oct 07 2020 at 14:56):

I think if you do John's construction in HoTT, you get something where part of it can be collapsed out. Like, you have $p : E → B$, and $E' = Σ_{e:E} Σ_{b:B} p(e) \equiv b$, and $p' = \mathsf{fst} \circ \mathsf{snd}$. But the inner $Σ$ is contractible, so $E' \simeq E$.

Dan Doel (Oct 07 2020 at 15:01):

Also that is how you write pullbacks in HoTT. $Σ_{a:A,b:B} f(a) \equiv g(b)$

sarahzrf (Oct 07 2020 at 16:51):

more like homotopy pullbacks

John Baez (Oct 07 2020 at 16:58):

sarahzrf said:

is this a pseudo pullback?

You could say "pseudo pullback", but one piece of jargon that's good for googling around is "iso-comma object".

The terminology for weakened pullbacks is annoying because there are many variants, e.g.

"If the coherence isomorphisms are retained, but ... are required to be identities and ... is required to be unique, then the simplified definition becomes that of a strict iso-comma object, while the unsimplified definition becomes that of a strict pseudo-pullback.

John Baez (Oct 07 2020 at 17:00):

But anyway, yes, I bet you can think of the homotopy cocylinder of $p: E \to B$ as a pseudo pullback or "iso-comma object" built from $p: E \to B$ and $1 : B \to B$.

Hakimi Rashid (Oct 27 2020 at 07:37):

Sorry if this seems out of topic. But, with my limited knowledge... I think somehow this fibration concept maybe can be used to capture parameter estimation?