Timeline for Are all group monomorphisms regular, constructively?
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 13, 2018 at 10:09 | history | edited | YCor | CC BY-SA 4.0 |
added question in text
|
| Mar 25, 2018 at 13:16 | comment | added | Todd Trimble | Paul's last comment is ancient history, but what was meant in the quoted text is a permutation on the set of cosets plus the distinguished element, which swaps the identity and distinguished element, and which leaves everything else fixed. | |
| Jun 20, 2017 at 12:05 | answer | added | Todd Trimble | timeline score: 9 | |
| Nov 14, 2010 at 16:09 | answer | added | Paul Taylor | timeline score: 7 | |
| Nov 14, 2010 at 15:40 | comment | added | Paul Taylor | "Construct an involution t which exchanges the coset of 1 and the distinguished element." If the index of the subgroup is odd then there will be no involutions at all. | |
| Oct 7, 2010 at 14:13 | answer | added | Monic Win | timeline score: 2 | |
| Oct 7, 2010 at 6:20 | answer | added | Andrej Bauer | timeline score: 4 | |
| Oct 7, 2010 at 2:08 | comment | added | Peter LeFanu Lumsdaine | …for this case, i.e. $G = \mathit{Perm}(X)$, $H = \mathit{Stab}(x_0)$, we look at the functor $X \mapsto X+1$; that functor gives the embedding $\mathit{Perm}(X) \to \mathit{Perm}(X+1)$, and then the involution $t$ does the rest. Perhaps one could find another functor to replace it with, with another involution which would work constructively in a similar way? It certainly seems plausible that this approach might still work… | |
| Oct 7, 2010 at 2:02 | comment | added | Peter LeFanu Lumsdaine | One observation: the part of the standard proof still goes through (amusingly, a part that only emerges by leaving in one of the things I complained of as a typos). We can still construct the homomorphism $f \colon G \to \mathit{Perm}(G/H)$, and then $g \in H$ iff $f(g)$ fixes the trivial coset. So this reduces the general case to just the case where $G$ is the group of permutations on some set, and $H$ is the stabiliser of some element. Classically, the second half of the proof can then be seen as... | |
| Oct 7, 2010 at 1:56 | comment | added | Peter LeFanu Lumsdaine | Hmmm… interesting — I'd thought it was fairly standard in constructive logic to call a proposition/predicate/subset decidable if (internally) one can prove the excluded middle for it, but googling for a few phrases like “decidable truth-values” etc. does suggest that it's mostly categorical logicians and computer scientists who use this terminology. | |
| Oct 6, 2010 at 17:58 | comment | added | Monic Win | Fixed the typos. "Decidable" has computational connotations. Of course there is a strong constructive/computational link, and I did in fact use "decidable" in the PER-version of the question. Still, for abstract set theory I think I prefer "detachable". | |
| Oct 6, 2010 at 17:48 | history | edited | Monic Win | CC BY-SA 2.5 |
errors in previous edit
|
| Oct 6, 2010 at 17:15 | comment | added | Peter LeFanu Lumsdaine | The edit currently has a few typos: you need to adjoin the additional element to the set of cosets before taking the permutation group and constructing the homormorphism from G to it; and at the end, the second homomorphism you construct should look at $t \cdot f(g) \cdot t$, not $t(f(t(g))$. Also, what you call “detachable subgroup” would I think normally be known as a “decidable subgroup” (since the condition is exactly that its membership predicate is decidable)? But this is in any case a lovely question! | |
| Oct 6, 2010 at 15:01 | history | edited | Monic Win | CC BY-SA 2.5 |
add standard proof and pinpoint problem; added 93 characters in body
|
| Oct 6, 2010 at 14:45 | comment | added | Monic Win | Yeah, this deserves some text so I'm editing the question. | |
| Oct 6, 2010 at 8:16 | comment | added | Martin Brandenburg | Why is the usual proof (see for example exercise 7H (a) in "abstract and concrete categories", katmat.math.uni-bremen.de/acc/acc.pdf) not constructive? | |
| Oct 5, 2010 at 21:05 | history | asked | Monic Win | CC BY-SA 2.5 |