Added a related incarnation of the argument for distributive categories

Dario Stein

]]>Note that convex powerset of distributions monad is not commutative.

]]>Sorry, taking it back again.

karlin

]]>Revert

karlin

]]>I’m pretty sure you need symmetry, or at least a braiding, to get Eckmann-Hilton. I’m not sure whether commutative monoids really make sense in a merely braiding monoidal category.

karlin

]]>I’m pretty sure you need symmetry, or at least a braiding, to get Eckmann-Hilton. I’m not sure whether commutative monoids really make sense in a merely braiding monoidal category.

karlin

]]>Added link to exchange law

Anonymous

]]>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)

added pointer to:

- Tomer Schlank, Lior Yanovski,
*The ∞-Categorical Eckmann-Hilton Argument*, Algebr. Geom. Topol. 19 (2019) 3119-3170 (arXiv:1808.06006, doi:10.2140/agt.2019.19.3119)

added pointer to the original argument

- Beno Eckmann, Peter Hilton, Theorem 1.12:
*Structure maps in group theory*, Fundamenta Mathematicae 50 (1961), 207-221 (doi:10.4064/fm-50-2-207-221)

reviewed (somewhat imperfectly!?) in:

- Beno Eckmann, Peter Hilton, Theorem 5.4.2 in:
*Group-like structures in general categories I multiplications and comultiplications*, Math. Ann. 145, 227–255 (1962) (doi:10.1007/BF01451367)

Gives a trivial proof by string diagram.

Yuxi Liu

]]>A bit about two symmetric idempotent operations without units, which I often need to remind myself of. I am not sure if this goes here, but the proof is quite similar to the standard EH proof. Happy to move it somewhere else if need be.

]]>Thanks, Todd.

]]>Got rid of the redundancy noted in the (nForum) discussion.

]]>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 $Mon$).

]]>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.

]]>Urs, I think incorporating common wisdom of many people in early phases of $n$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 $n$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. 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.

]]>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.

]]>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 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.

]]>RIP Hilton; good luck Zoran.

]]>I’ve started a new thread if anybody wants to continue the general discussion.

]]>@ 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.