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: pushing fibrations

Christian Williams (Jan 07 2023 at 15:48):

I'm wondering when a bifibration is of a simple classic form. In a category with pullbacks, the codomain functor $cod: Arr(C)\to C$ is a bifibration, with pullback as the fibration and postcomposition as its left adjoint.

Pullback along $f^\ast: C/b \to C/a$ is right adjoint to postcomposition $f(-): C/a \to C/b$, because a morphism $f(x)\to y$ in $C/b$ is equivalent to $x\to f^\ast y$ in $C/b$, by the universal property of pullback: image.png

But we care about lots of fibrations which "sit inside" $cod$: special morphisms, such as monomorphisms. Being mono is not preserved by postcomposition, but we can take the image factorization to get a new mono. So the "push" that's left adjoint to "pull" is basically postcomposition, though not literally.

My question is:
If $M(C)$ is a subcategory of $Arr(C)$ and $cod:M(C)\to C$ is a fibration via pullback, when do we know that it is also a bifibration by postcomposition (or postcomp + some help, like image factorization)?

I think the uniqueness of left adjoints should imply that it must be postcomposition, whenever the property determining $M(C)$ is preserved by postcomp, or whenever there is a way to "force" things back into $M(C)$ after postcomposing.

(I think there are probably references for this, but I haven't found one yet.)

James Deikun (Jan 07 2023 at 15:59):

Do you actually care about non-full subcategories? I ask because it probably complicates things.

Christian Williams (Jan 07 2023 at 16:01):

Yes, I do. My main motivation is Fib over Cat, which is not full. How does it complicate?

James Deikun (Jan 07 2023 at 16:20):

That should probably be fine since IIRC it still includes all the pullback squares between the arrows it includes.

Christian Williams (Jan 07 2023 at 17:28):

Hm, okay. The composite of a fibration with a functor is not a fibration; but like image factorization, somehow the pushforward is some canonical "free fibration" on this - is that right?

Christian Williams (Jan 07 2023 at 17:31):

Turning the fibration into an indexed category $A:I^{op}\to Cat$, pushing forward along $F:I\to J$ has the left extension formula $F_!A(j) = \int i:I.\; A(i)\times J(j,Fi)$. This looks just like "composing $A$ with the conjoint $J(1,F)$", though that doesn't actually type-check because $A$ is not a profunctor but a diagram of categories and profunctors.

Christian Williams (Jan 07 2023 at 17:33):

So it seems at least morally, pushing forward along $F$ is "composing with $J(1,F)$". But that doesn't literally make sense, so I'm wondering what's the story here. Are we just composing a fibration $A\to I$ with $F:I\to J$ and then "freely making it a fibration"?

Christian Williams (Jan 07 2023 at 18:06):

That must be the idea. $dom:Arr(C)\to C$ is the universal fibration over $C$. Similarly the comma category $dom: J/F\to J$ should be the "free fibration" of $F$, and somehow pushing forward by $F$ is tensoring with this.

Christian Williams (Jan 07 2023 at 18:07):

This is the abstract theory of fibrations I really need to learn. Is Street the main source?

Christian Williams (Jan 07 2023 at 18:39):

Ah yes! I think it's this image.png

Christian Williams (Jan 07 2023 at 18:46):

Finally a clearer view of "pushing" fibrations; I'd been wanting that for like a year.

For context, I care about pushing fibrations because that is how to compose profunctors of fibrant double categories (equipments).

If anyone has thoughts, just let me know.

Mike Shulman (Jan 07 2023 at 23:56):

It's not literally the free fibration, because it should respect the fibration structure of the one you started with. That is, if you gave a fibration $p:A\to I$ and a functor $f:I\to J$, and you take $q : \hat{A}_J \to J$ to be the free fibration on the composite $A\to I \to J$, then the resulting square from $p$ to $q$ will not be a morphism of fibrations.

Mike Shulman (Jan 07 2023 at 23:57):

But you should be able to tell a story about "relatively free" things, given the two related monads on slice categories for fibrations over $I$ and fibrations over $J$.

Christian Williams (Jan 08 2023 at 02:40):

Wow, sounds like a beautiful idea.

Christian Williams (Jan 08 2023 at 02:44):

Also, something special is happening in the diagram above: pushforwards in Fib are given by composition by the companion in TwoSidedFib! What's going on?

Mike Shulman (Jan 08 2023 at 05:36):

Isn't that essentially just the usual fact about any framed bicategory, that pushforwards and pullbacks are given by composition with the base change objects?

Christian Williams (Jan 08 2023 at 06:33):

Yes, in TwoSidedFib, but that's pushing forward fibrations as loose morphisms; I want to think of them as objects.

Christian Williams (Jan 08 2023 at 06:34):

I was wondering earlier about some kind of arrow double category of TwoSidedFib, but it doesn't seem to include fibered profunctors the way I'd want.

Christian Williams (Jan 08 2023 at 06:47):

Damn, maybe what's missing is that TwoSidedFib is really a triple category. The current definition leaves out profunctors, just like the current definition of Fib as 2-category.

Mike Shulman (Jan 08 2023 at 07:07):

A loose morphism is an object.

Christian Williams (Jan 08 2023 at 07:08):

An object of a category, yes. I mean an object of a double category.

Christian Williams (Jan 08 2023 at 07:09):

I think TwoSidedFib actually is a triple category, and the concept of fibered profunctor we've discussed generalizes directly.

Mike Shulman (Jan 08 2023 at 07:19):

Oh, I see what you mean.

Christian Williams (Jan 08 2023 at 07:27):

great! I think it's a vast and rich universe. I'll label a cube.

Christian Williams (Jan 08 2023 at 07:33):

tsfib.png
$Q_0,Q_1$ and $R_0,R_1$ are two-sided fibrations. $Q_0\to Q_1$ and $R_0\to R_1$ are morphisms of them. this is the current notion of TwoSidedFib in the literature --- but it's forgetting profunctors.

$f_0$ and $g_0$ are profunctors, and $\gamma_0$ is a "two-side-fibered profunctor": a profunctor $\gamma_0:Q_0\to R_0$ equipped with transformations to $\gamma_0\Rightarrow f_0(\pi^Q_X, \pi^R_A)$ and $\gamma_0\Rightarrow g_0(\pi^Q_Y,\pi^R_B)$, such that the collage of these two transformations forms a two-sided fibration.

Christian Williams (Jan 08 2023 at 07:38):

(similarly for $\gamma_1$.) finally, a cube $\gamma_0$ to $\gamma_1$ is basically "a morphism of their collage two-sided fibrations".