Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added to Eckmann-Hilton argument the formal proposition formulated in any 2-category.
BTW, doesn’t anyone have a gif with the nice picture proof?
No, but I have a nice animation.
No, but I have a nice animation.
I can’t see an animation in the pdf files on my system. Do I need to open the mpg file?
Clicking on the avi-link takes me to a page with a psalm on it and then some general links. Help! What do I need to do to see that animation?
Eugenia Cheng has a picture here
Thanks, I have linked to it from the entry now.
Why are they always called “abelian” monoids here? I swear, every book I’ve ever read calls them commutative monoids?
Harry is right, it is my impression, one does not say abelian ring, abelian finitary monad, and even abelian monoid but commutative instead.
I think that abelian should really be reserved for groups (since it’s really okay to give an additive representation then (since you can subtract and cancel). A general commutative monoid can have nontrivial idempotents under the operation, so things like can happen, even though in an abelian group, this implies that . That is, you should only use “abelian” when it makes sense to write it additively (if it at least admits the structure of a Z-module)
What happens on your system when you hit the edit-button at the bottom of an nLab page?
I decide that I’d rather raise the issue on the forum before taking possibly controversial action myself.
Okay, but now please change it.
I don’t know – I’ve heard people say “abelian monoid” too. (But not abelian ring. Abelian Lie algebra, yes.) I’m pretty sure I personally say “commutative monoid”, since what I am accustomed to writing as is a pretty important category. But both terms are used.
I’m pretty sure that I’ve heard “abelian monoid”, although at this point it’s too late to be sure if I ever heard it from anybody outside the John Baez circle. (Google gives some hits, however. Wikipedia.EN mentions it but gives no reference.) But not “abelian ring”.
I find Harry’s comments interesting. It never occurred to me to link the term “abelian” with the additive notation. But that would explain why nobody says “abelian ring” (although it doesn’t explain why some people do say “abelian Lie algebra”; presumably that’s in analogy to abelian Lie groups).
However, it seems to me that an abelian monoid can be written additively, and I often would do so. People usually the free monoid on one generator (which is abelian) additively! The monoid shouldn’t have to be cancellative for this to look right (and in any case, there are cancellative abelian monoids that aren’t groups, such as the free example); you just don’t allow yourself to subtract. I’m happy to use additive notation as long as the operation is associative and commutative, and even in some other cases (such as ordinal addition, which gives a nonabelian monoid, or vertical composition of natural transformations when using superscripts for application).
@ Andrew
Your presentation astonishes me!
Norwegian really has two different words for doughnuts with holes and doughnuts without holes?
I agree with Toby #14 – if writing an operation multiplicativity doesn’t entail an ability to divide, I don’t see why writing it additively should entail an ability to subtract.
@Mike: Writing additively at least implies the ability to cancel, if not subtract.
@Harry There is a difference between temptation and giving way! Ronnie consistently used additive notation in situations in which cancellation was not necessarily possible. His reason… it freed up juxtaposition for use elsewhere. The notation does not ’imply’ cancellation, but it may be prudent to avoid a temptation (don’t leave a big chocolate cake in view when I come back from a long run! (Not true really I just get the craving’)). Baues also uses additive notation a lot even for actions where is in a group and in another group on which it acts.
The notation is one thing the name another. Someone asked recently why do mathematicians insist in calling commutative groups Abelian. The use of Abelian was, to him, obscure. I have used Abelian monoid, but that is because monoids are structures very near to groups, but I think that commutative is much better… that does not imply that I will use it merely that I think it is clearer :-)
@Harry #17: not at all. Consider the rig of isomorphism classes of real vector bundles on , with Whitney sum giving addition and tensor product giving multiplication. Addition is non-cancellative since
where is the trivial line bundle and .
I’ve added Eugenia’s picture and Andrew’s animation to the references.
I think that it makes sense for a page about a theorem to have two different sections, one for statement and one for proof, rather than using theorem and proof environments. I don’t think that it makes sense to have a section for the statement and then to put the proof in that section. And it definitely does not make sense to put that proof immediately after a theorem environment for a different statement. So I have put things back.
I think that it makes sense for a page about a theorem to have two different sections, one for statement and one for proof,
I think proofs should go in proof-environments below the Proposition/Theorem environments that they refer to. Currently somebody is writing a piece of software that is trying to harvest the nLab for Definin/Proposition/Theorem/Proof-environments and extract databases of useful information from that. For that kind of thing to work, we need to stick to using these environments. Also if we ever decide to globally change the formatting of proofs, it would be nice if all proofs were machine-readably labeled as such.
And it definitely does not make sense to put that proof immediately after a theorem environment for a different statement.
What’s the difference? Is it that you want to highlight that the two binary operations need not even have any associativity that you want to emphasize?
I think for the nPOV it would be good to say that the EH argument is about in a 2-category and maybe remark after that that the proof did not actually involve any associativity.
And also Eugenia’s picture proof is about the 2-category statement.
Todd, I wrote “even for abelian monoids” to emphasise that, while not default standard, it is not that unusual to say abelian for monoids as it is for some other structures with commutativity. I did hear it more than once, but not nearly standard, while never heard it for some other notions. Of course, abelian Lie algebras, but they are called abelian because in f.d. case they integrate to abelian Lie groups. It is not true what Harry said in 17 that it is always assumed that writing an operation additively it must be commutative. For example in the Baues’ school of track categories etc. they use regularly additive notation for a noncommutative operation.
Also if we ever decide to globally change the formatting of proofs, it would be nice if all proofs were machine-readably labeled as such.
This would suppose many things. For example that proofs are indeed proofs, while often I see proof environment used and than it contains only the references. Then why not having reference environment there, rather than misleading proof environment ?
On the other hand, extracting to a database may also produce lots of semantical errors. Each entry has a different author and hence different silent assumptions and notation. Taken out of context may make it wrong when comparing to another result taken from its context. Thus if I write a proof of something in some entry I would like to have it intrepreted within this entry, unless humanly and thoughtfully stated to be used otherwise. Thus I would like to have a software option to take a particular theorem into a standalone part and humanly include it at multiple places, but I would not like that some system automatically extracts and dislocates the stuff which is organic in some entry. Even the words have different meanings in different entries. Somewhere a topos means Grothendieck topos, at another place it means an elementary topos. Somewhere manifold means differentiable, somewhere topological somewhere even paracompactness is dispensed with. At some point I may like to split theorem into two, change from theorem to metatheorem, to text, or to schema of theorems, and so on, chnage between different kinds of integration with the system. If the theorem were extracted outside and depending on rigid database format this would limit my wish to write anything in such environments. I also think that it is useful to have slightly differing versions of the same theorem in different entries, reflecting the level of detail, the notational prerequisites and other aspects. Human copy and paste and thoughtful adaptation would do for that, provided there is no software which overwrites this uniformly.
I would not like that some system automatically extracts and dislocates the stuff
Once you put material out there on the wiki, you are no longer in control of how people use it. So you have instead to ensure that whichever way people use it, it will make sense. Therefore it is good to stick to a little bit of standardization, the same kind of standardizaton that is today fully accepted standard in all math books.
I think proofs should go in proof-environments below the Proposition/Theorem environments that they refer to.
First of all, that’s not what you actually did. The proof referred to the -point version where associativity is not assumed. Yet you placed it beneath a -categorial version where associativity is assumed, a rather special case.
Secondly, I do not agree that proof environments should always go directly beneath the corresponding theorem environments. Even by the “fully accepted standard in all math books”, there is room for remarks between these, or even for relegating an unenlightening proof to an appendix (for us, another page).
Also if we ever decide to globally change the formatting of proofs, it would be nice if all proofs were machine-readably labeled as such.
If you don’t put it in an environment, then there’s nothing to globally change, so this doesn’t make sense to me.
However, I think that it’s fine to put this proof in a proof environment. I just don’t think that it should be in the ## Statement ## section or directly beneath a different proposition.
I think for the nPOV it would be good to say that the EH argument is about in a 2-category and maybe remark after that that the proof did not actually involve any associativity.
We could do that. I have also rearranged the Statement section now to give the -categorial version more prominence.
And also Eugenia’s picture proof is about the 2-category statement.
I have clarified this. Although really, her diagram makes perfect sense to me for the monoid object in monoid objects version in any monoidal category.
Once you put material out there on the wiki, you are no longer in control of how people use it. So you have instead to ensure that whichever way people use it, it will make sense.
Urs, this is not personal discussion around me. Look at the way entries are: most theorems have silent assumptions, context and assumed notations. This is a fact. Please think of the fine remarks I have put there in order to construct a better system in advance instead of personally scorning me for disobedience to cheering some secret motion behind the scene.
It is very discuraging.
I have to agree with Zoran. Unless the nLabizens decide to start writing like Bourbaki, it’s inevitable that theorems are going to be context-dependent. That’s not to say I’d be against a Bourbaki-style nLab!
However, I think that it’s fine to put this proof in a proof environment. I just don’t think that it should be in the ## Statement ## section or directly beneath a different proposition.
Sometimes in books one starts the proof and works for one page then in a natural break point one formulates a lemma, goes with it, and then after the lemma goes back to finish the main proof. So the main theorem proof is often disconnected for large theorems. While it is legitimate for some to avoid this (and it can indeed always be reorganized) but I do not see a reason to limit the style various people may have.
Please think of the fine remarks I have put there in order to construct a better system in advance instead of personally scorning me for disobedience to cheering some secret motion behind the scene. It is very discuraging.
I don’t understand this. what do you think I said? You said you don’t want people to use the nLab in a certain way. I pointed out that you hardly have control over how people will use it. Is that controversial?
Also if we ever decide to globally change the formatting of proofs, it would be nice if all proofs were machine-readably labeled as such.
If you don’t put it in an environment, then there’s nothing to globally change,
Exactly. So that’s too bad if we have all other proofs elsewhere formatted uniformly.
But, you know, I didn’t mean this minor issue to become such a big deal. Sorry for messing with your formatting decisions.
Urs, I brought relevant issues, e.g. said things like
extracting to a database may also produce lots of semantical errors
Therefore one has to design things carefully not to subtract the value from the carefully made content by overwriting it with not enough carefully thought through substance. The way you announced sound to me like a conspiracy; I read your message as there is a new system being created behind the scene by somebody, so I read your statement as saying implicitly
please comply by putting everything in a controlled way so we can automatically change it with database driven system. Somebody is working to extract into a database, so guys, let’s write formatted this and that way.
So if anybody is prescribing the way, then implicitly is your statement, this is the way I read it.
I call for more care in such a step (I cheer the possibility to extract, as long as it does not limit everybody’s flexibility in formatting, and is not overrighting carefully done work with less care than the original), to allow more possibilities without undermining those which we already have. Prescribing
you have instead to ensure that whichever way people use it, it will make sense
is really strange. First of all, it is impossible in higher extent unless one forbids context-sensitive discourse. Second, you are here prescribing while claiming in the message that you do not want me/us to prescribe “usage” ourselves (but we are talking about creation, and overwriting, not usage! if I misunderstood the fault is due misterious anouncement with new rules and without full description of the target behind). I think that it is more sensitive to create a more flexible system in advance. My call for care about things contributors care is not a call for control, but call for careful creation. (This is so obvious, it looks to me.)
It is one thing if somebody changes a text on individual and thought-driven basis. This is understood and it is about the mutual respect in the community. The systematic changes however are different and for them some discussion and careful announcement are needed. Call for this is not call for control.
32 Thanks.
Zoran,
maybe that’s not the right place to discuss things here, but I think that we should all be aware that the nLab is publicly visible and that people will tend to want to use it as a reliable source. You know the student who is currently programming a database based on the nLab just as well as I do from the discussion here. (Not quite a conspiracy yet ;-) This is just one example of an attempt of people to attempt to make systematic use of the nLab.
I tried to highlight this fact before when I said that it would eventually be good if we had confirmed theorems here. From my perspective, that simple statement, too, was met with reactions here that I could not quite follow. I have a similar sensation now.
But I think this is maybe too awkward to sort out electronically. Maybe we need to meet all in person on a conference Lab 2011 and discuss these matters in person to avoid misunderstandings as above, and to be more efficient than before.
Urs,
I do not see that the desire for flags for checked theorems and many other features we discussed before is nearly the same as the much less systematic boundary between non-environment proof and environment proof we are discussing here. Having the list of third-party checked results is one thing and the possibility for formalising the (non-proof-read by others) environments for just regular proofs and theorems is another. One is about flagging another is about creating material. However if you do understand these things to be related you could have said that you want just to do flags.
I do not understand your delegating to discuss 1-1 issues. If you talked to some guy (I do not know who he is, I do not remember name of people who rarely appear in discussions), do you expect that he will explain what he does separately to each person in nlab ? You clearly took tactics which is going to kill my enthusiasm here. I can not aspire to contribute to system which I do not understand.
It is good to meet in person, but it is likely that it will happen that I will have no resources nor permission to travel in near future. You say it is not a conspiracy, but if one delegates any meaningful discussion to unrealistic future, and does not believe in online discussion then why doing nlab ? If online there is no understanding than we better do math offline then. How can I after such words persuade new users to join us ?
Zoran,
I am perplexed by your strong feelings. I have the impression that you are reacting to something that did not happen. Are we seriously talking about whether there is conspiracy against somebody?
About discussion: I simply do not have the time and energy for the huge discussions about how to label a theorem or not. If after a few attempts from my side I see that my proposals are not finding support, I simply give up. I have more important things to do. But I do imagine in person such things are easier to sort out. That’s not a conspiracy, just my feeling.
Are we seriously talking about whether there is conspiracy against somebody?
Come on. I am symbolically talking about the lack of communication here and misunderstanding of importance and now even lack of understanding the communicability of it, and of usefulness of bringing the whole aspect of the story. If you have more important things to do than to communicate to collaborators, then you loose the support which you could have gotten with little patience. Urs, we invest immense time, and hurt our careers with the dedication to this and other n-collaborations. Hence it is important. I do not see what is problem with “in person”. I have skype on.
I am perplexed by your strong feelings.
I raised very concrete constructive issues in my first post on this and was immediately accused of forcing usage on other people. Of course I feel hurt by such accusations after all the hard work and genuine remarks.
I agree with Urs that this time we do not need discussing this issue, as it seems after a longer discussion that it still does not contain the changing dimension I was afraid off.
Zoran, I am not accusing you of anything. Also we are, unfortunately, not collaborating on anything here. I wish we were. In fact I wish we would stop this discussion here which I find entirely perplexing and confusing (sorry, but it’s true) and turn back to genuine technical issues.
Also we are, unfortunately, not collaborating on anything here.
I was not meaning research, but diverting attention to else’s nlab work and change the topic of today’s work in order to provide references and other contributions to the entries of else’s interest. If you do not find it useful, I will change the mode. On the other hand, I agree that it would be nicer if one would overlap in research again, but it is at the moment almost impossible for reasons i would not publicly detail (I can tell you on skype).
and turn back to genuine technical issues
I considered talking about which proof formats we use in practice a genuine technical issue as well.
Therefore it is good to stick to a little bit of standardization, the same kind of standardizaton that is today fully accepted standard in all math books.
The thing is that the range of topics and authors is here far more than what is in the much more focused and usually more single-handed work on a book. So I think it is too much to expect. Although individually the items are not much worse here than in books, the overall coherence of the whole nlab can not be achieved at the same level.
I would suggest that as in all these topics, we just take into account the points made and continue writing the entries. I sometimes find the environments get in the way of a smooth exposition, but mainly they are no bother and I use them. (The result does not always look quite as nice as I had hope but someone usually notices this and smooths out the formatting :-))
The overall coherence of the lab is good in my view. Some of the earlier and less visited entries need sprucing up and this is a good thing to do not only for formatting but for content. as more content is added then more things come to the surface.
Thanks Tim for optimism, but you know I am so much a pessimist and used too much to isolation. Therefore I have great fear from loosing any stability in doing math and nlab is providing some. Similar to you I am at an institution which does not have math in their statute nor culture and constantly need to invent something else to survive and not do what I like most. Thus I am maybe too sensitive to loose the little I have here as well.
As this thread is called the Eckmann-Hilton argument, it would seem to be a good place to tell you all that Peter Hilton has died at the age of 87. I knew him well. He was a real gentleman, interested in maths for its beauty, fun, and fascination. He helped me a lot when I was starting out, acting as one of my referees. As his wife’s brother and sister-in-law live in North Wales, he would visit quite frequently and we would meet up for a meal with Ronnie and others. He was always entertaining. I was just wondering how he was a few days ago, and this morning there is a message on the ALG-Top list.
I have made an entry for him and copied the Obituary that will appear in the Binghamton newspapers to it for information.
Nice, thanks. That’s an interesting life he had.
I added a last sentence to the entry, saying that his name is attached to the EM-argument (maybe to more things?)
At Eckmann-Hilton argument I took the liberty of moving the “History”-section down before the “References”-section. I think historical aspects of concepts are important to know, but I feel a page should first decribe a concept and then later recall its history, for otherwise the reader may not be able to appreciate the history.
I made a link on his name at Eckmann-Hilton duality. He wrote a nice book ’Homotopy Theory and Duality’ which has the projective homotopy theory of modules outlined in it. He also wrote a neat ’Introduction to Homotopy Theory’ which has crossed modules in yet was published in 1966. It is a very clear book. His book with Wylie was not so successful.
Peter used to talk about Turing, and had a completely different take on his story from the standard one which is influenced by the retelling of it in plays and on television. His stories about Bletchley Park were very interesting and amusing.
(I once counted up those people that I knew or met, who had worked at Bletchley Park. I was amazed to find who had helped there.)
@Zoran §43. I understand that feeling. I am not, in fact, at any institute as I rarely go in to Bangor, which is just across the Menai Straits from where I live but quite a distance by car, and fuel prices do not stop going up!
The challenge as far as the Lab is concerned is how to get something that is fairly self organising. I feel that it is already influential as a source, so we need some good exposition, but here ’good’ is a variable quantity, (I suspect having cyclic values). We are breaking new ground in what we are attempting, and the fact that people are looking at the entries is great. We should have a fairly ’organic’ structure, i.e. the entries need local coherence. The local to global principle then should mean that there is a semblance of global coherence. (<- this is not a theorem nor any where near to one and so I will not put it in the optimistic-wild-hope environment.:-)) Too rigid a control of styles etc. may be counterproductive, as we cannot predict what way the ’organism’ will evolve, but our collective ’good sense’ will help.
I should leave this and get back to doing something else… possibly collecting up fallen leaves in a biting east wind! possibly working on sketches, spherical objects etc. or writing referees reports on some papers, (long overdue… bother!).
My contract expires on Dec 4, then we can collect leaves together :)
Keep and eye on the jobs in the UK. There are a few around still. Not everything has shut down yet!
UK is too far from my parents, unfortunately. I will try to stay near by.
Sorry to hear that, Zoran. What’s the perspective?
Thank you for kind concern, Urs. I applied to only one place (the one I mentioned to you, Urs, a couple of weeks ago). Long term I can probably promote my adjunct assistant professorship at the university, math dept, into a full time assistant professorship, but this needs a decision and much preparation and administrative help of colleagues, what means delay of roughly a year. Legally I could try to extend present position for another 3 months or so (more than that could happen if some things improve in the meantime), and-or take another few months of a kind low-paid guest stipend at one German University, which I discussed with a person there. I skipped applying for a nice two year position of my profile (nc geometry) in Denmark, what I feel sorry now. The whole thing is not that bad, except for loosing additional peace (more worries, including for my parents and relatives) and stability; so it will be diffcult to stay focused. I do not have short-term problem with money, living in my own appartment (not really my own, but effectively, in a family) and having reasonable savings. I also have some students in Zagreb who I care about and would not like to go too far from them, unless I can help them in some better way.
Dear Zoran,
Not to be a gossip, but…
When I went to the MWTS, you came up in a conversation that I was listening to (unfortunately, I’m not at a high enough level to actually participate), and you’re very highly regarded, so take heart!
If you don’t put it in an environment, then there’s nothing to globally change,
Exactly. So that’s too bad if we have all other proofs elsewhere formatted uniformly.
Formatted how?
The only thing that the proof environment does it to write ‘Proof.’ at the beginning and put a box at the end. If you put the proof in a section labelled ## Proof ##, then you don’t need this. If someday we change the period to a colon or fill the box in black, that’s irrelevant for a proof that doesn’t use the environment. (It is relevant for people who write ‘Proof.’ and put in the box by hand. I agree that people should use the environment instead of that.)
@ Tim
(The result does not always look quite as nice as I had hope but someone usually notices this and smooths out the formatting :-))
Is it you who keeps putting link breaks in the opening of the environments?
@ Zoran
If it helps, the person who’s extracting things from the nLab (I vaguely remember the conversation) is not going to be writing over our material. So Urs is just trying to have the Lab in a state where it’s useful for him.
I’ve started a new thread if anybody wants to continue the general discussion.
RIP Hilton; good luck Zoran.
@Toby Mea culpa … probably.
Is it you who keeps putting link breaks in the opening of the environments?
I have tried to see what determines the formatting, looking at pages that look good with no large breaks, but have been unable to work it out as I sometimes copy source material from a page that looks good, paste where I want it then do a minor edit…. Doh! Large white spaces have appeared from nowhere and I can find no reason. I have tried editing separately (Mac with Textedit) and it still does not look good. (I have guiltily thought ’Well Toby will come behind and clean it up!’ Sorry (and thanks)) I found it difficult to find the necessary formatting advice in FAQs ’How to’ etc. It is probably there but I cannot find it.
Formatted how?
Toby, we must be talking past each other.
I think it would eventually be good if the nLab pages have uniform formatting of formal definition/lemma/theorem/proof content. Uniformly formatted such that it is easy for the reader to spot what is supposed to be a formal statement, what is supposed to be a formal proof, and uniformly marked in the source code, so that it is possible to have a computer program scan the Lab for, say, all theorems and proofs asserting existence of limits in some categories (that’s what this student is trying to do).
Therefore I am advocating to put each proof in a proof-environment.
I think this is a simple means to increase a certain robustness of the nLab content and a little step in making the content we provide here be usefully extractable, hence a little step in improving the effect that our efforts here have.
Toby, we must be talking past each other.
I think that we are a bit, but it probably does not matter too much, since I agree with this.
I am advocating to put each proof in a proof-environment.
Perhaps I think that you put too much emphasis on that, but it’s not worth arguing about.
I didn’t like where you put the proof environment at Eckmann-Hilton argument, but I’m happy with where I put it. If you’re happy with that too, then we’re OK.
so that it is possible to have a computer program scan the Lab for, say, all theorems and proofs asserting existence of limits in some categories
Since this has nothing to do with the Eckmann–Hilton argument, I’ve responded to it here.
I think that you put too much emphasis on that
That’s no fair. I said several times that I’d rather give up this discussion here than insist on my point. We do need to find a more effective way to deal with such issues, it steals too much time. Unfortunately, when I said this before here (suggesting that it would be more effective to discuss this in person) even more discussion ensued.
You all please put your theorem-environments where you like.
Urs, I think incorporating common wisdom of many people in early phases of lab is worthy its trouble in long run. Of course, nobody needs to sacrifice for it now or ever, but I do not feel that most of the discussions in past several bursts of discussions on technical background and organization of lab were fruitless. On the contrary, with few notable exceptions.
I think that you put too much emphasis on that
That’s no fair. I said several times that I’d rather give up this discussion here than insist on my point.
Your respons sounds like a non sequitur to me, so I think that we’re still talking past each other. (How insistent you are with a point is independent of how much emphasis that point puts on something.)
I don’t think that you have behaved unreasonably.
Getting back to the mathematical content, I don’t see why in step 2 in the proof (each operation preserves the other’s identity element) is needed. When I presented this proof to my class yesterday, someone asked about this, because it didn’t seem to be used further down. And it follows once you know the identities and the operations coincide, no? On Twitter, Eugenia suggested (something to the tune of) it might be to prove that the first binary operation (say) is a unital magma object internal to the category of unital magmas (though she phrased it as a monoid object in ).
Thanks, Todd.
added pointer to the original argument
reviewed (somewhat imperfectly!?) in:
added pointer to:
added pointer to:
Univalent Foundations Project, Thm. 2.1.6 in: Homotopy Type Theory – Univalent Foundations of Mathematics 2013 (web, pdf)
Kristina Sojakova, Syllepsis in Homotopy Type Theory, 2021 (pdf)
1 to 79 of 79