Timeline for Constructively, is the unit of the “free abelian group” monad on sets injective?
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Oct 2, 2022 at 9:45 | vote | accept | Peter LeFanu Lumsdaine | ||
| Oct 2, 2022 at 8:48 | answer | added | David Wärn | timeline score: 6 | |
| Feb 22, 2022 at 10:45 | vote | accept | Peter LeFanu Lumsdaine | ||
| S Oct 2, 2022 at 9:45 | |||||
| Nov 13, 2018 at 10:04 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
fixed typo
|
| Jun 12, 2018 at 11:58 | answer | added | Itai Bar-Natan | timeline score: 2 | |
| Jun 12, 2018 at 11:53 | comment | added | Ingo Blechschmidt | To put the claim into the form of a geometric sequent, I was thinking of this: $\langle 1, x \rangle \sim \langle 1, y \rangle \vdash x = y$ (in the context $x,y : X$). With $({\sim})$ I'm referring to the equivalence relation by Mines–Richman–Ruitenberg. If we expand the definition of that relation, we obtain several existential quantifiers (and conjunctions and disjunctions), but no universal quantifiers or implications. Regarding the unnecessarity of baby Barr: Your argument assumes that the topos of sets is Boolean, right? With baby Barr, we can avoid that assumption. | |
| Jun 12, 2018 at 8:26 | comment | added | Peter LeFanu Lumsdaine | @darijgrinberg: Yes, the permutation property you suggests follows from the explicit description of the free algebras in either my or Ingo’s answer. Thankyou also for the pointer to the Loehr–Mendes — that looks interesting, though as you say, will take some thought to see how it applies constructively! | |
| Jun 12, 2018 at 8:25 | comment | added | Peter LeFanu Lumsdaine | @IngoBlechschmidt: By the way, if the claim can be formulated geometrically (which I still don’t see but would love to hear), then I think even baby Barr’s is overkill: It’s easy to see that this property (for any finitary algebraic theory) holds in all Grothendieck toposes iff it holds in Sets, since free algebras in presheaves are pointwise, and free algebras in sheaves can be constructed by sheafification from presheaves, which preserves monos. | |
| Jun 11, 2018 at 19:59 | comment | added | darij grinberg | The calculus of "combinatorial objects" in Nicholas A. Loehr, Anthony Mendes, Bijective matrix algebra, Linear Algebra and its Applications, Volume 416, Issues 2--3, 15 July 2006, pp. 917--944 also seems of relevance -- though the way they have built it up, it probably requires all the sets to have decidable equality. | |
| Jun 11, 2018 at 19:57 | comment | added | darij grinberg | ... boil down to something like the Garsia-Milne involution principle: A crucial step is to show that if a tuple $\mathbf{a}$ is a permutation of a tuple $\mathbf{b}$, and some sub-tuple $\mathbf{a}'$ of $\mathbf{a}$ is a permutation of some sub-tuple $\mathbf{b}'$ of $\mathbf{b}$, then the complementary tuple of $\mathbf{a}'$ in $\mathbf{a}$ is a permutation of the complementary tuple of $\mathbf{b}'$ in $\mathbf{b}$. | |
| Jun 11, 2018 at 19:50 | comment | added | darij grinberg | More generally (and more usefully), we should be able to prove that if $1_{a_1} + 1_{a_2} + \cdots + 1_{a_n} = 1_{b_1} + 1_{b_2} + \cdots + 1_{b_m}$ for some elements $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_m$ of $X$, then the list $\left(a_1, a_2, \ldots, a_n\right)$ is a permutation of the list $\left(b_1, b_2, \ldots, b_m\right)$ (in the concrete sense: i.e., we have $n = m$, and there is some permutation $\sigma$ of $\left\{1,2,\ldots,m\right\}$ such that each $i$ satisfies $a_i = b_{\sigma\left(i\right)}$). I have a hunch that this should ... | |
| Jun 11, 2018 at 19:00 | comment | added | Peter LeFanu Lumsdaine | @IngoBlechschmidt: I don’t see how to formulate the claim as a geometric sequent, I’m afraid — what did you have in mind? Given that, I agree with the rest of the argument. | |
| Jun 11, 2018 at 15:16 | comment | added | Ingo Blechschmidt | I believe that the existence of such a constructive proof [constructively] follows from the existence of the classical proof, since we can apply the baby version of Barr's theorem (the double negation translation followed by Friedman's trick), as the claim can be formulated as a geometric sequent. Do you concur? | |
| Jun 11, 2018 at 15:14 | answer | added | Ingo Blechschmidt | timeline score: 6 | |
| Jun 11, 2018 at 8:26 | answer | added | Peter LeFanu Lumsdaine | timeline score: 12 | |
| S Jun 11, 2018 at 8:23 | answer | added | Peter LeFanu Lumsdaine | timeline score: 16 | |
| S Jun 11, 2018 at 8:23 | history | asked | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |