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.
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 and every above and , a coproduct diagram above .
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 and are not the Cartesian arrow above and 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.)
If the projection is a fibration, then it should have this property as soon as it preserves coproducts. Pick some arbitrary coproduct of and , then is a coproduct of and , hence isomorphic to . Now a cartesian lifting of that isomorphism ending at has a domain that's also a coproduct of and and lies strictly above .
Yeah, I trough about that, but it makes the lifting a bit silly, with, in particular 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 would be the same thing as the the sum of Cartesian lifting along pullbacks . By using extensivity along Cartesian arrows (i.e. where is the category of cartesian slices to ) 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.