Dear Thomas, I am a bit surprised that you, of all people, should defend cleavages, i.e. indexed categories. As far as I remember, there not many of them in the notes you wrote on Fibered categories a la Benabou. I remind you that these notes were written not only after lectures I gave, but after long conversations we had, many times, in my flat, and also a few days you spent in my house in the south of France, where, for at least 10 hours everyday I explained in detail to you my work on fibered categories and corrected many mistakes you made in first drafts of that paper. Nevertheless, for the sake of the people on the category list,to whom this message is also addressed, I shall answer your questions an remarks. Let p: X --> S be a surjective group homomorphism. It is a fibration, and a cleavage is a section of p (in Set). This was explicitly noted by Grothendieck more than 50 years ago! Does such a p come equipped with a cleavage? Take for p the morphim : R --> R/Z of the reals on the circle. Suppose I were to teach periodic functions, i.e functions with domain R which factor through R/Z. Wouldn't it be ridiculous to use a section of p ? Which one by the way? Take the theorem : The composite of two fibrations is a fibration. Does it need cleavages, i.e. AC for classes, to be proved? Of course, if you are cleavage fan, as you seem to be, you can add that, given cleavages of p and q one gets an associated cleavage of pq. Let's look at an important example,namely categories S with pull backs, not with choice of pull backs mind you. This is a first order notion, saying that : for every cospan of S there exists a universal span making the obvious square commutative. Then, without AC, you can prove that the functor Codom: S^2 --> S is a fibration. And again, if you are cleavage happy, add that a cleavage of this fibration, if it exists, (I'm not assuming AC) is a choice of pullbacks in S. I could multiply the examples. But let's look at an important question. Suppose you prove an intrinsic result about fibrations, using cleavages, in principle you'd have to see what happens when you change cleavages. And don't wave your hands and tell me that, for formal 2-categorical reasons, the result is obvious. I'll believe you only when you write a precise metatheorem which covers ALL the cases. You are convinced, and I am convinced, and everybody is convinced that such a metatheorem is not necessary. But that is NOT A PROOF ! And why are you convinced? Because, even if you say the contrary, deep in your mind you KNOW that intrinsic properties of fibrations AND cartesian functors should not refer to cleavages. Let me insist on the fact that the mythic metatheorem should also cover cartesian functors F: X --> X' where you change the cleavages of both X and X' Of course the theorem I mentioned in my mail on pre foliations, applies to fibrations and gives new results in that case. But this theorem is true for F: X --> X' where X is a prefoliation hence, even with AC, has no cleavage, and X' is an arbitrary category over S, i.e. has even less cleavages than X. In order not to make this mail too long I have not, but I should have, mentioned internalization where cleavages are even more problematic. Best to all, Jean Le 30 juil. 2014 à 17:06, Thomas Streicher a écrit :
Dear Jean,
of course, you are right when emphasizing that one need choice for classes to endow an "anonymous" fibration with a cleavage. But that applies also to catgeories with say binary products. One needs choice for classes in order to choose a product cone for every pair of objects. In many instances, however, categories come together with a choice of products and fibrations come together with a choice of a cleavage.
For example Set comes with a choice of a cleavage. Fibrations arising from internal categories are even split. Many constructions on fibrations allow one to choose a cleavage given cleavages for the arguments. Do you know of any construction on fibrations which is not "cleavage preserving" in this sense?
Of course, one should not require cartesian functors to preserve cleavages just as one should not require functors to preserve chosen products.
Thomas
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear all, I prefer fibrations over fibrations furnished with a cleavage (indexed categories) many times for reasons purely pragmatical mixed with an aesthetic philosophy. Suppose you are dealing with fibrations where a canonical cleavage is present, suppose even that these cleavages come first and that the fibration is just a conceptual context around them. Even in this case, faced to the need to produce a proof, if you succeed to find one without utilizing the cleavages, you will have something much nicer than the cleavage arguing. It will also give you a deeper understanding and a truthful light on the situation. Suppose you do not care about foundations, axiom of choice, or things of that sort. You should still prefer fibrations. They are simpler, more to the point, and CERTAINLY AHEAD IN THE PROGRESS OF MATHEMATICS. NOTE: I wonder why so many people are so happy working with pull-backs and pull-back preserving functors (*) without even thinking in introducing a choice of pullbacks, and when it comes to fibrations, feel the need to introduce and work with cleavages. (*) for example even when dealing with the category of sets (or categories whose objects have an underlying set), which are plenty of choices of pull-backs, for example, inverse image of a subset, the standard construction as a subset of the set of pairs, etc. We precisely teach in category theory courses that you should not work with any particular choice between the choices. We all agree that it is neither necessary not good to choose a choice between all possible choices. This is precisely the progress that represents category theory thinking over set theory thinking. See for example, in the dawn of category theory, the considerations of Mac Lane concerning the fact that a quotient of a quotient of a group is not a quotient (as it is still now taught in algebra courses, category theory thinking has not arrived there yet). You may say that the choice of a cleavage is at a different level than all this, but, essentially, deep down, for me it is the same. There is an old way of thinking (as Grothendieck said, SLN224, page 193) that hesitates in face of fibrations and prefer to work with a chosen cleavage. On 30/07/14 14:56, Jean B?nabou wrote:
Dear Thomas,
I am a bit surprised that you, of all people, should defend cleavages, i.e. indexed categories. As far as I remember, there not many of them in the notes you wrote on Fibered categories a la Benabou. I remind you that these notes were written not only after lectures I gave, but after long conversations we had, many times, in my flat, and also a few days you spent in my house in the south of France, where, for at least 10 hours everyday I explained in detail to you my work on fibered categories and corrected many mistakes you made in first drafts of that paper. Nevertheless, for the sake of the people on the category list,to whom this message is also addressed, I shall answer your questions an remarks.
Let p: X --> S be a surjective group homomorphism. It is a fibration, and a cleavage is a section of p (in Set). This was explicitly noted by Grothendieck more than 50 years ago! Does such a p come equipped with a cleavage? Take for p the morphim : R --> R/Z of the reals on the circle. Suppose I were to teach periodic functions, i.e functions with domain R which factor through R/Z. Wouldn't it be ridiculous to use a section of p ? Which one by the way?
Take the theorem : The composite of two fibrations is a fibration. Does it need cleavages, i.e. AC for classes, to be proved? Of course, if you are cleavage fan, as you seem to be, you can add that, given cleavages of p and q one gets an associated cleavage of pq.
Let's look at an important example,namely categories S with pull backs, not with choice of pull backs mind you. This is a first order notion, saying that : for every cospan of S there exists a universal span making the obvious square commutative. Then, without AC, you can prove that the functor Codom: S^2 --> S is a fibration. And again, if you are cleavage happy, add that a cleavage of this fibration, if it exists, (I'm not assuming AC) is a choice of pullbacks in S.
I could multiply the examples. But let's look at an important question. Suppose you prove an intrinsic result about fibrations, using cleavages, in principle you'd have to see what happens when you change cleavages. And don't wave your hands and tell me that, for formal 2-categorical reasons, the result is obvious. I'll believe you only when you write a precise metatheorem which covers ALL the cases. You are convinced, and I am convinced, and everybody is convinced that such a metatheorem is not necessary. But that is NOT A PROOF ! And why are you convinced? Because, even if you say the contrary, deep in your mind you KNOW that intrinsic properties of fibrations AND cartesian functors should not refer to cleavages. Let me insist on the fact that the mythic metatheorem should also cover cartesian functors F: X --> X' where you change the cleavages of both X and X'
Of course the theorem I mentioned in my mail on pre foliations, applies to fibrations and gives new results in that case. But this theorem is true for F: X --> X' where X is a prefoliation hence, even with AC, has no cleavage, and X' is an arbitrary category over S, i.e. has even less cleavages than X.
In order not to make this mail too long I have not, but I should have, mentioned internalization where cleavages are even more problematic.
Best to all, Jean
Le 30 juil. 2014 ? 17:06, Thomas Streicher a ?crit :
Dear Jean,
of course, you are right when emphasizing that one need choice for classes to endow an "anonymous" fibration with a cleavage. But that applies also to catgeories with say binary products. One needs choice for classes in order to choose a product cone for every pair of objects. In many instances, however, categories come together with a choice of products and fibrations come together with a choice of a cleavage.
For example Set comes with a choice of a cleavage. Fibrations arising from internal categories are even split. Many constructions on fibrations allow one to choose a cleavage given cleavages for the arguments. Do you know of any construction on fibrations which is not "cleavage preserving" in this sense?
Of course, one should not require cartesian functors to preserve cleavages just as one should not require functors to preserve chosen products.
Thomas
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Eduardo, I agree with many things in your message, but I think you are taking your argument too far. Talking of pullbacks you say:
We precisely teach in category theory courses that you should not work with any particular choice between the choices.
I agree that it is better to avoid such a choice when possible. Yet you cannot define a bicategory of spans without assuming that such a choice has been made; in the same way as you cannot define the (good) monoidal structure of Ab without recurring to a choice of tensor products. Such a situation, we all know, generally arises in non-strict bicategories (and monoidal categories, in particular). Unless you want to redefine bicategories replacing the composition of arrows with an existence property. I still prefer working with a choice (eg of pullbacks) to such a complicated structure. Best regards Marco [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Related to Marco's point: In order to define the category Set, we have to define Set(X,Y) for all sets X and Y. There are many isomorphic options, but to get a category we have to choose one. Now replace "category" by "category with distinguished binary products and exponentials.". We shall then have to choose a particular implementation of X x Y and X -> Y. Why do some people find this philosophically objectionable? How is it worse than choosing Set(X,Y)? (Personally, I'd be inclined to make the same choice for X -
Y as for Hom(X,Y).)
Paul On 2 Aug 2014, at 11:58, Marco Grandis wrote:
Dear Eduardo,
I agree with many things in your message, but I think you are taking your argument too far. Talking of pullbacks you say:
We precisely teach in category theory courses that you should not work with any particular choice between the choices.
I agree that it is better to avoid such a choice when possible. Yet you cannot define a bicategory of spans without assuming that such a choice has been made; in the same way as you cannot define the (good) monoidal structure of Ab without recurring to a choice of tensor products. Such a situation, we all know, generally arises in non-strict bicategories (and monoidal categories, in particular).
Unless you want to redefine bicategories replacing the composition of arrows with an existence property. I still prefer working with a choice (eg of pullbacks) to such a complicated structure.
Best regards
Marco
-- Paul Blain Levy School of Computer Science, University of Birmingham +44 121 414 4792 http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Marco Grandis <grandis@dima.unige.it> wrote in part:
Yet you cannot define a bicategory of spans without assuming that such a choice has been made; in the same way as you cannot define the (good) monoidal structure of Ab without recurring to a choice of tensor products.
A monoidal structure on a category C is a functor C x C -> C, an object of C (aka a functor 1 -> C), and various natural transformations satisfying some equations. If by "functor" we mean an anafunctor, then no choice is needed. Presumably you are thinking along these lines when you write
Unless you want to redefine bicategories replacing the composition of arrows with an existence property.
My point is that anafunctors tell you automatically what to do. Better yet, working in HoTT tells you automatically what to do. All of this only looks complicated from a set-based perspective. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Toby, The theory of monoidal categories and bicategories is already written. I may be interested in working with them, even though it is unpleasant to recur to choice for most (non-strict) structures of these kinds. I have no interest in rewriting these theories in a different shape, using anafunctors or similar tools, or even study such variations if someone has given them. Of course other people may prefer the way you are saying. I just wanted to point out that there are many occasions where we are led to use choice - at least if we want to stay within 'classical' category theory, as expounded - say - in Mac Lane's text. Regards, Marco On 03/ago/2014, at 18.30, Toby Bartels wrote:
Marco Grandis <grandis@dima.unige.it> wrote in part:
Yet you cannot define a bicategory of spans without assuming that such a choice has been made; in the same way as you cannot define the (good) monoidal structure of Ab without recurring to a choice of tensor products.
A monoidal structure on a category C is a functor C x C -> C, an object of C (aka a functor 1 -> C), and various natural transformations satisfying some equations. If by "functor" we mean an anafunctor, then no choice is needed.
Presumably you are thinking along these lines when you write
Unless you want to redefine bicategories replacing the composition of arrows with an existence property.
My point is that anafunctors tell you automatically what to do.
Better yet, working in HoTT tells you automatically what to do. All of this only looks complicated from a set-based perspective.
--Toby
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Jean, It has not been my intention to defend indexed categories against fibered categories. I just wanted to say that it is sometimes "convenient" to use cleavages. First of all I would say that fibrations with cleavages are not the same as indexed categories. Firstly, because the coherence conditions for the maps chosen by the cleavage are determined by the functor and do not have to be stated explicitly. Secondly, for fibrations with cleavages one can show that they are closed under composition which for indexed categories would be (close to) impossible. Nevertheless, I agree with you that it is in general preferable to formulate things in such a way that one avoids reference to cleavages as far as possible. Sometimes, however, this makes things a bit more complicated as I want to illustrate by the following example. Chevalley's original formulation of his famous condition for internal sums is much more convenient than the one usually found in the literature. An analogue can be formulated for internal products (as in section 7 of my Notes on Fibrations you have mentioned). In Th.7.1 of loc.cit. I have given a characterization of fibration having internal products which avoids any reference to cleavages. This appears to me a bit clumsy and there is a version using cleavages which essentially says that reindexing functors have right adjoints and that their counits are preserved by reindexing up to isomorphism. This latter version is useful when checking that a given fibration has internal products as is necessary e.g. when constructing models of type theory. But in any case I think that conceptually it is preferable to define P having internal products as P^op having internal sums. This formulation is free from cleavages but for using it in concrete instances it is sometimes useful to have equivalent formulations available which don't abhor making reference to reindexing functors and thus to cleavages. But this is a pragmatic issue and not a foundational issue. The same applies to linear algebra. If it is convenient to refer to bases of vector spaces I am not against doing so. But, of course, it would be stupid to require all vector spaces to be endowed with bases. For this reason I want to CORRECT the point of view of my previous mail. One should not require all fibrations to be endowed with a cleavage. Rather one should be open to accept some strong choice principles on the meta level which allow one to assume the existence of cleavages whenever convenient. But, definitely, one should give most definitions and constructions in a way not referring to cleavages. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 03/08/14 06:22, Thomas Streicher wrote:
One should not require all fibrations to be endowed with a cleavage. Rather one should be open to accept some strong choice principles on the meta level which allow one to assume the existence of cleavages whenever convenient. But, definitely, one should give most definitions and constructions in a way not referring to cleavages.
I completely agree with this, it is my own feeling beautifully and synthetically expressed. I only add: "... most definitions and constructions AND proofs in a way ..." Also, that many times the use of cleavages may seem convenient, when in fact it is not. And I also put in the same bag the equivalences (which in general have only one direction. Then one should proceed using the fully-faithfulness and essentially surjectiveness whenever possible, and be free to assume the existence of quasi-inverses only if it is necessary. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (6)
-
Eduardo J. Dubuc -
Jean Bénabou -
Marco Grandis -
Paul Levy -
Thomas Streicher -
Toby Bartels