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: a property of bifibrations


view this post on Zulip Max New (Jul 18 2022 at 00:07):

A bifibration p:EBp : E \to B induces for each f:bbf : b \to b' adjoint functors between the fibers f!ff_! \dashv f^*.

In my work I use bifibrations where this adjunction is a co-reflection, i.e., ff!f^* \circ f_! is isomorphic to the identity. Is there a name for this kind of bifibration/is anyone aware of places this concept has been used?

view this post on Zulip John Baez (Jul 18 2022 at 00:16):

Does the bifibration p:GraphSetp: \mathsf{Graph} \to \mathsf{Set}, which picks out the set of nodes of a graph, have this property?

view this post on Zulip Max New (Jul 18 2022 at 00:30):

No, because you can take any graph G and map it to a one node graph with no edges and then push/pull to get back the discrete graph of G.

This probably indicates that you need a pretty restrictive notion of morphism in EE. I should mention that in my examples, E and B are preorders and so f!f_! and ff^* are a Galois connection.

view this post on Zulip John Baez (Jul 18 2022 at 03:49):

Thanks. Okay, yes, it sounds like a strong condition.

view this post on Zulip Max New (Jul 18 2022 at 13:17):

Oh, I wasn't quite right above but the property is still not true. As an example start with { l -> r }, pushforward the unique function to a one-element set to get a vertex with a self loop, and then pull back and you will get a complete graph on two vertices

view this post on Zulip John Baez (Jul 18 2022 at 13:26):

Okay, that's better. You fooled me with the first example. :upside_down:

view this post on Zulip John Baez (Jul 18 2022 at 13:27):

Is it true that pulling back and then pushing forward is also not isomorphic to the identity for p:GraphSetp: \mathsf{Graph} \to \mathsf{Set}? If I were awake I could figure it out.

view this post on Zulip John Baez (Jul 18 2022 at 13:29):

I guess it's not. Start with the map from the 2-element set to the 1-element set. Take the graph with a single self-loop on the 1-element set. Pull it back to the 2-element set, then push forward. I think you get a graph with 4 self-loops on the 1-element set.

view this post on Zulip Max New (Jul 18 2022 at 13:31):

I think a simpler example that works for non-multi-graphs would be to start with a vertex with a self loop and then pull back over an empty set of vertices and then push forward and you get a vertex with no self loop

view this post on Zulip John Baez (Jul 18 2022 at 13:32):

Yes.

view this post on Zulip John Baez (Jul 18 2022 at 13:33):

So, it seems nothing like this property holds for the bifibrations of the sort I've been thinking about. (If it did, I would want to know!)

view this post on Zulip Tom Hirschowitz (Jul 18 2022 at 13:50):

@Max New Now I'm curious about how your bifibration looks like!

view this post on Zulip Max New (Jul 19 2022 at 19:11):

It comes from my work on gradual typing https://arxiv.org/abs/1802.00061 That paper is phrased in terms of double categories that are pro-arrow equipments, and there's a way to define pro-arrow equipments using fibrations so I was wondering if there was a word for this additional axiom that we have.

view this post on Zulip John Baez (Jul 19 2022 at 19:19):

As you probably know - but just in case you don't - when Shulman gets pro-arrow equipments from bifibrations in Framed bicategories and monoidal fibrations, in Definition 13.31 he introduces various special kinds of bifibrations, like Beck-Chevalley, strong Beck-Chevalley, weak Beck-Chevalley, etc. I needed to learn about these in my work on decorated and structured cospan double categories. But I don't think he mentions the kind you're talking about.

view this post on Zulip Nathanael Arkor (Jul 19 2022 at 19:48):

This seems quite an unusual property to impose on an equipment: asking for every induced adjunction to be a coreflection is asking for every morphism in the underlying 2-category to be fully faithful. Accordingly, the condition is in a sense an equipment-theoretic version of left cancellative (2-)category. I would suspect that such structures are not particularly widespread.