Timeline for Are all group monomorphisms regular, constructively?
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 21, 2022 at 2:00 | history | edited | Todd Trimble | CC BY-SA 4.0 |
not a bump, just an edit to remove the ugliness where the first character of a line was a period
|
| Nov 13, 2018 at 5:23 | history | edited | Todd Trimble | CC BY-SA 4.0 |
added an important link
|
| Jun 11, 2018 at 8:28 | comment | added | Peter LeFanu Lumsdaine | @ToddTrimble: indeed, “partitions” was a slightly misleading way to phrase it. I’ve written the argument up in mathoverflow.net/questions/302516/…, rephrased in terms of colourings instead of partitions, and generalised to modules over rigs, which makes it slightly clearer. | |
| Jun 9, 2018 at 16:12 | comment | added | Todd Trimble | Okay. Usually partitions are understood as having nonempty classes, hence my puzzlement. I'll be glad to see what you write, but generally your outline sounded good. | |
| Jun 9, 2018 at 15:59 | comment | added | Peter LeFanu Lumsdaine | @ToddTrimble: Andrej also persuaded me in off-MO discussion that the argument needs writing out in more detail. Can’t quite yet as I’m travelling now, but I’ll write it up longer in an answer here once I get the chance! Quickly answering your question now, though: yes, the partition can include an empty class, so yes those examples are similar. | |
| Jun 9, 2018 at 15:48 | comment | added | Todd Trimble | @PeterLeFanuLumsdaine I sort of follow, but I have trouble following the description of the congruence as it supposed to apply where one of the lists is empty. For example, are the empty list $e$ and the list $(x^-, x^+)$ congruent according to your description? | |
| Jun 9, 2018 at 13:50 | comment | added | Peter LeFanu Lumsdaine | in the partitions. But now if singleton lists $[x^+]$, $[y^+]$ are related in this congruence, we must have $x=y$, so we're done. I guess the argument Paul Taylor had in mind in his answer was some non-commutative analogue of this! | |
| Jun 9, 2018 at 13:46 | comment | added | Peter LeFanu Lumsdaine | I think it's ok: we can explicitly describe a congruence on $\mathrm{List}(X \times \{+,-\}$ that gives the free Ab group on $X$. Say two lists $a$, $b$ are similar if there exists some partition of the positions of $a$ as $S_1$, …, $S_n$, and of the positions of $b$ as $T_1$, … $T_n$ (they have the same number of classes), such that for each $i$, the $X$ components of the entries of $a$ on $S_i$ and of $b$ on $T_i$ are all equal, and also $S_i$ and $T_i$ have the same “signed size”. The only tricky bit of showing this is a congruence is transitivity, which involves merging classes [cont’d] | |
| Jun 8, 2018 at 19:46 | comment | added | Todd Trimble | Well, what I meant by "stepping stone" consisted in a hope of showing constructively that the free commutative monoid, which has a reasonably explicit description as outlined above, is a cancellation monoid. Of course I'm not yet sure this is a promising approach. | |
| Jun 8, 2018 at 15:07 | comment | added | Peter LeFanu Lumsdaine | Existence of free commutative groups/monoids is fine — the free monoid is as Todd says, while the free group can similarly be taken as the quotient of $\mathrm{List}(\{+,1\} \times X)$ by the congruence generated by the group axioms. The problem for injectivity is with giving a more explicit description of this congruence. Commutative monoids are much easier — $X$ embeds as singletons in $\mathcal{P}(X)$, which is a commutative monoid under $\land$ or $\lor$. But $\mathcal{P}(X)$ is absorbing, so any map from it to a group is constant, so I don’t see how to use it as a stepping stone. | |
| Jun 8, 2018 at 14:10 | comment | added | Todd Trimble | I was thinking more about the free commutative monoid as a stepping stone, which I was thinking should be internally constructible as $\sum_{n: \mathbb{N}} X^n/\Sigma_n$ with $X$ embedding into the $n=1$ part, similar to the list monad. | |
| Jun 8, 2018 at 13:55 | comment | added | Andrej Bauer | It would help if we could know anything specific about the free group $A$. Actually, I imagine naively that existence of free groups is not under question here? | |
| Jun 8, 2018 at 13:49 | comment | added | Todd Trimble | @PeterLeFanuLumsdaine Interesting! Now that you bring it up, I'm not seeing it clearly either. In a topos it would suffice to embed $\Omega$ into an abelian group, but that doesn't necessarily bring us closer. (I'm fond of this argument though; it'd be a pity to have to retract it.) | |
| Jun 8, 2018 at 13:34 | comment | added | Peter LeFanu Lumsdaine | Maybe I’m missing something obvious, but it’s not clear to me how to show constructively that there’s any injection from $G/H$ into an Abelian group. If there is such an injection, then of course the unit map into the free Abelian group on $G/H$ is one, but I don’t see how to show the unit is injective other than by exhibiting such an injection explicitly. Of course classically one can take the embedding into e.g. $\mathbb{Z}^{G/H}$, but constructively this only works when $G/H$ has decidable equality, which brings us back to the case of decidable $H$, proven in the question. | |
| Mar 25, 2018 at 12:00 | history | edited | Todd Trimble | CC BY-SA 3.0 |
fixed the definition of a particular action
|
| Jun 20, 2017 at 12:05 | history | answered | Todd Trimble | CC BY-SA 3.0 |