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: theory: category theory

Topic: fibrations and quantifiers

James Deikun (May 02 2022 at 13:32):

Grothendieck and Street fibrations $p : E \to B$ are normally defined as "for each $e : E$ and $f : b \to p(e)$ there is a Cartesian lift" where Cartesianness is a universal property. This results in a $\forall\exists\forall\exists!$ predicate. Is this logical complexity inherent in fibrations or is there some reformulation that uses less quantifiers, ideally something more like $\forall\exists!$?

Chad Nester (May 02 2022 at 14:05):

I guess the 2-categorical universal property of street fibrations is only one alternation?

James Deikun (May 02 2022 at 14:36):

Looks like at least some versions are ...

James Deikun (May 02 2022 at 14:37):

... but I question whether maybe there's another alternation hidden in the definition of comma category?

Mike Shulman (May 02 2022 at 15:48):

I think if you write out the definition of Street fibration explicitly, it has exactly the same alternation of quantifiers, just with an extra isomorphism inserted.

Tim Campion (May 03 2022 at 15:11):

It depends what your language is. One way to define a fibration is the following:

Def: A fibration is a functor $p : E \to B$ such that the induced map $E \to B^{[1]} \times_B E$ has a left adjoint over $B$.

Here it comes out as just $\exists(!)$. But this comes at the price of requiring that you know how to talk about pullbacks of categories and arrow categories, or at least that you know how to talk about this particular sort of pullback (the category $B^{[1]} \times_B E$ is the lax limit of $E \to B$).

Tim Campion (May 03 2022 at 15:11):

