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: co-cartesian monoidal fibration


view this post on Zulip Flavien Breuvart (Jan 15 2024 at 10:22):

Dear all,
I need, for my work, a proper notion of co-Cartesian monoidal fibration. The notion of monoidal fibration is well known and has been extensively studied by Michael, remains to make it "co-cartesian". Naively, I through that it was sufficient to require the fibration, the base and the projection to be Cartesian monoidal. Unfortunately, it was not sufficient for my works.
My issue is that the co-cartesian product is unique up-to iso, in a way, it is not a monoidal product, but a bunch of equivalent ones, and I need all of those to be lifted from the base category to the fibration category. Concretely, I need, for every co-product diagram i,j:XZYi,j : X\rightarrow Z \leftarrow Y and every A,BA,B above XX and YY, a coproduct diagram i,j:AAi ⁣+ ⁣jBBi^*,j^*: A\rightarrow A\: {_{i\!}{+}_{\!j}}\: B\leftarrow B above i,ji,j.
Have any of you seen anything of the kind ? I feel that there should be a higher level framework where this lifting is a kind of fibrational lifting, but I can't see it. In particular, the fact that ii^* and jj^* are not the Cartesian arrow above ii and jj makes the link a bit difficult to understand.
(I have to precise that I ran into this issue while working with an expensive base, which makes arbitrary the choice of the co-product.)

view this post on Zulip Mike Shulman (Jan 15 2024 at 17:45):

If the projection is a fibration, then it should have this property as soon as it preserves coproducts. Pick some arbitrary coproduct CC of AA and BB, then p(C)p(C) is a coproduct of XX and YY, hence isomorphic to ZZ. Now a cartesian lifting of that isomorphism ending at CC has a domain that's also a coproduct of AA and BB and lies strictly above ZZ.

view this post on Zulip Flavien Breuvart (Jan 16 2024 at 07:49):

Yeah, I trough about that, but it makes the lifting a bit silly, with, in particular A+BA ι1 ⁣ ⁣+ ⁣ι2 BA+B\neq A\ _{\iota_1\!\!}+_{\!\iota_2}\ B and the composition counterpart (see below). I was kind of hopping for an easier framework to work with, but I will go with that ^^" thanks !
To be more precise, I was looking for conditions where the Cartesian lifting f(A i ⁣ ⁣+ ⁣j B)f^*(A\ _{i\!\!}+_{\!j}\ B) would be the same thing as the the sum of Cartesian lifting along pullbacks fi(A) if ⁣ ⁣+ ⁣jf fj(B)f_{|i}^*(A) \ _{i_{|f}\!\!}+_{\!j_{|f}}\ f_{|j}^*(B). By using extensivity along Cartesian arrows (i.e. C/A+C/BC/(A+B)\mathbb C/A+\mathbb C/B\sim \mathbb C/(A+B) where C/A\mathbb C/A is the category of cartesian slices to AA) we are not that far, but I don't see any way to get ride of the last iso. I will have to deal with it.