Post #1816211

2026-02-18 15:48 UTC

A bunch of cool results on idempotents in a homotopical setting can be found in e.g. Kerodon, but the one above seems to have gone unnoticed. I gave a proof last year in response to a question from Georg Lehner at https://mathoverflow.net/q/496917 . Yesterday I took the time to formalise it in Agda: https://dwarn.se/agda/Idem.html . A weaker result appears in recent papers of Lehner and Antieau (Theorem 5.6 of https://arxiv.org/pdf/2507.00221 and https://arxiv.org/pdf/2508.13106 ).

Replies (3)

@dwarn@mathstodon.xyz 2026-02-18 15:52

I rarely formalise things, so whenever I do get to be reminded of what it's like. My takeaway this time is how amazing it is that MLTT lets us reason about path algebra completely rigorously and with sol little friction.

Open ##1816212
@jakub_et_al@mathstodon.xyz 2026-02-19 09:32

@dwarn This sounds very much like stuff Walter Taylor worked on in 70's [https://doi.org/10.4153/CJM-1977-054-9]. In the paper, he showed (among many other things) that topological semilattices have trivial homotopy groups, or as he phrased it: THEOREM 6.2. Semilattices obey the law x = 1 in homotopy.

Open ##1816214
@OscarCunningham@mathstodon.xyz 2026-02-24 05:43

@dwarn I'm not an expert so this might be a stupid question, but does this also answer this question: https://mathoverflow.net/questions/161190/homotopy-theory-of-suplattices ? A suplattice is a semilattice with extra properties, so they must all be discrete. Like maybe we can't answer the precise question about model categories, but can we at least say that the 'Homotopy Theory of Suplattices' is trivial?

Open ##1816218