* Re terminology: @ 2010-05-19 10:38 Ronnie Brown 2010-05-20 7:58 ` soloviev ` (4 more replies) 0 siblings, 5 replies; 34+ messages in thread From: Ronnie Brown @ 2010-05-19 10:38 UTC (permalink / raw) To: categories Peter Sellinger writes recently: --------------------------------------------------- I think this is a very apt illustration of what happens if a term with an existing meaning is redefined to mean something else. Henceforth it is impossible for anybody to use the term (with either meaning) without first giving a definition. --------------------------------------------------- I completely agree. My own problem is with term `infinity groupoid' which is used to describe something which is not even a groupoid, and whose use seems to me to militate against the understanding of what has been achieved with the original and much earlier definition. I once asked Gian-Carl Rota about such change of terminology, in connection with a refereeing job, and he agreed that mathematicians are used to creating confusion in this way. There are two easy tendencies: one is to use an old name in a quite different way, and the other is to use a new name for an old idea, so that the use of the old term looks old fashioned, and a lot of work may be consigned to the dustbin of history, becoming not easy of access for new students. It seems to be an example of these confusions is the way the simplicial singular complex of a space is called an infinity-groupoid, even the `fundamental infinity groupoid', when what seems to be referred to is that it is a Kan complex, i.e. satisfies the Kan extension condition, studied since 1955. The new term sounds like `dressing up' an old idea to look new. My personal objection to this change of terminology (i.e. axe to grind!) is that this distracts from studying the not so simple proofs that strict higher homotopical structures exist, which mainly are for structured spaces (in particular filtered spaces (Brown/Higgins, Ashley), n-cubes of spaces (Loday), and more recently smooth spaces (Faria Martins/Picken)). The analysis and comparison of these uses should be made. It was certainly a relief to Philip and I that we could do something with filtered spaces which we could not do for the absolute case; the significance of the fact that these constructions work and lead to specific calculations should be thought about. The term `higher dimensional group theory' which was published in a paper with that title in 1982 was intended to suggest developing higher groupoid theory and its relations to homotopy theory in the spirit of group theory, which meant specific constructions relevant to geometry and calculations, even computer calculations, of many examples, in which actual numbers arise as a test of and examples of the general theory, and in which some aspects of group theory are sensibly seen as better represented in the higher dimensional theory; and example of this is the nonabelian tensor product of groups, where group theorists have found lots of pickings. I am not sure how these terminological problems will be resolved, and I know the term (\infty,n)-groupoid has been well used recently but the problem of relation to the older ideas, which have had a certain success, should be recognised. Ronnie Brown [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re terminology: 2010-05-19 10:38 Re terminology: Ronnie Brown @ 2010-05-20 7:58 ` soloviev 2010-05-20 19:53 ` terminology Eduardo J. Dubuc 2010-05-20 22:15 ` Re terminology: Joyal, Andre 2010-05-20 11:58 ` Urs Schreiber ` (3 subsequent siblings) 4 siblings, 2 replies; 34+ messages in thread From: soloviev @ 2010-05-20 7:58 UTC (permalink / raw) To: Ronnie Brown My personal opinion is that this process is very much influenced by the pressure of "bibliometry", "impact factors" and other "modern trends" - people often not very scrupulously invent and reinvent terminology to be better cited, and, conscious or not, it often very much smells of imposture. Sergei Soloviev > Peter Sellinger writes recently: > > --------------------------------------------------- > > I think this is a very apt illustration of what happens if a term with > an existing meaning is redefined to mean something else. Henceforth it > is impossible for anybody to use the term (with either meaning) > without first giving a definition. > > --------------------------------------------------- > > I completely agree. My own problem is with term `infinity groupoid' which > is used to describe something which is not even a groupoid, and whose use > seems to me to militate against the understanding of what has been > achieved with the original and much earlier definition. I once asked > Gian-Carl Rota about such change of terminology, in connection with a > refereeing job, and he agreed that mathematicians are used to creating > confusion in this way. > > There are two easy tendencies: one is to use an old name in a quite > different way, and the other is to use a new name for an old idea, so that > the use of the old term looks old fashioned, and a lot of work may be > consigned to the dustbin of history, becoming not easy of access for new > students. > > It seems to be an example of these confusions is the way the simplicial > singular complex of a space is called an infinity-groupoid, even the > `fundamental infinity groupoid', when what seems to be referred to is that > it is a Kan complex, i.e. satisfies the Kan extension condition, studied > since 1955. The new term sounds like `dressing up' an old idea to look > new. My personal objection to this change of terminology (i.e. axe to > grind!) is that this distracts from studying the not so simple proofs that > strict higher homotopical structures exist, which mainly are for > structured spaces (in particular filtered spaces (Brown/Higgins, Ashley), > n-cubes of spaces (Loday), and more recently smooth spaces (Faria > Martins/Picken)). The analysis and comparison of these uses should be > made. It was certainly a relief to Philip and I that we could do something > with filtered spaces which we could not do for the absolute case; the > significance of the fact that these constructions work and lead to > specific calculations should be thought about. > > The term `higher dimensional group theory' which was published in a paper > with that title in 1982 was intended to suggest developing higher groupoid > theory and its relations to homotopy theory in the spirit of group theory, > which meant specific constructions relevant to geometry and calculations, > even computer calculations, of many examples, in which actual numbers > arise as a test of and examples of the general theory, and in which some > aspects of group theory are sensibly seen as better represented in the > higher dimensional theory; and example of this is the nonabelian tensor > product of groups, where group theorists have found lots of pickings. > > I am not sure how these terminological problems will be resolved, and I > know the term (\infty,n)-groupoid has been well used recently but the > problem of relation to the older ideas, which have had a certain success, > should be recognised. > > Ronnie Brown > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-05-20 7:58 ` soloviev @ 2010-05-20 19:53 ` Eduardo J. Dubuc 2010-05-20 22:15 ` Re terminology: Joyal, Andre 1 sibling, 0 replies; 34+ messages in thread From: Eduardo J. Dubuc @ 2010-05-20 19:53 UTC (permalink / raw) To: Categories soloviev@irit.fr wrote: > My personal opinion is that this process is very much influenced > by the pressure of "bibliometry", "impact factors" and other "modern > trends" - people often not very scrupulously invent and reinvent > terminology to be better cited, and, conscious or not, it often very > much smells of imposture. > > Sergei Soloviev I agree with this. But it should be clear that many times it is not conscious, but certainly it often smells of imposture. Other times it smells of excessive logic and formalism. Concerning "injective" I see no problem at all that some times injective means (1-1) and other times it means the dual of projective. Where is the problem !!, the context always tells you which meaning it is being used. e.d. [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re terminology: 2010-05-20 7:58 ` soloviev 2010-05-20 19:53 ` terminology Eduardo J. Dubuc @ 2010-05-20 22:15 ` Joyal, Andre 1 sibling, 0 replies; 34+ messages in thread From: Joyal, Andre @ 2010-05-20 22:15 UTC (permalink / raw) To: soloviev, Ronnie Brown, urs.schreiber Dear Urs and Ronnie, Sergei Soloviev wrote: >My personal opinion is that this process is very much influenced >by the pressure of "bibliometry", "impact factors" and other "modern >trends" - people often not very scrupulously invent and reinvent >terminology to be better cited, and, conscious or not, it often very >much smells of imposture. Urs Schreiber wrote: >It seems to follow the well established terminology in higher category >theory, which proceeds: category, 2-category, 3-category, .... >infinity-category and groupoid, 2-groupoid, 3-groupoid, ... >infinity-groupoid. I introduced the terminology "quasi-category" as an alternative name for weak Kan complexes because I wanted to suggest that the theory of these objects was closer to category theory than to the theory of Kan complexes. For example, the notion of an initial object in a quasi-category is very important, like that of initial object in a category. But only a contractible Kan complex can have an initial object. The theory of quasi-categories turns out to be amazingly close to category theory despite the fact that its natural setting is simplicial homotopy theory. The name "quasi-category" is for me less frightening than "infinity-category" which has the name of God into it. More seriously, why should we attach the prefix "infinity" to an object which is no more endless than the set of natural numbers, or the set of rational numbers, or the simplicial category Delta? The terminology could be reflecting the (relative) failure of the algebraic approach to higher categories. An algebraic description of homotopy type of the 2-sphere is missing and it could be endless. But the 2-sphere is easy to describe simplicially: S^2= Delta[2]/partial \Delta[2] Best, André -------- Message d'origine-------- De: categories@mta.ca de la part de soloviev@irit.fr Date: jeu. 20/05/2010 03:58 À: Ronnie Brown Objet : categories: Re terminology: My personal opinion is that this process is very much influenced by the pressure of "bibliometry", "impact factors" and other "modern trends" - people often not very scrupulously invent and reinvent terminology to be better cited, and, conscious or not, it often very much smells of imposture. Sergei Soloviev [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re terminology: 2010-05-19 10:38 Re terminology: Ronnie Brown 2010-05-20 7:58 ` soloviev @ 2010-05-20 11:58 ` Urs Schreiber [not found] ` <AANLkTikre9x4Qikw0mqOl1qZs9DDSkcBu3CXWA05OTQT@mail.gmail.com> ` (2 subsequent siblings) 4 siblings, 0 replies; 34+ messages in thread From: Urs Schreiber @ 2010-05-20 11:58 UTC (permalink / raw) To: Ronnie Brown Dear Ronnie Brown, you write:: > My own problem is with term `infinity groupoid' which > is used to describe something which is not even a groupoid, It seems to follow the well established terminology in higher category theory, which proceeds: category, 2-category, 3-category, .... infinity-category and groupoid, 2-groupoid, 3-groupoid, ... infinity-groupoid. > It seems to be an example of these confusions is the way the simplicial > singular complex of a space is called an infinity-groupoid, even the > `fundamental infinity groupoid', when what seems to be referred to is that > it is a Kan complex, i.e. satisfies the Kan extension condition, studied > since 1955. The notion of Kan complex is one model for the notion of infinity-groupoid. There are other, equivalent models. And there are models that model stricter subclasses of infinity-groupoids, such as those you are famous for having studied. Part of the point of saying "infinity-groupoid" instead of "Kan complex" or else is to amplify the general notion over its concrete implementation. > this distracts from studying the not so simple proofs that strict > higher homotopical structures exist, I don't quite see why the term should distract from or otherwise diminish accomplishments made in the study of strict infinity-groupoids. On the contrary, to my mind the general theory of infinity-groupoids puts many of these constructions into the full perspective of higher category theory and thereby amplifies their relevance. > I know the term (\infty,n)-groupoid has been well used recently Not quite: the term (infinity,n)-category is used to denote an infinity-category in which all k-morphisms for k greater than n are equivalences. So an infinity-groupoid is an (infinity,0)-category. This terminology was not invented in order to hide anybody's previous accomplishments. On the contrary, I think, this terminology follows established use in higher category theory and serves to nicely organize past, present and future insights into higher category theory in a coherent picture. I am hoping that eventually we find a constructive way of thinking about these things, where past insights are seen as fitting into the beautiful picture of higher category theory that has recently been emerging, and are not seen to be in conflict with them. Here is an example I quite like: in the context of (infinity,1)-category theory Jacob Lurie gave an entirely intrinsic category-theoretic definition of (infinity,1)-sheaves, also known as infinity-stacks: these are infinity-groupoid valued presheaves satisfying a suitable descent condition. Working backwards from the abstract higher category-theoretic definition of these, one can work out how this notion matches related models that were previously investigated. Among these are two main strands: 1) the homotopical structures/model category structures on categories of ordinary presheaves with values in simplicial sets, as developed by Brown, Joyal, Jardine, Dugger and others. 2) The notion of presheaves with values in strict infinity-groupoids / strict omega-groupoids, as originally conceived by John Roberts and then formalized by Ross Street and others. One might worry that both these decade-old developments might not harmonize with the intrinsic higher-categorical notion of (infinity,1)-sheaf. But the opposite is true: one finds that they are neatly subsumed in the abstract definition and conversely provide concrete workable models for the abstract notion. For point 1) this is proven in Jacob Lurie's book on higher topos theory: the Joyal/Jardine model structure models precisely those (infinity,1)-sheaves which are "hypercomplete". More generally, the left Bousfiled localization of the model structure on simplicial presheaves at Cech nerves models (infinity,1)-sheaves. For point 2) this has been proven by Dominic Verity, following a conjecture I made: one can show that under mild conditons, under the inclusion of strict omega-groupoids / strict infinity-groupoids into all infinity-groupoids, the Roberts-Street notion of descent for such strict oo-groupoid sheaves does model the abstractly found (infinity,1)-sheaf condition. http://ncatlab.org/nlab/show/Verity+on+descent+for+strict+omega-groupoid+valued+presheaves So this means now not a diminishing but a considerable increase in value of the old work on presheaves with values in strict infinity-groupoids / omega-groupoids: since it embeds these constructions into a powerful abstract theory, we now conversely have all the abstract tools and insights available to study and use the former. I have been using this embeddingg of strict oo-groupoid valued oo-stacks into all oo-stacks quite a lot in my research, originally starting with the observation that the BCSS-model of the string 2-group realizes it as a strict 2-groupoid valued stack on Diff, which is quite useful for some applications. All along I have greatly benfitted by having your book and nonabelian algebraic topology next to me, together with Ross Street's articles on descent, and at the same time having Higher Topos Theory on the table. I find that that these two aspects interact very nicely, and I was therefore a bit saddened by hearing what sounded like accusations that new developments in higher category theory try to intentionally diminish previous development. I think math is a win-win game, not a competition: one person's insight does not dimish the other person's insight, but both increase each other's value. I am dearly hoping that those who practiced aspects of higher category theory for so long see the new developments not as in conflictt with their work, but as a beautiful blossoming of the theory that they started developing. Because it is true. Best regards, Urs [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
[parent not found: <AANLkTikre9x4Qikw0mqOl1qZs9DDSkcBu3CXWA05OTQT@mail.gmail.com>]
* Re terminology: [not found] ` <AANLkTikre9x4Qikw0mqOl1qZs9DDSkcBu3CXWA05OTQT@mail.gmail.com> @ 2010-05-21 17:00 ` Ronnie Brown 2010-05-22 19:40 ` Joyal, André [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5827@CAHIER.gst.uqam.ca> 0 siblings, 2 replies; 34+ messages in thread From: Ronnie Brown @ 2010-05-21 17:00 UTC (permalink / raw) To: Urs Schreiber, categories Dear Urs, Thanks for your friendly and detailed reply. I should say that I also feel responsible for defending and advertising the work of my long time collaborator, Philip Higgins, without whom of course much of the work would not have got done, certainly not so quickly. His last contribution to maths was in 2005; I helped with the presentation of his TAC paper, but insisted that it showed `you know the lion from his claw', as all the ideas were his. He is happily playing the violin and making string instruments from bare blocks of wood! (That shows his craftmanship.) He remembers the project as very hard work but a lot of fun! You mention the process from category to infinity-category. Actually that was why we introduced the term infinity-category in 34. (with P.J. HIGGINS), ``The equivalence of $\infty$-groupoids and crossed complexes'', {\em Cah. Top. G\'eom. Diff.} 22 (1981) 371-386. See also: 33. (with P.J. HIGGINS), ``The equivalence of $\omega$-groupoids and cubical $T$-complexes'', {\em Cah. Top. G\'eom. Diff.} 22 (1981) 349-370. The paper [34] also gives a definition of what is now called (rightly) a globular set. I am curious to know whether there are earlier definitions of these terms. Joachim Lambek once asked me at a category theory meeting: `Why don't people from xxxx refer to these papers?' What could I say? People do write about 2-groupoids without referring to analogous work on crossed complexes. The points Andre makes are very interesting. In the 1970s we were very puzzled by the Kan condition, and still are, for the following reason. The fact that the simplicial singular complex of a space is a Kan complex is due to a fact about the models, namely a geometric simplex retracts onto all faces but one. So we can have in effect fillers for S(X) natural in X, by making choices on the models. Also these fillers are clearly related to multiple compositions of the remaining faces. The problem is that there is no unique choice of such retractions, nor is it clear what might be the relations between iterates of such fillers. These considerations led Keith Dakin to the notion of T-complex for his 1976 thesis; somehow `T-complex' has more recently become `complicial set', but nobody asked me. (Groan! Groan!) So it seems that the notion of quasi category as a weak Kan complex still has not captured something about the basic example; but how to repair that is quite unclear. As I have said before, we found it necessary for certain aspects to work cubically, as expressing in a manageable way `algebraic inverses to subdivision', and also to get monoidal closed structures. Again, it is not clear how to capture axiomatically the properties of the cubical singular complex, as some kind of weak cubical infinity groupoid. I have been unable to cope with the complications of multiple compositions in globular or simplicial terms. Is there an operad view of the cubical case? I have no wish to hold things up or disparage work developing these ideas in different ways, just the contrary, and indeed I wrote that I was thinking of higher dimensional group theory, rather than category theory. The contrast and relations between such views could, perhaps should, be illuminating. We are putting a photo from Macquarie of John Robinson's sculpture `Journeys' as a frontispiece to the new book. Best wishes to all for the future of this great adventure. Ronnie Urs Schreiber wrote: > Dear Ronnie Brown, > > you write:: > > >> My own problem is with term `infinity groupoid' which >> is used to describe something which is not even a groupoid, >> > > It seems to follow the well established terminology in higher category > theory, which proceeds: category, 2-category, 3-category, .... > infinity-category and groupoid, 2-groupoid, 3-groupoid, ... > infinity-groupoid. > > >> It seems to be an example of these confusions is the way the simplicial >> singular complex of a space is called an infinity-groupoid, even the >> `fundamental infinity groupoid', when what seems to be referred to is that >> it is a Kan complex, i.e. satisfies the Kan extension condition, studied >> since 1955. >> > > The notion of Kan complex is one model for the notion of > infinity-groupoid. There are other, equivalent models. And there are > models that model stricter subclasses of infinity-groupoids, such as > those you are famous for having studied. Part of the point of saying > "infinity-groupoid" instead of "Kan complex" or else is to amplify the > general notion over its concrete implementation. > .... [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re terminology: 2010-05-21 17:00 ` Ronnie Brown @ 2010-05-22 19:40 ` Joyal, André [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5827@CAHIER.gst.uqam.ca> 1 sibling, 0 replies; 34+ messages in thread From: Joyal, André @ 2010-05-22 19:40 UTC (permalink / raw) To: Ronnie Brown, Urs Schreiber, categories Dear Urs and Ronnie, As you know, there are important differences between category theory and classical algebra. One lies in the fact that equivalent categories are considered to be the "same", even if when they are not isomorphic. In category theory most constructions are yielding an object which is not unique, but only unique up to some kind of equivalence, at best unique up to a unique isomorphism. The general idea seems to be that an object is well defined if its different incarnations are connected by a contractible network of equivalences. It seems to me that the challenge of higher dimensional algebra is to learn how to handle constructions whose output are not unique but only unique only up to a contractible network. Of course, we may decide to replace these constructions by ones producing a truly unique object, but the replacement seems often artificial. For example, we may decide to choose a representative for the cartesian product of every pair of objects in a category. We are then lead to distinguish between two kinds of product preserving functors. The functors preserving the product strictly are given a role, but this seems artificial to me. I do not want to be negative about the idea of turning higher dimensional algebra into ordinary algebra, because we may learn something in the process. Also, Quillen homotopical algebra can be regarded as a method for reducing higher categorical and homotopy algebra to ordinary categorical algebra. However, there was a real gain in moving from a purely algebraic description of higher categories to one based on simplicial sets and homotopical algebra. The category of quasi-categories is cartesian closed, a property which appears to be false for the category of fibrant objects in the "algebraic" models. This is also true for the category of n-quasi-category (Rezk). Best, André -------- Message d'origine-------- De: categories@mta.ca de la part de Ronnie Brown Date: ven. 21/05/2010 13:00 À: Urs Schreiber; categories@mta.ca Objet : categories: Re terminology: Dear Urs, Thanks for your friendly and detailed reply. I should say that I also feel responsible for defending and advertising the work of my long time collaborator, Philip Higgins, without whom of course much of the work would not have got done, certainly not so quickly. His last contribution to maths was in 2005; I helped with the presentation of his TAC paper, but insisted that it showed `you know the lion from his claw', as all the ideas were his. He is happily playing the violin and making string instruments from bare blocks of wood! (That shows his craftmanship.) He remembers the project as very hard work but a lot of fun! You mention the process from category to infinity-category. Actually that was why we introduced the term infinity-category in 34. (with P.J. HIGGINS), ``The equivalence of $\infty$-groupoids and crossed complexes'', {\em Cah. Top. G\'eom. Diff.} 22 (1981) 371-386. See also: 33. (with P.J. HIGGINS), ``The equivalence of $\omega$-groupoids and cubical $T$-complexes'', {\em Cah. Top. G\'eom. Diff.} 22 (1981) 349-370. ........ [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
[parent not found: <B3C24EA955FF0C4EA14658997CD3E25E370F5827@CAHIER.gst.uqam.ca>]
* Re: terminology [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5827@CAHIER.gst.uqam.ca> @ 2010-05-22 21:43 ` Ronnie Brown [not found] ` <4BF84FF3.7060806@btinternet.com> 1 sibling, 0 replies; 34+ messages in thread From: Ronnie Brown @ 2010-05-22 21:43 UTC (permalink / raw) To: André Dear André There seems to me to be a tremendous amount of great work going on higher category theory, but when you write ----------------------------------------------------- One lies in the fact that equivalent categories are considered to be the "same", even if [or] when they are not isomorphic. ----------------------------------------- this seems to go against the grain of what I have been doing in groupoids since I decided they were valuable in about 1965! It sounds like the old canard `groupoids reduce to groups', so there must be some confusion in my mind on what you are saying. One thing that took me a while to realise was that it was not enough to study the fundamental groupoid or a fundamental group but one needed to consider intermediate cases, namely the fundamental groupoid on a set of base points chosen according to the geometry at hand. (`Algebraic topology' has not understood this it seems.) The vertices of a groupoid give a spatial component to group theory, a kind of geography, and sometimes, even often, that is needed to model the geometry. So for example it is useful to replace the trefoil group which has 2 generators x,y and one relation x^2=y^3 by the trefoil groupoid which is the double mapping cylinder (homotopy pushout) in groupoids of the two maps Z \to Z, given by squaring and cubing. So we add an extra groupoid generator iota on different vertices which turns x^2 into y^3. This corresponds to the double mapping construction to give a CW-complex. So groupoids give the strict algebra of keeping the information which makes things the same. In higher dimensions we want not just commutative diagrams but control of the ways of filling these diagrams. If the diagram is a pentagon (as we all know does happen) I would want a pentagon as part of the geometry, and the only question is how to deal with multiple compositions of various such objects, and that was the aim of David Jones thesis on Polyhedral T-complexes. The point is that the pieces to be composable have to be all faces but one of a general poyhedral `horn', the process of composing them is the filler of the horn, and the composite of the pieces is the remaining face of the filler. (It was not attempted to do this in category rather than groupoid terms, and that is still a mystery!) So you can see I have long been very sympathetic to using the Kan condition for describing algebraic or structural objects, but find the simplicial approach too awkward (for me, of course; I found the way Nick Ashley coped with that was amazing). I do not want to consider equivalent groupoids the same, as I may want to use the spatial components to describe how they might be glued together. It is partly the old tag of not throwing away information till the last possible moment. On the other hand, some computations are best done at the strict level, rather than the weak one. I mention here the rotations in my paper: ``Higher dimensional group theory'', in {\em Low dimensional topology}, London Math Soc. Lecture Note Series 48 (ed. R. Brown and T.L. Thickstun, Cambridge University Press, 1982), pp. 215-238. (see also a fuller exposition in the new book on Nonabelian algebraic topology), which would seem to be more difficult to write out at the lax level. The fact that the strict calculations imply the existence of certain homotopies is part of the interest. So in the work with Higgins a Kan fibration - from the singular filtered complex of a filtered space to the quotient to give a strict structure - ties in the lax and the strict in a necessary way for the theory and calculations. I am really searching for points of agreement. Best regards Ronnie [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
[parent not found: <4BF84FF3.7060806@btinternet.com>]
* Re: terminology [not found] ` <4BF84FF3.7060806@btinternet.com> @ 2010-05-22 22:44 ` Joyal, André 2010-05-23 15:39 ` terminology Colin McLarty 0 siblings, 1 reply; 34+ messages in thread From: Joyal, André @ 2010-05-22 22:44 UTC (permalink / raw) To: Ronnie Brown Dear Ronnie, I totally agree with what you wrote. I wrote ------------------------------------------------------------ One lies in the fact that equivalent categories are considered to be the "same", ------------------------------------------------------------- I was careful not to write ------------------------------------------------------------ One lies in the fact that equivalent categories are considered to be the same, ------------------------------------------------------------- Sorry for not been clear enough. I hope this settle our apparent disagreement. Best, André -------- Message d'origine-------- De: Ronnie Brown [mailto:ronnie.profbrown@btinternet.com] Date: sam. 22/05/2010 17:43 À: Joyal, André Cc: Urs Schreiber; categories@mta.ca Objet : Re: RE : categories: Re terminology: Dear André There seems to me to be a tremendous amount of great work going on higher category theory, but when you write ----------------------------------------------------- One lies in the fact that equivalent categories are considered to be the "same", even if [or] when they are not isomorphic. ----------------------------------------- this seems to go against the grain of what I have been doing in groupoids since I decided they were valuable in about 1965! It sounds like the old canard `groupoids reduce to groups', so there must be some confusion in my mind on what you are saying. .... [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-05-22 22:44 ` terminology Joyal, André @ 2010-05-23 15:39 ` Colin McLarty 2010-05-24 13:42 ` equivalence terminology Paul Taylor ` (5 more replies) 0 siblings, 6 replies; 34+ messages in thread From: Colin McLarty @ 2010-05-23 15:39 UTC (permalink / raw) To: categories I have very much appreciated André's subtlety on this issue in conversation 2010/5/22 Joyal, André <joyal.andre@uqam.ca>: > I wrote > ------------------------------------------------------------ > One lies in the fact that equivalent categories are considered > to be the "same", > ------------------------------------------------------------- > I was careful not to write > ------------------------------------------------------------ > One lies in the fact that equivalent categories are considered > to be the same, > ------------------------------------------------------------- John Baez has written carefully on this point too. But not everyone is so careful and Ronnie has good reason to be concerned about a tendency to sweep away distinctions that do need to be made. Isomorphic categories too must be distinguished from one another, some times and for some purposes notably including all currently articulated versions of categorical foundations. Grothendieck gave it a fine nuance in Tohoku (p. 125) saying "Aucune des equivalences de categories qu'on rencontre en pratique n'est un isomorphisme (none of the equivalences one meets in practice are isomorphisms)." He stressed that we must distinguish isomorphisms from equivalences. Throughout that and later works he *constructs* a great many categories up to isomorphism, and not just up to equivalence. We do not meet these isomorphisms, we construct them -- and it is quite important that once constructed they are not merely equivalences. It is an interesting impulse in higher category theory to avoid identity in favor of isomorphism on the level of objects, and to avoid isomorphism in favor of equivalence on the level of categories. But so far as I know no one has yet articulated a way to avoid ever using identity of objects and identity of categories. Colin [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* equivalence terminology 2010-05-23 15:39 ` terminology Colin McLarty @ 2010-05-24 13:42 ` Paul Taylor 2010-05-24 15:53 ` we do meet isomorphisms of categories Marco Grandis ` (4 subsequent siblings) 5 siblings, 0 replies; 34+ messages in thread From: Paul Taylor @ 2010-05-24 13:42 UTC (permalink / raw) To: categories; +Cc: Colin McLarty Colin McLarty said, > It is an interesting impulse in higher category theory to avoid > identity in favor of isomorphism on the level of objects, and to avoid > isomorphism in favor of equivalence on the level of categories. But > so far as I know no one has yet articulated a way to avoid ever using > identity of objects and identity of categories. I am not going to get involved in higher category theory, but one setting in which (essentially) the question of identity of objects arises is in the interpretation of type theories in categories, where one needs to "choose" binary products, to give the simplest case. Any type theory has its category of contexts and substitutions (or classifying category). This has the categorical structure that is analogous to the type theoretic connectives, for example it's a CCC if we started with lambda calculus. Conversely, any category has its proper language, consisting of names for its objects and morphisms and various axioms. Without even having the structure, let alone a choice of it, the category is embedded in the category of contexts and substitutions of its proper language. If the category has choices for the structure then this embedding is a strong equivalence, ie with a pseudo-inverse, If it has the structure but not choices for it then it is a weak embedding - full, faithful and essentially surjective. The upshot of this is that, by replacing the category with a weakly equivalent one, you become able to talk about equality of objects, choices of product, etc. In other words, using the principle of interchangeability at a higher categorical level, we get the convenience of working with equality in the original structure. This is all explored in my book, "Practical Foundations of Mathematics". Paul [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* we do meet isomorphisms of categories 2010-05-23 15:39 ` terminology Colin McLarty 2010-05-24 13:42 ` equivalence terminology Paul Taylor @ 2010-05-24 15:53 ` Marco Grandis 2010-05-26 15:21 ` Toby Bartels ` (2 more replies) 2010-05-24 18:04 ` terminology Vaughan Pratt ` (3 subsequent siblings) 5 siblings, 3 replies; 34+ messages in thread From: Marco Grandis @ 2010-05-24 15:53 UTC (permalink / raw) To: categories On 23 May 2010, at 17:39, Colin McLarty wrote: > Grothendieck gave it a fine nuance in Tohoku (p. 125) saying "Aucune > des equivalences de categories qu'on rencontre en pratique n'est un > isomorphisme (none of the equivalences one meets in practice are > isomorphisms)." He stressed that we must distinguish isomorphisms > from equivalences. Throughout that and later works he *constructs* a > great many categories up to isomorphism, and not just up to > equivalence. We do not meet these isomorphisms, we construct them -- > and it is quite important that once constructed they are not merely > equivalences. We do meet isomorphisms of categories. Only, they are so obvious that sometimes we do not see them. For instance: The category of abelian groups is (canonically) isomorphic to the category of Z-modules. Groups are often defined as semigroups satisfying two conditions; but they can also be defined as sets with a zeroary operation, a unary operation and a binary operation satisfying certain axioms. Again, we have two isomorphic categories. An unbiased definition would give a third isomorphic category (and one can form infinitely many intermediate cases between the second and the third, likely of little interest). Algebras for the free group monad are directly linked with the unbiased version, yet not the same. Lattices (with 0 and 1) can be defined as ordered sets satisfying some conditions; or as sets with two binary operations satisfying other conditions; then one can add two zeroary operations;... Best regards Marco Grandis [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* we do meet isomorphisms of categories 2010-05-24 15:53 ` we do meet isomorphisms of categories Marco Grandis @ 2010-05-26 15:21 ` Toby Bartels 2010-05-27 9:29 ` Prof. Peter Johnstone [not found] ` <alpine.LRH.2.00.1005271007240.11352@siskin.dpmms.cam.ac.uk> 2 siblings, 0 replies; 34+ messages in thread From: Toby Bartels @ 2010-05-26 15:21 UTC (permalink / raw) To: categories Marco Grandis wrote in part: >Colin McLarty wrote: >>Grothendieck gave it a fine nuance in Tohoku (p. 125) saying "Aucune >>des equivalences de categories qu'on rencontre en pratique n'est un >>isomorphisme (none of the equivalences one meets in practice are >>isomorphisms)." He stressed that we must distinguish isomorphisms >>from equivalences. Throughout that and later works he *constructs* a >>great many categories up to isomorphism, and not just up to >>equivalence. We do not meet these isomorphisms, we construct them -- >>and it is quite important that once constructed they are not merely >>equivalences. >We do meet isomorphisms of categories. Only, they are so obvious that >sometimes we do not see them. >The category of abelian groups is (canonically) isomorphic to the category >of Z-modules. [further examples cut] In all of these examples (although obviously not all examples of isomorphisms), this is more than just an isomorphism; it's an isomorphism over Set. That is, it's an isomorphism in the slice category Cat/Set. It may seem beside the point, but in fact it is also important that it's an isomorphism in the full subcategory of Cat/Set whose objects are only the faithful functors to Set; call this the category Conc of CONCRETE categories. (So they are all concrete isomorphisms of concrete categories.) If you take a strictly speak-no-evil approach to category theory (perhaps even going so far as to found your mathematics on FOLDS), then it is impossible to state that two categories are isomorphic, because you must speak of equality of objects (or functors) to do this. In this approach, Cat and Cat/Set are bicategories but not categories. But it IS still possible to state that two concrete categories are isomorphic; the bicategory Conc is (up to equivalence) a locally posetal bicategory (so if you ignore the non-invertible transformations, it's a category). So it is possible (and necessary) to say, even when you speak no evil, that all of Marco's examples are concrete isomorphisms. So I agree that it is important that these are not mere equivalences, but I claim (playing the role of an equality-is-evil partisan) that what is important is not so much that they are isomorphisms as that they are concrete. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: we do meet isomorphisms of categories 2010-05-24 15:53 ` we do meet isomorphisms of categories Marco Grandis 2010-05-26 15:21 ` Toby Bartels @ 2010-05-27 9:29 ` Prof. Peter Johnstone [not found] ` <alpine.LRH.2.00.1005271007240.11352@siskin.dpmms.cam.ac.uk> 2 siblings, 0 replies; 34+ messages in thread From: Prof. Peter Johnstone @ 2010-05-27 9:29 UTC (permalink / raw) To: Marco Grandis Yes, we do meet isomorphisms of categories; my favourite algebraic example is the isomorphism between (Boolean algebras) and (Boolean rings), and another good one is the isomorphism between (finite T_0-spaces) and (finite partial orders). But there's a sense in which these isomorphisms are "accidental", arising from the fact that both categories are based on the same category of sets, and in practice (so far as I know) one never makes use of the fact that they are isomorphisms rather than mere equivalences. An even better example occurs in realizability. Some years ago on this list I queried the need for the condition "Sxy is defined for all x and y" in the definition of a partial combinatory algebra, and John Longley came up with a beautiful proof that, given a "weak pca" A which fails to satisfy this condition, there is a pca A' which does satisfy it, such that the category of A-valued assemblies is *identical* (not just equivalent, or even isomorphic) to the category of A'-valued assemblies. (Details can be found in Jaap van Oosten's book.) The accident arises in this case from the fact that A' happens to have the same underlying set as A. But, once again, I don't know of any use for the fact that the correspondence between the categories of assemblies is anything more than an equivalence. Peter Johnstone --------------------------- On Mon, 24 May 2010, Marco Grandis wrote: > We do meet isomorphisms of categories. Only, they are so obvious that > sometimes we do not see them. > > For instance: > > The category of abelian groups is (canonically) isomorphic to the > category > of Z-modules. > > Groups are often defined as semigroups satisfying two conditions; but > they > can also be defined as sets with a zeroary operation, a unary > operation and > a binary operation satisfying certain axioms. Again, we have two > isomorphic > categories. An unbiased definition would give a third isomorphic > category > (and one can form infinitely many intermediate cases between the second > and the third, likely of little interest). Algebras for the free > group monad are > directly linked with the unbiased version, yet not the same. > > Lattices (with 0 and 1) can be defined as ordered sets satisfying > some conditions; > or as sets with two binary operations satisfying other conditions; > then one can > add two zeroary operations;... > > Best regards > > Marco Grandis [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
[parent not found: <alpine.LRH.2.00.1005271007240.11352@siskin.dpmms.cam.ac.uk>]
* we do meet isomorphisms of categories [not found] ` <alpine.LRH.2.00.1005271007240.11352@siskin.dpmms.cam.ac.uk> @ 2010-05-27 10:08 ` Marco Grandis 2010-05-30 12:05 ` Joyal, André 0 siblings, 1 reply; 34+ messages in thread From: Marco Grandis @ 2010-05-27 10:08 UTC (permalink / raw) To: categories I should have mentioned another quite elementary example, that is perhaps more intriguing. Let us write Top for (topological spaces defined by open sets) and Top' for the isomorphic category (topological spaces defined by closed sets). Let (X, L) be a set X equipped with a complete sublattice L of its lattice of parts. Viewing it as on object of Top or Top' will interchange an Alexandrov topology for X with the opposite one, generally different. This says that - formally - we cannot think of these two isomorphic categories as being the same thing. Even if, of course, we do think that way, informally and in practice. I am not entirely convinced by a comment of Peter: "in practice (so far as I know) one never makes use of the fact that they are isomorphisms rather than mere equivalences". I am happy with the fact that, going from Top to Top' and back, we get the same space on the nose; this spares a lot of complications. Best regards Marco Grandis [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* we do meet isomorphisms of categories 2010-05-27 10:08 ` Marco Grandis @ 2010-05-30 12:05 ` Joyal, André 0 siblings, 0 replies; 34+ messages in thread From: Joyal, André @ 2010-05-30 12:05 UTC (permalink / raw) To: Marco Grandis, categories Dear Marco, Perhaps I can advocate the importance of isomorphism between categories. An equivalence between skeletal categories is necessarly an isomorphism. There are many examples of skeletal categories in mathematics. The category of matrices over a ring is skeletal. The category Delta in homotopy theory is also skeletal. The category Delta(+) of all finite ordinals and order preserving maps is an interesting example because, as everyones know, it is freely generated as a monoidal category by a monoid object. It is not free in the category of strict monoidal functors but free in the category of (strong) monoidal functors. There is of course another category, FatDelta(+), which is freely generated by a monoid object in the category of strict monoidal functors, but it is seldom used. The two categories FatDelta(+) and Delta(+) are equivalent, but the category Delta(+) is simpler because it is skeletal. The category of finite cardinals and all maps is also skeletal. It is freely generated by one object as a category with finite coproducts. It is also freely generated by a commutative monoid as a symmetric monoidal category. A category C is skeletal iff every equivalence A-->C has a section. This property characterises minimal models in algebraic topology. For example, a Kan complex Y is minimal iff every homotopy equivalence X-->Y, with X a Kan complex, has a section. Minimal models are important in topology. Sullivan's rational homotopy theory is essentially a technique for constructing minimal models of graded commutative algebras. The rational homotopy groups of a space can be read directly form its minimal Sullivan model. Minimal models exists in higher category theory too. Every quasi-category has a minimal model (should I say skeletal?). This not a property shared by all types of (infty,1)-categories. Some are better than others. For example, simplicial categories do not admit minimal models (in general). Strict monoidal categories do not admit minimal models either. This is because strict monoidal structures cannot be transported (in general) along equivalence of categories. Of course, non-strict monoidal structures can. There is an obstruction for transfering a strict monoidal structure to its skeletal model. It is represented by a cohomology class of degree 3 when the category is groupoidal. It is a small miracle of nature that the category Delta(+) is both strict monoidal and skeletal. Similarly for the category of finite cardinals and maps. Best wishes, André [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-05-23 15:39 ` terminology Colin McLarty 2010-05-24 13:42 ` equivalence terminology Paul Taylor 2010-05-24 15:53 ` we do meet isomorphisms of categories Marco Grandis @ 2010-05-24 18:04 ` Vaughan Pratt 2010-05-26 3:08 ` terminology Toby Bartels 2010-05-24 23:06 ` Equality again Joyal, André ` (2 subsequent siblings) 5 siblings, 1 reply; 34+ messages in thread From: Vaughan Pratt @ 2010-05-24 18:04 UTC (permalink / raw) To: categories list On 5/23/2010 8:39 AM, Colin McLarty wrote: > It is an interesting impulse in higher category theory to avoid > identity in favor of isomorphism on the level of objects, and to avoid > isomorphism in favor of equivalence on the level of categories. But > so far as I know no one has yet articulated a way to avoid ever using > identity of objects and identity of categories. Is identity even definable? I thought it was a kind of received wisdom, like the natural numbers. All of us seem to be working with the same notions of = and N, but what are they, exactly? That was only intended as a rhetorical question, btw. We can readily agree on some properties of = and N, which logicians of various stripes have gone to the trouble of spelling out, and which number theorists both analytic and algebraic have expanded on. Moreover most of us would agree that the proposition "the prime factors of M = 7^7^7^7 + 5^5^5^5 + 1 (7#4 + 5#4 + 1 where m#n denotes an exponential stack of n m's) are all greater than 2 billion and there are more than a thousand distinct such" not only makes perfect sense but is either true or false. However fewer might be willing to join me in insisting that it is certainly true. Those who question excluded middle for this proposition may have received different wisdom about N than the rest of us, though if I'm right then there's a constructive proof of the proposition that can be checked on any laptop in under an hour, which should then oblige the intuitionistic objectors to stand down. (No, I don't currently know a single prime factor of M and I don't believe anyone else does either. I do however know the least prime factors of both M + 1 and M + 958; leaving the former as an exercise, the latter is 1,985,781,901. M in decimal is 1755522...1375469 where the number of omitted digits when itself written in decimal has 695,975 digits, so although M in binary wouldn't fit in the universe let alone a laptop's random-access memory its length in binary would easily fit in the latter. The requisite calculations for all these observations take only minutes on an ordinary laptop.) Without exponentiation in the language, M would not be known to us: with only the polynomial operations the requisite expression 7*7*...*7 + 5*5*...*5 + 1 would stretch beyond the farthest known galaxies. This question about M, which is a question about N, could therefore not have arisen. With it, the question becomes part of our understanding, or lack thereof, of N. The same can be said of identity. The richer the language, the more tools we have to probe our understanding of identity, and the clearer our lack of complete understanding of it becomes. Vaughan Pratt [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-05-24 18:04 ` terminology Vaughan Pratt @ 2010-05-26 3:08 ` Toby Bartels 0 siblings, 0 replies; 34+ messages in thread From: Toby Bartels @ 2010-05-26 3:08 UTC (permalink / raw) To: categories list Vaughan Pratt wrote in part: >Moreover most of us would agree that the proposition "the prime factors >of M = 7^7^7^7 + 5^5^5^5 + 1 (7#4 + 5#4 + 1 where m#n denotes an >exponential stack of n m's) are all greater than 2 billion and there are >more than a thousand distinct such" not only makes perfect sense but is >either true or false. However fewer might be willing to join me in >insisting that it is certainly true. Since I know very little about these issues, I'm not ready to accept your claim that it is true. (I know that you sketched a way for me to verify it by performing some calculations on my laptop, but it would take a while for me to figure out what to program and then to convince myself that the output meant what you say.) However, I am happy to agree that the statement is true or false. >Those who question excluded middle for this proposition may have >received different wisdom about N than the rest of us, though if I'm >right then there's a constructive proof of the proposition that can be >checked on any laptop in under an hour, which should then oblige the >intuitionistic objectors to stand down. Anyone who doubts excluded middle for *this* proposition is not merely a constructivist, or even an intuitionist. Excluded middle for this proposition is provable in Heyting arithmetic. While a straightforward calculation of the factors of M would not fit into the physical universe, it is still finite. Those who doubt excluded middle (or meaningfulness) for this proposition go beyond intuitionism; they have been called "ultra-intuitionists", although the preferred term these days is "ultra-finitists". As someone who is quite comfortable with constructivism, I still find ultra-finitism a very strange way to think. Ultra-finitists definitely have a different recieved wisdom about N from what the rest of us have received. Ob categories: Does anybody know any work on ultra-finitism from the perspective of categorial logic? (somewhat in the way that topos theory can provide a perspective on constructivism). I doubt that any exists, but I would it would be nice if it did. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Equality again 2010-05-23 15:39 ` terminology Colin McLarty ` (2 preceding siblings ...) 2010-05-24 18:04 ` terminology Vaughan Pratt @ 2010-05-24 23:06 ` Joyal, André 2010-05-26 2:27 ` Patrik Eklund 2010-05-27 11:30 ` Prof. Peter Johnstone 2010-05-25 14:08 ` terminology John Baez 2010-05-26 8:03 ` terminology Reinhard Boerger 5 siblings, 2 replies; 34+ messages in thread From: Joyal, André @ 2010-05-24 23:06 UTC (permalink / raw) To: Colin McLarty, categories Dear Colin, You wrote: >It is an interesting impulse in higher category theory to avoid >identity in favor of isomorphism on the level of objects, and to avoid >isomorphism in favor of equivalence on the level of categories. But >so far as I know no one has yet articulated a way to avoid ever using >identity of objects and identity of categories. I love the equality symbol more than an isomorphism symbol, and an isomorphism symbol more than an equivalence symbol. I always try to use the equality symbol whenever possible. I often use the equality symbol for a canonical isomorphism. Is there a special symbol for canonical isomorphism? (as oppose to a plain isomorphism). I would love to write something like A times (B times C) =' (A times B) times C André -------- Message d'origine-------- De: categories@mta.ca de la part de Colin McLarty Date: dim. 23/05/2010 11:39 À: categories@mta.ca Objet : categories: Re: terminology I have very much appreciated André's subtlety on this issue in conversation ... [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: Equality again 2010-05-24 23:06 ` Equality again Joyal, André @ 2010-05-26 2:27 ` Patrik Eklund 2010-05-27 11:30 ` Prof. Peter Johnstone 1 sibling, 0 replies; 34+ messages in thread From: Patrik Eklund @ 2010-05-26 2:27 UTC (permalink / raw) To: categories I may have missed some parts of the equality message exchange, but here a few lines from general equational programming point of view. I believe it is always important to note where equality or its genetic siblings reside. As far as I understand we do category theory mostly over ZFC, so ZFC is a metalanguage for category theory. The equality for "the diagram commutes" is in ZFC, but the "equation" t1 = t2 involving two terms over a signature is more tricky. You might say it's an ordered pair (t1,t2), and that structure is in ZFC. The objective of rewriting is to find a substitution (Kleisli morphism) s so that s(t1)=s(t2). More precisely, the substitution is a morphism s : X -> TY, so you extend it to Ts : TX -> TTY, and bring it to mu_Y o Ts : TX -> TY with the mu from the term monad. All this is done over Set, i.e. T is a monad over Set, and therefore TX and TY are sets in ZFC. So, the equality in mu o Ts(t1) = mu o Ts(t2) is the equality in ZFC. Incidently, Set is already here in question as Set covers only the one-sorted signatures case. Moving over to many-sorted signatures you need more. However, you can use composed monads instead of T, and you don't have to be over Set, or its multisorted cousin. Even more so, is it really only about ordered pairs? In the end, we are looking for a substitution bringing that "possibly something else than just an ordered pair" to something close to a 'singleton', where the notion of 'singleton' then should reside mostly in the purely categorical language, rather than in only and exclusively in ZFC. General logics (Meseguer, Goguen, Burstall et al) in a general monadic setting both for terms as well as sentences, invites to this thinking, even if admittedly the programing examples at this point, for the monadic extensions, are rather artificial. Also note that syntactics has for quite a while been studied with respect to categorization, but semantics is mostly seen in the metalanguage of set theory. Doesn't have to be so? Cannot be so? We are obviously trying to complicate things as much as possible in syntactics, and when it comes to semantics, our semantics domains are mostly sets, and equality is like the emperor, changing clothes all the time. Best regards, Patrik On Mon, 24 May 2010, Joyal, André wrote: > Dear Colin, > > You wrote: > >> It is an interesting impulse in higher category theory to avoid >> identity in favor of isomorphism on the level of objects, and to avoid >> isomorphism in favor of equivalence on the level of categories. But >> so far as I know no one has yet articulated a way to avoid ever using >> identity of objects and identity of categories. > > I love the equality symbol more than an isomorphism symbol, > and an isomorphism symbol more than an equivalence symbol. > I always try to use the equality symbol whenever possible. > I often use the equality symbol for a canonical isomorphism. > Is there a special symbol for canonical isomorphism? (as oppose > to a plain isomorphism). I would love to write something like > > A times (B times C) =' (A times B) times C > > André > > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: Equality again 2010-05-24 23:06 ` Equality again Joyal, André 2010-05-26 2:27 ` Patrik Eklund @ 2010-05-27 11:30 ` Prof. Peter Johnstone 2010-06-01 6:36 ` Marco Grandis 1 sibling, 1 reply; 34+ messages in thread From: Prof. Peter Johnstone @ 2010-05-27 11:30 UTC (permalink / raw) To: André Joyal On Mon, 24 May 2010, Joyal, André wrote: > I love the equality symbol more than an isomorphism symbol, > and an isomorphism symbol more than an equivalence symbol. > I always try to use the equality symbol whenever possible. > I often use the equality symbol for a canonical isomorphism. > Is there a special symbol for canonical isomorphism? (as oppose > to a plain isomorphism). I would love to write something like > > A times (B times C) =' (A times B) times C > > André > TeX provides a command \doteq for an equality sign with a dot over it; this is used in other areas of mathematics to mean "is approximately equal to", but as far as I know it hasn't yet been used by category-theorists. Perhaps we could use it to mean "is canonically isomorphic to"? I'd also like to use it (or something like it) between pairs of morphisms, meaning that (they are not equal but) they become equal when composed with the appropriate canonical isomorphisms (to which I can't be bothered to give names) in order to match up their domains and codomains. (Of course, this is simply saying that they are canonically isomorphic as objects of the functor category [2,C], where C is the category in which they live.) Peter Johnstone [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: Equality again 2010-05-27 11:30 ` Prof. Peter Johnstone @ 2010-06-01 6:36 ` Marco Grandis 2010-06-01 14:38 ` Joyal, André 0 siblings, 1 reply; 34+ messages in thread From: Marco Grandis @ 2010-06-01 6:36 UTC (permalink / raw) To: Prof. Peter Johnstone, categories On 27 May 2010, at 13:30, Prof. Peter Johnstone wrote: > > TeX provides a command \doteq for an equality sign with a dot over it; > this is used in other areas of mathematics to mean "is approximately > equal to", but as far as I know it hasn't yet been used by category- > theorists. Perhaps we could use it to mean "is canonically > isomorphic to"? > > I'd also like to use it (or something like it) between pairs of > morphisms, meaning that (they are not equal but) they become equal > when composed with the appropriate canonical isomorphisms (to which > I can't be bothered to give names) in order to match up their domains > and codomains. (Of course, this is simply saying that they are > canonically isomorphic as objects of the functor category [2,C], > where C is the category in which they live.) > > Peter Johnstone Dear Peter, Isn't this very dangerous? 1. First, I think you are referring to some (specified) *coherent* (contractible) system of isomorphisms, otherwise you can easily prove that 1 = - 1 (see an example below). 2. Even in that case, we know that coherence can be a delicate thing. Let us take the cartesian product in Set (or the tensor product in a symmetric monoidal category). Would you write XxY =. YxX for the symmetry isomorphism s? Then by XxX =. XxX do you mean s or the identity? For XxXxX =. XxXxX we have six permutations of variables, generated by sxX and Xxs; and so on. I hope nobody will suggest some complicated trick to account for this; transpositions and permutations are already there, known to everybody; but we have to name them. 3. Coming back to point 1, "canonical" isomorphisms need not be coherent. There are a lot of such situations; I like to refer to the induced isomorphisms in homological algebra, because much of my early work was linked with that. A is an abelian group (or an object of an abelian category, or something more general that we do not need to consider here); X is a sublattice of the (modular) lattice of subobjects of A. We consider the subquotients H/K of A, where H and K belong to X. Then the canonical isomorphisms between these subquotients (induced by idA) are coherent if and only if X is distributive. (This is what I am calling now a "coherence theorem for homological algebra"; it applies to all the usual systems that produce spectral sequences, and is the reason "why" one cannot make errors when using canonical isomorphisms there.) An easy example of non-coherence can be built in the group A = ZxZ, taking for X the whole lattice of subgroups, obviously not distributive. Then Zx0 is canonically isomorphic to A/diagonal, and the latter is canonically isomorphic to 0xZ. Now, Zx0 and 0xZ are not canonically isomorphic, as already remarked in Mac Lane's "Homology". But notice that the composite of these isomorphisms is (x, 0) |--> (0, -x), while when you go through A/codiagonal, you get the opposite isomorphism, (x, 0) |--> (0, x). Best regards Marco Grandis [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: Equality again 2010-06-01 6:36 ` Marco Grandis @ 2010-06-01 14:38 ` Joyal, André 0 siblings, 0 replies; 34+ messages in thread From: Joyal, André @ 2010-06-01 14:38 UTC (permalink / raw) To: Marco Grandis Dear Marco, We could use of the dotted-equality symbol only when the canonical isomorphism under consideration is part of a contractible network of isomorphisms. The network does not need to be explicitly identified if the context is clear enough. For example, the dotted equality (A times B)times C =. A times (B times C) is refering to the associativity constraint. The dotted equality A times B =. B times A is refering to the symmetry constraint. But the dotted equality A times A =. A times A is ambiguous and should be excluded (actually, it is not ambiguous, since the identity of A times A is denoted A times A = A times A ). I am proposing a rule of thumb, not a new formalism. Mathematics is as much an art as it is an exact science. Best, André -------- Message d'origine-------- De: categories@mta.ca de la part de Marco Grandis Date: mar. 01/06/2010 02:36 À: Prof. Peter Johnstone; categories@mta.ca Objet : categories: Re: Equality again On 27 May 2010, at 13:30, Prof. Peter Johnstone wrote: > > TeX provides a command \doteq for an equality sign with a dot over it; > this is used in other areas of mathematics to mean "is approximately > equal to", but as far as I know it hasn't yet been used by category- > theorists. Perhaps we could use it to mean "is canonically > isomorphic to"? > > I'd also like to use it (or something like it) between pairs of > morphisms, meaning that (they are not equal but) they become equal > when composed with the appropriate canonical isomorphisms (to which > I can't be bothered to give names) in order to match up their domains > and codomains. (Of course, this is simply saying that they are > canonically isomorphic as objects of the functor category [2,C], > where C is the category in which they live.) > > Peter Johnstone Dear Peter, Isn't this very dangerous? 1. First, I think you are referring to some (specified) *coherent* (contractible) system of isomorphisms, otherwise you can easily prove that 1 = - 1 (see an example below). 2. Even in that case, we know that coherence can be a delicate thing. Let us take the cartesian product in Set (or the tensor product in a symmetric monoidal category). Would you write XxY =. YxX for the symmetry isomorphism s? Then by XxX =. XxX do you mean s or the identity? For XxXxX =. XxXxX we have six permutations of variables, generated by sxX and Xxs; and so on. I hope nobody will suggest some complicated trick to account for this; transpositions and permutations are already there, known to everybody; but we have to name them. 3. Coming back to point 1, "canonical" isomorphisms need not be coherent. There are a lot of such situations; I like to refer to the induced isomorphisms in homological algebra, because much of my early work was linked with that. ... [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-05-23 15:39 ` terminology Colin McLarty ` (3 preceding siblings ...) 2010-05-24 23:06 ` Equality again Joyal, André @ 2010-05-25 14:08 ` John Baez 2010-05-25 19:39 ` terminology Colin McLarty 2010-05-26 8:03 ` terminology Reinhard Boerger 5 siblings, 1 reply; 34+ messages in thread From: John Baez @ 2010-05-25 14:08 UTC (permalink / raw) To: categories Colin wrote: It is an interesting impulse in higher category theory to avoid identity in > favor of isomorphism on the level of objects, and to avoid isomorphism in > favor of equivalence on the level of categories. But > so far as I know no one has yet articulated a way to avoid ever using > identity of objects and identity of categories. > I think Michael Makkai has done it. He has formulated a foundational approach to mathematics based on infinity-categories, in which equality plays no fundamental role: http://www.math.mcgill.ca/makkai/mltomcat04/mltomcat04.pdf I think some approach along these general lines might ultimately become quite popular. However, to think in an easy intuitive way about a mathematical world without equality, we need new definitions of words such as "the" and "is". Those who find it unpleasant to change the definition of words such as "autonomous" may think it absurd to consider a such a radical shift in basic terminology. However, we can already see these words changing their meanings as we pass from reasoning within sets - where we say "the" product 2 x 3 "is" 6 - to reasoning within categories - where we say "the" product of "the" 2-element set and "the" 3-element set "is" "the" 6-element set. For a readable introduction to some of Makkai's ideas, try: http://www.math.mcgill.ca/makkai/equivalence/equivinpdf/equivalence.pdf Best,. jb [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: Re: terminology 2010-05-25 14:08 ` terminology John Baez @ 2010-05-25 19:39 ` Colin McLarty 2010-05-29 21:47 ` terminology Toby Bartels 0 siblings, 1 reply; 34+ messages in thread From: Colin McLarty @ 2010-05-25 19:39 UTC (permalink / raw) To: categories; +Cc: John Baez As to articulating a way to avoid ever using identity of objects and identity of categories, John Baez writes > I think Michael Makkai has done it. He has formulated a foundational > approach to mathematics based on infinity-categories, in which equality > plays no fundamental role: > > http://www.math.mcgill.ca/makkai/mltomcat04/mltomcat04.pdf > > I think some approach along these general lines might ultimately become > quite popular. But so far as know, this remains an approach, and not any specific set of axioms offered as foundation. In this paper Michael defines "multitopic ω-category" more or less analogously to how Eilenberg and Mac~Lane defined "category," and he defines "the (large) multitopic set of all (small) multitopic ω-categories" using that definition. If I understand these correctly (and have not, for example, confused intuitive motivation with strict definition) they take for granted such as ideas as the category Set of sets, and Set-valued functors. While Eilenberg and Mac~Lane saw (and referred to) the foundational significance of their ideas, they did not offer their definition as a foundation per se. And they were right. Lawvere's foundations ETCS and CCAF are first-order axiomatizations which suffice to prove the theorems of mathematics (exactly which theorems depending on exactly which axioms, but he clearly defined variants suited to classical analysis and various extensions of that). Has anyone yet offered a first-order (or ML-typetheoretic) axiomatization of mathematics along Makkai's lines? Popular is another question! And I am not worried about finding a final form of such axioms. But I do not yet know of such axioms. best, Colin [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-05-25 19:39 ` terminology Colin McLarty @ 2010-05-29 21:47 ` Toby Bartels 2010-05-30 19:15 ` terminology Thorsten Altenkirch [not found] ` <A46C7965-B4E7-42E6-AE97-6C1D930AC878@cs.nott.ac.uk> 0 siblings, 2 replies; 34+ messages in thread From: Toby Bartels @ 2010-05-29 21:47 UTC (permalink / raw) To: categories Colin McLarty wrote in part: >As to articulating a way to avoid ever using identity of objects and >identity of categories, John Baez writes [snip] >Has anyone yet offered a first-order (or ML-typetheoretic) >axiomatization of mathematics along Makkai's lines? I don't know very much about what's been done along Makkai's lines; I also would like to see a specific (if not final) set of axioms. But category theory has been done in Martin-Löof type theory: http://www.cs.st-andrews.ac.uk/~rd/publications/CTMLTT.pdf It has also been done in the type-theoretic proof assistant Coq: http://coq.inria.fr/distrib/v8.2/contribs-20090527/ConCaT.html In both of these, there *is* a notion of equality (or better, identity) at all types, hence a notion of identity of objects of any given category, allowing one to define isomorphism of categories, etc. However, this logicians' identity does not match mathematicians' equality; the easiest way to see this is that there are no quotient types. (This means that already to do set theory, let alone category theory, you must define a set to be a type equipped with an equivalence relation. Such a thing is also called "setoid", depending on which author you read.) You an also use Mike Shulman's SEAR, in the variant without identity. http://ncatlab.org/nlab/show/SEAR http://ncatlab.org/nlab/show/SEAR#eqfree This looks much more like the ordinary language of mathematics. (Actually, one could modify ETCS in a similar way, although it would no longer deserve to be called "ETCS".) --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-05-29 21:47 ` terminology Toby Bartels @ 2010-05-30 19:15 ` Thorsten Altenkirch [not found] ` <A46C7965-B4E7-42E6-AE97-6C1D930AC878@cs.nott.ac.uk> 1 sibling, 0 replies; 34+ messages in thread From: Thorsten Altenkirch @ 2010-05-30 19:15 UTC (permalink / raw) To: Toby Bartels > But category theory has been done in Martin-Löof type theory: > http://www.cs.st-andrews.ac.uk/~rd/publications/CTMLTT.pdf > It has also been done in the type-theoretic proof assistant Coq: > http://coq.inria.fr/distrib/v8.2/contribs-20090527/ConCaT.html > > In both of these, there *is* a notion of equality (or better, > identity) > at all types, hence a notion of identity of objects of any given > category, > allowing one to define isomorphism of categories, etc. > However, this logicians' identity does not match mathematicians' > equality; > the easiest way to see this is that there are no quotient types. > (This means that already to do set theory, let alone category theory, > you must define a set to be a type equipped with an equivalence > relation. > Such a thing is also called "setoid", depending on which author you > read.) I don't know any reasonable formalisation in Intensional Type Theory. People usually assume that hom sets are a setoid but objects aren't. This means that constructions like arrow categories are not available. To avoid this one would have to formalize explicitely what is a family of setoids indexed over a setoid. After this it is hard to see the category theory... Cheers, Thorsten [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
[parent not found: <A46C7965-B4E7-42E6-AE97-6C1D930AC878@cs.nott.ac.uk>]
* Re: terminology [not found] ` <A46C7965-B4E7-42E6-AE97-6C1D930AC878@cs.nott.ac.uk> @ 2010-05-30 20:51 ` Toby Bartels 2010-06-01 7:39 ` terminology Thorsten Altenkirch [not found] ` <7BF50141-7775-4D3C-A4AF-D543891666B9@cs.nott.ac.uk> 0 siblings, 2 replies; 34+ messages in thread From: Toby Bartels @ 2010-05-30 20:51 UTC (permalink / raw) To: categories Thorsten Altenkirch wrote: >Toby Bartels wrote: [I suggested formalising category theory without equality of objects in intensional Martin-Löf type theory, Coq, or SEAR without equality] >I don't know any reasonable formalisation in Intensional Type Theory. >People usually assume that hom sets are a setoid but objects aren't. >This means that constructions like arrow categories are not available. >To avoid this one would have to formalize explicitely what is a family >of setoids indexed over a setoid. After this it is hard to see the >category theory... Why do you say that one cannot construct arrow categories? We need only dependent sums, which Martin-Löf has in his type theory, to form the type of all morphisms of a given category C. We cannot compare these for equality, nor do we want to. What we do need to compare for equality are commutative squares (which are the morphisms in the arrow category) with given corners (actually, even with two given parallel sides), and this we can do. To be explicit, let Ob be the type of objects of the category C; given x, y: Ob, let x -> y be the type of morphisms from x to y. Given further two morphisms f, g: x -> y, we have a proposition f = g. (Martin-Löf identifies propositions with types, but Coq does not, so I say "proposition" so you can interpret it in either system.) Then of course, there are operations and axioms that I will skip, except to introduce ; as notation for composition in diagrammatic order: f: x -> y, g: y -> z |- f;g: x -> z. Then the type of objects of the arrow category of C is sum_{x:Ob} sum_{y:Ob} x -> y, a dependent sum of dependent sums; a typical element of this type is (x,y,f), where x,y: Ob and f: x -> y. Given two objects (x,y,f) and (u,v,g) of the arrow category, the type of morphisms from (x,y,f) to (u,v,g) is sum_{a:x->u} sig_{b:y->v} f;b = a;g. (*) (Again, I say "sig" to keep things correct in Coq, since then f;b = a;g is a proposition rather than a type; this is the same as a sum to Martin-Löf.) A typical element of this type is (a,b,p), where p is a proof of the relevant equality. A set theorist might well write (*) above as { (a,b) | a: x -> u, b: y -> v, f;b = a;g }; they do not refer to p, since set theorists accept proof irrelevance. They would then be finished, but as type theorists, we still need to define when parallel morphisms are equal. We do this by imposing proof irrelevance in the definition; that is, the definition of equality makes no reference to p. Specifically, given parallel morphisms (a,b,p) and (c,d,q), both from (x,y,f) to (u,v,g) in the arrow category, we define the proposition that they are equal to be the conjunction of a = c and b = d. Notice that this makes sense, since a,c: x -> u and b,d: y -> v. So we can define that equality which we need in the arrow category. To sum up: An object in the arrow category of C is (x,y,f), where x and y are objects of C and f: x -> y is a morphism of C. A morphism from (x,y,f) to (u,v,g) in the arrow category of C is (a,b,p), where a: x -> u, b: y -> v, and p: a;g = f;b. Finally, two such morphisms (a,b,p) and (c,d,q) are equal if and only if a = c and b = d. (I leave it as an exercise for the reader to define the operations and prove the axioms that define the arrow category of C as a category.) If you find the summary above a bit too wordy, say A morphism from (x,y,f) to (u,v,g) in the arrow category of C is (a,b), where a: x -> u and b: y -> v such that a;g = f;b. That we do not give a name to the proof that a;g = f;b makes it obvious what the definition of equality of morphisms should be, so we leave it out as an abuse of language, or a convention of definition. If it still seems odd that it is even possible to give a proof a name, well, that is a feature of Martin-Löf type theory and Coq that you can ignore (just as I ignore the feature of ZFC that it is possible to ask whether two arbitrary sets are equal), but you can also use SEAR without equality to avoid even that. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-05-30 20:51 ` terminology Toby Bartels @ 2010-06-01 7:39 ` Thorsten Altenkirch 2010-06-01 13:33 ` terminology Peter LeFanu Lumsdaine [not found] ` <7BF50141-7775-4D3C-A4AF-D543891666B9@cs.nott.ac.uk> 1 sibling, 1 reply; 34+ messages in thread From: Thorsten Altenkirch @ 2010-06-01 7:39 UTC (permalink / raw) To: Toby Bartels Dear Toby, Thank you for your reply. Of course I am aware of this construction. A setoid is the intensional representation of a quotient (ie coequalizer) and any construction involving it should respect this structure. To use the underlying set of a setoid to construct another set seems fundamentally flawed. My understanding of an arrow category is that it's objects are the morphisms of the underlying category and since this is a setoid objects should be represented as a setoid too. You may say that we are only interested in objects upto isomorphism. But what does this mean precisely? Cheers, Thorsten On 30 May 2010, at 21:51, Toby Bartels <toby +categories@ugcs.caltech.edu> wrote: > Thorsten Altenkirch wrote: > >> Toby Bartels wrote: > > [I suggested formalising category theory without equality of objects > in intensional Martin-Löf type theory, Coq, or SEAR without equality] > >> I don't know any reasonable formalisation in Intensional Type Theory. >> People usually assume that hom sets are a setoid but objects aren't. >> This means that constructions like arrow categories are not >> available. >> To avoid this one would have to formalize explicitely what is a >> family >> of setoids indexed over a setoid. After this it is hard to see the >> category theory... > ... [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-06-01 7:39 ` terminology Thorsten Altenkirch @ 2010-06-01 13:33 ` Peter LeFanu Lumsdaine 0 siblings, 0 replies; 34+ messages in thread From: Peter LeFanu Lumsdaine @ 2010-06-01 13:33 UTC (permalink / raw) To: categories On Tue, June 1, 2010 03:39, Thorsten Altenkirch wrote: > A setoid is the intensional representation of a quotient (ie > coequalizer) and any construction involving it should respect this > structure. To use the underlying set of a setoid to construct another set > seems fundamentally flawed. Indeed; but what we construct is not just a set, it's a category! :-) In Toby's construction \C |---> arr \C, the setoid structure of the hom-sets of \C is _not_ respected if you just look at the underlying objects of arr \C, but it _is_ respected once you look at the whole resulting category arr \C. This is surely no worse than the fact that in just about any construction on setoids X |---> F(X), if you look at the underlying set of F(X), this will not fully respect the setoid structure of X? > My understanding of an arrow category is that it's objects are the > morphisms of the underlying category and since this is a setoid objects > should be represented as a setoid too. The trouble here is that the original setoid structure is not on the whole arrow-set C_1, but on the individual hom-sets C_1(a,b). The arrow category sums this up over all a,b:C_0, and so is no longer a setoid from this data alone. (A dependent sum of setoids over a set doesn't have a natural setoid structure, as far as I can see?) In our case, of course, the object-sets _are_ also naturally setoids, with their equalities given by isomorphisms of the categories. But we don't want to think of this setoid structure as primary: it's just a coarse reflection of part of the overall category structure. > You may say that we are only interested in objects upto isomorphism. > But what does this mean precisely? Going on from the above, it's an extension to the statement "we are only interested in elements of a setoid up to the given equality relation". So a more precise statement could go along the lines of: Any construction dependent on objects should respect isomorphisms. Best, -p. -- Peter LeFanu Lumsdaine Carnegie Mellon University [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
[parent not found: <7BF50141-7775-4D3C-A4AF-D543891666B9@cs.nott.ac.uk>]
* Re: terminology [not found] ` <7BF50141-7775-4D3C-A4AF-D543891666B9@cs.nott.ac.uk> @ 2010-06-01 18:22 ` Toby Bartels 0 siblings, 0 replies; 34+ messages in thread From: Toby Bartels @ 2010-06-01 18:22 UTC (permalink / raw) To: Thorsten Altenkirch; +Cc: categories Thorsten Altenkirch wrote in part: >A setoid is the intensional representation of a quotient (ie >coequalizer) and any construction involving it should respect this >structure. To use the underlying set of a setoid to construct another >set seems fundamentally flawed. I would rather not say "underlying set" here, but "underlying type". The category of types can do what it likes, but the category of sets should already have coequalisers. (Some type theorists do say "set" here; I just think that it is liable to confuse category theorists.) It is the setoids which behave like the sets that we know. But what is flawed about using the underlying type of a set(oid)? Group theorists who found group theory on set theory are allowed to use the underlying set of a group. So set theorists who found set theory (as setoid theory) on type theory should be able to speak of the underlying type of a set(oid), and category theorists who found category theory on type theory should be able to speak of the underlying type of their structures. >My understanding of an arrow category is that it's objects are the >morphisms of the underlying category and since this is a setoid objects >should be represented as a setoid too. I'm not sure what you mean by "this is a setoid". If you mean that, given a category C (as formalised in type theory), the morphisms of C form a setoid, then this is not true. Given a category C and two objects x and y of C, then the morphisms of C from x to y form a setoid, nothing more. Even if they did form a setoid, what of that? In Peter May's example of the category of intermediate fields in a given field extension, the objects do form a setoid. I call such a category a "strict category": http://ncatlab.org/nlab/show/strict+category Any poset defines a strict category in which isomorphic objects are equal. More generally, any category in which any two parallel morphisms are equal may be made into such a strict category by defining equality as isomorphism. Assuming an appropriate version of the axiom of choice, any category whatsoever may be made into a strict category by defining equality as isomorphism and making some choices to match up hom-sets. The fact that strict categories exist does not invalidate the perspective from which categories are not inherently strict, any more than the existence of monoidal categories invalidates ordinary category theory. Even assuming the axiom of choice, that we can make any category into a strict category is like our ability to make any monoidal category into a strict monoidal category; the theory of weak categories and weak monoidal categories stands. (Incidentally, any strict monoidal category must be a strict category, while a weak monoidal category need not be.) >You may say that we are only interested in objects upto isomorphism. But >what does this mean precisely? What it means is that, whenever anyone refers to equality of objects, I interpret it as being a statement in strict category theory, with all other statements being in ordinary (weak) category theory. It is an empirical claim that the basic results of category theory as it is normally understood do not refer to equality of objects. It is conjecture in metamathematics that any such statement, if a theorem, has a proof that never refers to equality of objects. (Whether this conjecture is true or false can depend on exactly what your foundations of mathematics are. You also have to take care to identify defined concepts that implicitly make reference to equality of objects.) --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
* Re: terminology 2010-05-23 15:39 ` terminology Colin McLarty ` (4 preceding siblings ...) 2010-05-25 14:08 ` terminology John Baez @ 2010-05-26 8:03 ` Reinhard Boerger 5 siblings, 0 replies; 34+ messages in thread From: Reinhard Boerger @ 2010-05-26 8:03 UTC (permalink / raw) To: 'Colin McLarty'; +Cc: categories Dear Colin, dear all, you wrote: > It is an interesting impulse in higher category theory to avoid > identity in favor of isomorphism on the level of objects, and to avoid > isomorphism in favor of equivalence on the level of categories. But > so far as I know no one has yet articulated a way to avoid ever using > identity of objects and identity of categories. As far as I remember I listened to a talk by a logician called H. Preller in the seventies. She developed a language for categories, which did not contain the identity of objects. Greetings Reinhard [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
[parent not found: <4BF6BC2C.2000606@btinternet.com>]
* Re terminology: [not found] ` <4BF6BC2C.2000606@btinternet.com> @ 2010-05-21 18:48 ` Urs Schreiber 0 siblings, 0 replies; 34+ messages in thread From: Urs Schreiber @ 2010-05-21 18:48 UTC (permalink / raw) To: Ronnie Brown Dear Ronnie, > You mention the process from category to infinity-category. Actually that > was why we introduced the term infinity-category This is why I am thinking you could embrace the way the term is used these days: because it follows precisely your use back then, only removing the restriction of strictness. And algebraicity can be restored. See below... > The problem is that there is > no unique choice of such retractions, nor is it clear what might be the > relations between iterates of such fillers. These considerations led Keith > Dakin to the notion of T-complex for his 1976 thesis; somehow `T-complex' > has more recently become `complicial set', but nobody asked me. (Groan! > Groan!) So it seems that the notion of quasi category as a weak Kan complex > still has not captured something about the basic example; but how to repair > that is quite unclear. This has recently been clarified by Thomas Nikolaus in his work on algebraic Kan complexes (which are essentially simplicial T-complexes!) and algebraic quasi-categories: http://ncatlab.org/nlab/show/model+structure+on+algebraic+fibrant+objects He shows that the model category/quasi-category/(oo,1)-category (check preferred term) of all Kan complexes is equivalent to that of all Kan complexes with all horn fillers chosen. And analogously: that the model category/quasi-category/(oo,1)-category (check preferred term) of all quasi-categories is equivalent to that of all quasi-categories with all inner horn fillers chosen. This says that while a Kan complex or quasi-category is not directly an algebraic model for an oo-groupoid or (oo,1)-category, respectively, you can immediately turn it into an algebraic model by making choices, and up to equivalence, the resulting algebraic model does not depend on these choices. Best, Urs [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
[parent not found: <AANLkTilG69hcX7ZV8zrLpQ_nf1pCmyktsnuE0RyJtQYF@mail.gmail.com>]
* Re: terminology [not found] ` <AANLkTilG69hcX7ZV8zrLpQ_nf1pCmyktsnuE0RyJtQYF@mail.gmail.com> @ 2010-05-26 8:28 ` John Baez 0 siblings, 0 replies; 34+ messages in thread From: John Baez @ 2010-05-26 8:28 UTC (permalink / raw) Cc: categories Colin wrote: As to articulating a way to avoid ever using identity of objects and > identity of categories, John Baez writes > >> I think Michael Makkai has done it. He has formulated a foundational >> approach to mathematics based on infinity-categories, in which equality >> plays no fundamental role: >> >> http://www.math.mcgill.ca/makkai/mltomcat04/mltomcat04.pdf >> >> I think some approach along these general lines might ultimately become > quite popular. > > But so far as know, this remains an approach, and not any specific set of > axioms offered as foundation. > I should let Michael speak for himself, but I have the impression that he intends to found all his work on FOLDS - "first-order logic with dependent sorts". In this paper: http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf he writes: "The restriction on the use of equality in FOLDS is a fundamental feature. FOLDS is to be used in formulating categorical situations in which, for example, equality of objects of a category is not an admissible primitive. The absence of term-forming operators, to be interpreted as functions, is a consequence of the absence of equality; it seems to me that the notion of "function" is incoherent without equality. It is convenient to regard FOLDS a logic without equality entirely, and deal with equality, as much as is needed of it, as extralogical primitives." Best, jb [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 34+ messages in thread
end of thread, other threads:[~2010-06-01 18:22 UTC | newest] Thread overview: 34+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2010-05-19 10:38 Re terminology: Ronnie Brown 2010-05-20 7:58 ` soloviev 2010-05-20 19:53 ` terminology Eduardo J. Dubuc 2010-05-20 22:15 ` Re terminology: Joyal, Andre 2010-05-20 11:58 ` Urs Schreiber [not found] ` <AANLkTikre9x4Qikw0mqOl1qZs9DDSkcBu3CXWA05OTQT@mail.gmail.com> 2010-05-21 17:00 ` Ronnie Brown 2010-05-22 19:40 ` Joyal, André [not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5827@CAHIER.gst.uqam.ca> 2010-05-22 21:43 ` terminology Ronnie Brown [not found] ` <4BF84FF3.7060806@btinternet.com> 2010-05-22 22:44 ` terminology Joyal, André 2010-05-23 15:39 ` terminology Colin McLarty 2010-05-24 13:42 ` equivalence terminology Paul Taylor 2010-05-24 15:53 ` we do meet isomorphisms of categories Marco Grandis 2010-05-26 15:21 ` Toby Bartels 2010-05-27 9:29 ` Prof. Peter Johnstone [not found] ` <alpine.LRH.2.00.1005271007240.11352@siskin.dpmms.cam.ac.uk> 2010-05-27 10:08 ` Marco Grandis 2010-05-30 12:05 ` Joyal, André 2010-05-24 18:04 ` terminology Vaughan Pratt 2010-05-26 3:08 ` terminology Toby Bartels 2010-05-24 23:06 ` Equality again Joyal, André 2010-05-26 2:27 ` Patrik Eklund 2010-05-27 11:30 ` Prof. Peter Johnstone 2010-06-01 6:36 ` Marco Grandis 2010-06-01 14:38 ` Joyal, André 2010-05-25 14:08 ` terminology John Baez 2010-05-25 19:39 ` terminology Colin McLarty 2010-05-29 21:47 ` terminology Toby Bartels 2010-05-30 19:15 ` terminology Thorsten Altenkirch [not found] ` <A46C7965-B4E7-42E6-AE97-6C1D930AC878@cs.nott.ac.uk> 2010-05-30 20:51 ` terminology Toby Bartels 2010-06-01 7:39 ` terminology Thorsten Altenkirch 2010-06-01 13:33 ` terminology Peter LeFanu Lumsdaine [not found] ` <7BF50141-7775-4D3C-A4AF-D543891666B9@cs.nott.ac.uk> 2010-06-01 18:22 ` terminology Toby Bartels 2010-05-26 8:03 ` terminology Reinhard Boerger [not found] ` <4BF6BC2C.2000606@btinternet.com> 2010-05-21 18:48 ` Re terminology: Urs Schreiber [not found] ` <AANLkTilG69hcX7ZV8zrLpQ_nf1pCmyktsnuE0RyJtQYF@mail.gmail.com> 2010-05-26 8:28 ` terminology John Baez
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).