Timeline for Constructively, is the unit of the “free abelian group” monad on sets injective?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 16 at 13:08 | history | edited | David Wärn | CC BY-SA 4.0 |
correct typo
|
| Oct 19, 2022 at 13:02 | comment | added | Peter LeFanu Lumsdaine | @PaulTaylor: I don’t see any particular connection between this argument and that fact, either commonalities or conflicts. Did you have something specific in mind that I’m missing? | |
| Oct 19, 2022 at 9:40 | comment | added | Paul Taylor | @PeterLeFanuLumsdaine: given that this argument applies to any finitary algebraic theory, how does it fit in with the fact that any two finitely generated Jónnson-Tarski algebras are isomorphic? | |
| Oct 2, 2022 at 9:45 | vote | accept | Peter LeFanu Lumsdaine | ||
| Oct 2, 2022 at 9:42 | comment | added | Peter LeFanu Lumsdaine | But I remember us all really feeling sure it wasn’t just abstract nonsense, and really needed something explicit about groups/modules. Anyhow — since this proof is cleaner and more general than older answers, I’m accepting it in places of them — though I think they are still nice for the very explicit descriptions of free modules. | |
| Oct 2, 2022 at 9:40 | comment | added | Peter LeFanu Lumsdaine | Then decidable equality on $[n]$ lets you transfer this to injectivity of $\eta_{[n]}$: if $i,j \in [n]$ become equal under $\eta_{[n]}$, then by injectivity of $\eta_{[2]}$, they become equal under every map $[n] \to [2]$. So this proof really shows a more general result: If $A$ is any (finitary) algebraic theory, with some model with two distinct elements, then its unit is injective. Strange that no-one had noticed this during the discussions in Bonn that originally prompted this question — certainly Martín and Thierry were in those conversations, and I think Christian too! [cont’d] | |
| Oct 2, 2022 at 9:39 | comment | added | Peter LeFanu Lumsdaine | Yes, this is very nice! Funnily enough, I also came across largely the same proof recently (in discussion with Martín Escardó and Ivan di Liberti at the Coquand 60th in Göteborg) and had been thinking of adding it as here — so I have a long comment, from the things I’d thought of putting into it. The argument we had in mind for injectivity of the unit on finite sets was: First, note $\eta_{[2]} : [2] \to UF[2]$ is injective, by exhibiting an Abelian group with two distinct elements. [cont’d] | |
| Oct 2, 2022 at 9:05 | review | Late answers | |||
| Oct 2, 2022 at 10:40 | |||||
| S Oct 2, 2022 at 8:48 | review | First answers | |||
| Oct 2, 2022 at 9:00 | |||||
| S Oct 2, 2022 at 8:48 | history | answered | David Wärn | CC BY-SA 4.0 |