Timeline for Constructively valid reference for the soberness of discrete spaces and points of a locale coproduct
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 23, 2023 at 10:17 | history | edited | Gro-Tsen |
edited tags
|
|
| Mar 9, 2023 at 15:20 | comment | added | Gro-Tsen | @Tyrone “Discreteness” means the frame of opens is $\mathscr{P}(X)$: so the question is to check that the frame homomorphisms $\mathscr{P}(X)\to\Omega$ are “the same” as elements of $X$. Yes you can see them as completely prime filters, but AFAICT you'll still need to argue that (a) if a c.p. filter contains two singletons $\{x\}$ and $\{y\}$ then $x=y$, and (b) since it contains the union of all singletons $\{x\}$ for $x\in X$ it contains one of them, so it contains a unique singleton, so, etc. — this is pretty much exactly the proof I wrote down in the question. | |
| Mar 9, 2023 at 14:17 | comment | added | Tyrone | For $1$, why not just use discreteness to equate the completely prime open filters with the completely prime filters ($=$ points) and thus conclude sobriety? To be honest, I'm not even sure what definition of discreteness or sobriety you will accept. | |
| Mar 9, 2023 at 14:02 | comment | added | Peter LeFanu Lumsdaine | Actually, one other thought: this result could show up is Mikkelsen’s construction of colimits in elementary toposes, via showing that the contravariant power-set functor is monadic; and the proof has to work in arbitrary toposes, so must certainly be constructive. That monadicity is close enough to this result that (iirc) one fairly direct way to prove it is essentially by showing this. But I don’t remember where (if anywhere) I’ve seen that proof written, and looking up a couple of references for Mikkelsen’s theorem, they prove the monadicity indirectly, using monadicity theorems. | |
| Mar 9, 2023 at 13:53 | comment | added | Peter LeFanu Lumsdaine | I agree, this is surprisingly difficult to find in the literature — the one place I thought I remembered seeing it was Johnstone Stone spaces, but on a quick skim I can’t find it there. Every couple of years I find myself redoing (1) as an exercise, and it’s always more non-trivial than I expect; I don’t think I’ve ever found a substantially simpler version than what you give here. | |
| Mar 9, 2023 at 12:33 | history | edited | Gro-Tsen |
add the "reference-request" tag that I had forgotten
|
|
| Mar 9, 2023 at 12:22 | history | asked | Gro-Tsen | CC BY-SA 4.0 |