Timeline for Are all group monomorphisms regular, constructively?
Current License: CC BY-SA 2.5
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 3, 2020 at 10:01 | comment | added | Paul Taylor | Both my answer and Todd's require List() in the category, which suggests arithmetic universes, but he says that the result also holds for compact Hausdorff groups. So any categorist interested in this question should look for a proof in a pretopos and whatever extra condition is required to work in both cases. | |
| Feb 1, 2020 at 17:17 | comment | added | Todd Trimble | Regarding the conjecture: it turns out that all closed subgroup inclusions between compact Hausdorff groups are equalizers. This is shown in D. Poguntke, Einige Eigenschaften des Darstellungsringes kompakter Gruppen, Math. Z. 130, 107-117 (1973) (link: pub.uni-bielefeld.de/download/1775049/2311754); see Satz 1.3 and Bemerkung 1.4, page 109. | |
| Jun 20, 2017 at 12:24 | comment | added | Todd Trimble | Paul, the discussion is by now ancient, but I added an answer where $\Pi$s do come into play. :-) | |
| Nov 14, 2010 at 22:51 | comment | added | Paul Taylor | For my observation about "lengths" of elements of the pushout I need well behaved free monoids. The notion of arithmetic universe provides exactly this (or would, if anyone had ever written the paper about them). Maybe one could derive free monoids from Palmgren's system, but the $\Pi$s are surely overkill. | |
| Nov 14, 2010 at 20:44 | comment | added | David Roberts♦ | You probably know this, Paul, but for others' benefit I'll add that Palmgren's constructive foundations is basically the idea that the category Set is a well-pointed $\Pi$-pretopos with a NNO and enough projectives (see ncatlab.org/nlab/show/ETCS#references_19). However I don't know enough about this to know if the desired proof exists. | |
| Nov 14, 2010 at 16:09 | history | answered | Paul Taylor | CC BY-SA 2.5 |