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.
A bifibration induces for each adjoint functors between the fibers .
In my work I use bifibrations where this adjunction is a co-reflection, i.e., is isomorphic to the identity. Is there a name for this kind of bifibration/is anyone aware of places this concept has been used?
Does the bifibration , which picks out the set of nodes of a graph, have this property?
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 . I should mention that in my examples, E and B are preorders and so and are a Galois connection.
Thanks. Okay, yes, it sounds like a strong condition.
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
Okay, that's better. You fooled me with the first example. :upside_down:
Is it true that pulling back and then pushing forward is also not isomorphic to the identity for ? If I were awake I could figure it out.
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.
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
Yes.
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!)
@Max New Now I'm curious about how your bifibration looks like!
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.
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.
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.