Re: Fibrewise opposite fibration
If we work with split fibrations and arbitrary cartesian functors between them we can construct the opposite of a fibration without quotienting. That is possible but in my eyes less elegant than the usual approach where one assumes that one can factorize modulo equivalence relations even if they are big. Thomas ---------- You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. Leave group: https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27
2-monad theory and related model categories of sketches could be relevant here, because these techniques reduce the problematic case of a non-split fibrations F that was raised by David in his initial message to the easy case of an equivalent but split fibration F’. In terms of logical foundations, this requires sufficiently large universes, but I expect (but haven’t verified) that you can do without choice. I’m not sure I remember all the details correctly, but let me try to outline how this should work. Consider the category of sketches for fibrations: A sketch for a fibration is given by a functor E -> B and for each morphism f in B a set of “cartesian-marked” morphisms M_f in E that map to f. Morphism of sketches are commuting squares of functors that preserve Cartesian markings. Note that Cartesian-marked morphisms need not actually be Cartesian. Every fibration has a natural strucuture as sketch, where precisely the Cartesian morphisms are Cartesian-marked. And every sketch generates a fibration with natural marking. Informally, this generated fibration is obtained by freely adding morphisms to E so that all the M_f are non-empty and then adding commutative diagrams so that every Cartesian-marked morphism is actually Cartesian. Finally, one closes M_f under isomorphism over E. More formally, there is a model category structure on sketches such that precisely the naturally marked fibrations are fibrant objects, and the equivalences of fibrant objects are the componentwise equivalences in the arrow category on Cat. Fibrant replacement of a sketch is given by the informal free generation I explained in the previous paragraph. (Note that there’s a naming collision here: Fibrations in the sense of Grothendieck fibrations and in the model categorical sense.) Now, if you use Garner’s small object argument you get a fibrant replacement functor. Crucially, this fibrant replacement functor is the monad you get from a 1-categorical adjunction with the category of “strict” Grothendieck fibrations. These are given by Grothendieck fibrations with a cleavage, and their morphisms are commuting squares of functors that preserve cleavage on the nose. Why does this give you the equivalent split fibration F’ from a non-split fibration F I promised in the beginning? Like so: You first map F (considered as a naturally marked sketch) into the category of strict (in particular: split) fibrations via the left adjoint I mentioned in the preceding paragraph. From there you apply the right adjoint to get back to sketches, which is simply given by forgetting the cleavage and taking the natural marking to obtain F’. F -> F’ is an equivalence, and F’ has a cleavage by construction. If you want to know more about this you might want to take a look at my paper on models of type theory in lcc categories and its citations: https://protect-au.mimecast.com/s/J0ogCoV1Y2SzmkQri1YV08?domain=arxiv.org Among other things, this paper defines the model categories of sketches for lcc categories and strict lcc categories. Grothendieck fibrations should work entirely analogously. I believe Lack’s “Homotopy theoretic aspects of 2-category theory” works out the “strict” model category of strict Grothendieck fibrations I mentioned above in the generality of an arbitrary 2-monad, but I’m not aware of a general model categorical treatment of sketches. On Wed, Jan 31, 2024 at 17:41, <[streicher@mathematik.tu-darmstadt.de](mailto:On Wed, Jan 31, 2024 at 17:41, <<a href=)> wrote:
If we work with split fibrations and arbitrary cartesian functors between them we can construct the opposite of a fibration without quotienting. That is possible but in my eyes less elegant than the usual approach where one assumes that one can factorize modulo equivalence relations even if they are big.
Thomas
----------
You're receiving this message because you're a member of the Categories mailing list group from Macquarie University.
Leave group: https://protect-au.mimecast.com/s/H5fJCp81gYC8Z57nfDKrk8?domain=outlook.offi...
Hi Thomas et al, I believe the proposed non-quotiented construction works even with a cleaving that is not split. Does anyone know if this is true? (I thought I had checked this a while ago, but now I cannot find my notes and am less confident; however, it is claimed by Von Glehn in Example 3.9 here: http://www.tac.mta.ca/tac/volumes/33/36/33-36.pdf.) Glancing at it briefly, it looks rather like the identity and associativity laws follow from the higher identities governing associators and unitors in a pseudofunctor. I agree it is inelegant to assume a splitting, but I think it is rather elegant to assume a (non-split) cleaving as property-like structure (so we do not ask that it be preserved) — Indeed, this is precisely what you get from the Chevalley criterion for fibrations in a 2-category. I think this is analogous to the way that in an internal setting we must assume chosen structures but not typically ask to preserve the choices; when we do not wish to assume chosen structures at all, we can either pass to stacks or work in a univalent / fully saturated setting. Best, Jon On Wed, Jan 31, 2024, at 11:41 PM, streicher@mathematik.tu-darmstadt.de wrote:
If we work with split fibrations and arbitrary cartesian functors between them we can construct the opposite of a fibration without quotienting. That is possible but in my eyes less elegant than the usual approach where one assumes that one can factorize modulo equivalence relations even if they are big.
Thomas
You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
Dear Jon, for constructing the opposite of a fibration you do not need at all that the chosen cleavage is split. It is easy to see that fixing the cartesian arrow also fixes the vertical arrow. If everybody is happy with this solution I am fine. It is in the same spirit as chosen pullbacks or chosen finite limits. The reason for my reluctance is that nobody would consider as a natural notion a vector space with a chosen basis. The virtue of strong choice is that then such additional structure can be pulled out of the hat at demand. Thomas ---------- You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. Leave group: https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27
Hi Thomas, I'm sympathetic, but I don't agree about the comparison to vector spaces because a cleaving is nothing like a basis. My evidence for this is that for fibrations of univalent categories, cleavings are always canonical; on the other hand, there is no foundational tweak that could make vector spaces have canonical bases. Best, Jon On Thu, Feb 1, 2024, at 11:06 AM, Thomas Streicher wrote:
Dear Jon,
for constructing the opposite of a fibration you do not need at all that the chosen cleavage is split. It is easy to see that fixing the cartesian arrow also fixes the vertical arrow.
If everybody is happy with this solution I am fine. It is in the same spirit as chosen pullbacks or chosen finite limits. The reason for my reluctance is that nobody would consider as a natural notion a vector space with a chosen basis. The virtue of strong choice is that then such additional structure can be pulled out of the hat at demand.
Thomas
---------- You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. Leave group: https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27
I'm sympathetic, but I don't agree about the comparison to vector spaces because a cleaving is nothing like a basis. My evidence for this is that for fibrations of univalent categories, cleavings are always canonical; on the other hand, there is no foundational tweak that could make vector spaces have canonical bases.
I agree that from a univalent point of view all cleavages are equal. But from a univalent point of view all cleavages are even split! That is a bit too much for me (see Warning (1) on p.10 of my notes on fibered cats). But I do not want to take up old discussions! I really prefer to disagree. Instead I admit that all choices of cleavages are uniquely isomorphic which certainly is not teh case for bases. Thomas ---------- You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. Leave group: https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27
I think there is a problem with this analogy. A basis for a vector space is actual (higher) data, but a cleavage for a fibration is property-like data. Morphisms of fibrations that weakly preserve the cleavage are just morphisms of fibrations. Morphisms of vector spaces that preserve a chosen basis are very different from just morphisms of vector spaces. On Thu, 1 Feb 2024, 12:07 Thomas Streicher, <streicher@mathematik.tu-darmstadt.de<mailto:streicher@mathematik.tu-darmstadt.de>> wrote: Dear Jon, for constructing the opposite of a fibration you do not need at all that the chosen cleavage is split. It is easy to see that fixing the cartesian arrow also fixes the vertical arrow. If everybody is happy with this solution I am fine. It is in the same spirit as chosen pullbacks or chosen finite limits. The reason for my reluctance is that nobody would consider as a natural notion a vector space with a chosen basis. The virtue of strong choice is that then such additional structure can be pulled out of the hat at demand. Thomas You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
participants (5)
-
Christian Sattler -
Jon Sterling -
Martin Bidlingmaier -
streicher@mathematik.tu-darmstadt.de -
Thomas Streicher