(I've been a bit vague about some of the details related to variance here :))

Mike Shulman (May 04 2022 at 03:05):

Yes, you can reduce the apparent quantifier complexity of many things by shifting it into higher-order constructions on the objects you're talking about.

Tim Campion (May 04 2022 at 14:35):

In contexts like internal category theory, the definition I gave is to be preferred to the definition which talks about cocartesian lifts, since framing it in terms of cocartesian lifts leans into the fact that $Cat$ is generated by the terminal category, the arrow category, and the composable-pair category.

Does this mean that "in general" the idea of having a well-defined notion of quantifier complexity is problematic?

Reid Barton (May 04 2022 at 14:38):

Should it be $E^{[1]} \to B^{[1]} \times_B E$?

Tim Campion (May 04 2022 at 14:42):

Reid Barton said:

Should it be $E^{[1]} \to B^{[1]} \times_B E$?

That does seem like a more natural thing to write, but I think I wrote it right (for some choices of variance everywhere!)-- see the 3rd definition here. But now you've got me trying to think through why this is the correct thing...

Tim Campion (May 04 2022 at 14:48):

One indication of the subtlety is that although the notation $B^{[1]} \times_B E$ suggests a particular map $B^{[1]} \times_B E \to B$ to use to make everything "over $B$", this suggestion turns out to be wrong. I seem to be doing cocartesian fibrrations rather than cartesian fibrations, so I'll stick with that setting. I didn't actually say, but in the pullback $B^{[1]} \times_B E$, the map $B^{[1]} \to B$ is via the domain map, but the pullback $B^{[1]} \times_B E$ is to be regarded as "over $B$" using the codomain map $B^{[1]} \to B$.

Reid Barton (May 04 2022 at 14:49):

Oh, I overlooked the "over $B$" part entirely

Tim Campion (May 04 2022 at 14:51):

The left adjoint takes an object $e \in E$ and a morphism $\beta : p(e) \to b$, and carries it to the codomain of the cocartesian lift of $\beta$ emanating from $e$.

Tim Campion (May 04 2022 at 14:52):

It is funny, because there's a natural thing you could be mapping to in $E^{[1]}$, namely the cocartesian lift itself.

Jonathan Weinberger (May 04 2022 at 14:52):

Reid Barton said:

Should it be $E^{[1]} \to B^{[1]} \times_B E$?

This would be for the condition of the (non-fibered) LARI (or RARI) to exist (Chevalley criterion)

Mike Shulman (May 04 2022 at 14:53):

I tend to view the notion of quantifier complexity as an artifact of classical first-order logic rather than something intrinsically interesting about mathematics. The usual way of classifying quantifier complexity doesn't even make sense in constructive logic, where you can't rewrite everything with a single prefix of alternating quantifiers. But my biases are showing. (-:

Reid Barton (May 04 2022 at 14:53):

LARI?

Jonathan Weinberger (May 04 2022 at 14:54):

left adjoint right inverse

Reid Barton (May 04 2022 at 14:54):

Is the claim that there is some other definition of fibration in terms of whatever that means?

Jonathan Weinberger (May 04 2022 at 14:54):

Yes, the two definitions (in an appropriate context) are equivalent

Reid Barton (May 04 2022 at 14:55):

And what is the other definition?

Jonathan Weinberger (May 04 2022 at 14:55):

The one by @Tim Campion gives the "transport" map, while the LARI one gives the "lifting" map

Jonathan Weinberger (May 04 2022 at 14:56):

The pullback hom map $E^{[1]} \to B^{[1]} \times_B E$ has a left adjoint right inverse

Reid Barton (May 04 2022 at 14:57):

And "left adjoint right inverse" means one of the unit/counit (I'm sure I could work out which) is an isomorphism?

Reid Barton (May 04 2022 at 14:58):

That's nice! I can see that just asking for an adjoint might give you something that isn't actually a lift or starts at the correct object.

Jonathan Weinberger (May 04 2022 at 14:59):

The definitions make sense in a higher categorical setting as provided by $\infty$-cosmoses, cf. Theorem 5.2.8 in Riehl--Verity: Elements of ∞-Category Theory

Tom Hirschowitz (May 04 2022 at 15:33):

Cool! And the correct requirement appears to be that the above functor has a rari.

John Baez (May 04 2022 at 15:54):

Reid Barton said:

And "left adjoint right inverse" means one of the unit/counit (I'm sure I could work out which) is an isomorphism?

To be honest, in the literature it means that the left adjoint is the right inverse on the nose of the right adjoint, with the identity $LR = 1$ serving as the counit.

John Baez (May 04 2022 at 15:56):

So if you want to use these old results you need to either put up with that or adapt them to the case $LR \cong 1$.

John Baez (May 04 2022 at 15:57):

I believe it was John Gray who introduced the concepts of "lari" and "rali" - in any event, he has a paper where he used those concepts.

Jonathan Weinberger (May 04 2022 at 16:00):

John Baez said:

I believe it was John Gray who introduced the concepts of "lari" and "rali" - in any event, he has a paper where he used those concepts.

Yes, the reference is John W. Gray: Fibred and Cofibred Categories (1965)

John Baez (May 04 2022 at 16:11):

Thanks. Yes, @Christina Vasilakopoulou used these ideas in our paper Structured versus decorated cospans.

John Baez (May 04 2022 at 16:12):

We have

Lemma 4.4 (Gray). Let $U: X \to A$ be an opfibration. Then U has a lari if its fibers have initial objects that are preserved by the reindexing functors.

John Baez (May 04 2022 at 16:12):

"Has a lari" means the same thing as "is a rali".

John Baez (May 04 2022 at 16:15):

If I remember correctly, the 'evilness' of Gray's concept of lari - the fact that it demands $LR = 1$ on the nose - combines with the 'evilness' in the traditional definition of opfibration (or fibration) and the 'evilness' of demanding that initial objects be strictly preserved to make this result true.

John Baez (May 04 2022 at 16:16):

I don't like all this evil, but we had a situation where all this extra strictness actually held true, so it didn't seem worth avoiding it.

Jonathan Weinberger (May 04 2022 at 17:32):

John Baez said:

Thanks. Yes, Christina Vasilakopoulou used these ideas in our paper Structured versus decorated cospans.

Cool, thanks! :+1:

John Baez (May 04 2022 at 17:38):

Tom Hirschowitz said:

Cool! And the correct requirement appears to be that the above functor has a rari.

By the way, did you really mean "rari"? I've mainly seen results about ralis and laris. But I guess if a functor $A \to B$ is a lari then the corresponding functor $A^{\text{op}} \to B^{\text{op}}$ is a rari.

Jonathan Weinberger (May 04 2022 at 17:43):

Sorry, confusingly above I was referring to a theorem characterizing cartesian fibrations rather than cocartesian fibrations. So $\pi:E \to B$ is a cartesian fibration iff $E^{\Delta^1} \to B \downarrow \pi$ has a RARI. Dually, $\pi$ is a cocartesian fibration iff $E^{\Delta^1} \to \pi \downarrow B$ has a LARI.

Tim Campion (May 08 2022 at 18:48):

Jonathan Weinberger said:

Sorry, confusingly above I was referring to a theorem characterizing cartesian fibrations rather than cocartesian fibrations. So $\pi:E \to B$ is a cartesian fibration iff $E^{\Delta^1} \to B \downarrow \pi$ has a RARI. Dually, $\pi$ is a cocartesian fibration iff $E^{\Delta^1} \to \pi \downarrow B$ has a LARI.

I didn't know about this characterization, this is neat! Where's a good place to read more about it?

Tim Campion (May 08 2022 at 18:55):

Oh -- I see this "Chevalley criterion" is right there in 3.17 of Street's "Fibrations in bicategories". I think I'd previously read carelessly and assumed this was the same condition I was talking about above.

Tim Campion (May 08 2022 at 18:55):

I'm curious now why it's called the "Chevalley criterion" -- Street doesn't explain this reference.

Jonathan Weinberger (May 08 2022 at 18:56):

@Tim Campion For the $\infty$-cosmos theoretical context, in Riehl--Verity: Elements of ∞-Category Theory, Chapter 5, particularly Section 5.2.
A more elementary discussion is in Loregian--Riehl: Categorical notions of fibration.
As far as I know, the characterization is due to Gray who attributes it to Chevalley, and it also is used by Street, as you pointed out

Jonathan Weinberger (May 08 2022 at 18:58):

Tim Campion said:

I'm curious now why it's called the "Chevalley criterion" -- Street doesn't explain this reference.

To quote "Elements", (after) Remark 5.2.7:

Lemma 5.2.5 extends to give an internal characterization of cartesian fibrations inspired by a similar result of Street [118, 119, 121], which in turn was inspired by previous work of Gray [48] on what he calls a “Chevalley criterion”⁸ (see also [131]).

⁸Gray attributes [48, 3.11] – the special case of the equivalence of (i)⇔(ii) of Theorem 5.2.8 in the ∞-cosmos 𝒞𝑎𝑡 – to
unpublished notes from a seminar given by Claude Chevalley at Berkeley in 1962.

Tim Campion (May 08 2022 at 19:02):

@Jonathan Weinberger Thanks, I guess I must have been aware of this at some point, but only retained one of these two 2-categorical definitions from Riehl-Verity. I'm currently trying to puzzle through the 4 notions of co/cartesian co/fibration in the $(\infty,2)$-category $Pr^L$ of presentable $\infty$-categories. I'm hoping that one of them is represented (modulo size issues) by $Pr^L$ itself. So it's good to have multiple ways to package the data.

Jonathan Weinberger (May 08 2022 at 19:12):

Tim Campion said:

I'm hoping that one of them is represented (modulo size issues) by $Pr^L$ itself.

Analogously to the representability condition/definition e.g. in Loregian--Riehl, Def. 3.1.1?

The LARI/RARI Chevalley conditions are used in $\infty$-cosmos theory to construct $\infty$-cosmoses of co-/cartesian fibrations, cf. Elements Cor. 6.3.8. and (proof of) Prop. 6.3.14.

In Riehl--Shulman's simplicial homotopy type theory one can do something analogous to formally prove various closure properties of co-/cartesian type families, cf the joint paper with @Ulrik Buchholtz Synthetic fibered (∞,1)-category theory. In contrast, I wouldn't know how to formally generalize the fibered adjoint conditions (to arbitrary maps between arbitrary simplicial types).

Tim Campion (May 08 2022 at 19:22):

My motivation is the following statement of descent:

Fact: Let $\mathcal E$ be a $\kappa$-compactly-generated $\infty$-category. Then the following are equivalent:

1. $\mathcal E$ is an $\infty$-topos.
2. The covariant slice functor $\mathcal E / (-) : \mathcal E \to Pr^L_\kappa$, $E \mapsto \mathcal E/E$, preserves colimits (and so is in fact a morphism in $Pr^L$).

I want to guess that $Pr^L_\kappa$ classifies some sort of size-restricted fibration in $Pr^L$, and then interpret (2) as saying that the codomain functor $cod : \mathcal E^{[1]} \to \mathcal E$ is some kind of fibration in $Pr^L$. So somehow the key issue is the requirement that every functor in sight preserve colimits...

Tim Campion (May 08 2022 at 19:27):

Sorry, I just edited my last post a bunch, but I think the way I have it now (as I originally wrote it) is correct. The inclusion $Pr^L_\kappa \to Pr^L$ preserves colimits, after all (but not limits)

Jonathan Weinberger (May 08 2022 at 19:37):

Tim Campion said:

I want to guess that $Pr^L_\kappa$ classifies some sort of size-restricted fibration in $Pr^L$

Thanks. So "classifying/represented" is meant in the sense of the Grothendieck construction?

Tim Campion (May 08 2022 at 19:39):

Yeah, I'm thinking that maybe $(Pr^L_\kappa)_{Spaces / } \to Pr^L_\kappa$ is the "universal fibration in $Pr^L$" in some sense. So $Pr^L_\kappa$ should represent "fibrations" in the sense that $Pr^L(\mathcal E, Pr^L_\kappa)$ should be naturally equivalent to the category of fibrations over $\mathcal E$ (with size restrictions).

I think that $\mathcal E^{[1]} \to \mathcal E$ ought to be the pullback of this "universal fibration" along the classifying map $\mathcal E/(-)$, in the case where $\mathcal E$ is a topos so that $\mathcal E/(-)$ is a morphism in $Pr^L$.

Tim Campion (May 08 2022 at 19:41):

I'm hoping it's just a matter of figuring out where to throw in "co"'s and "op"'s to get the right definitions...

Jonathan Weinberger (May 08 2022 at 19:42):

Great, thanks!