Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created coherent topological space. Just the definition so far.
Should this page be merged with spectral topological space?
I think they certainly should be merged. I was not aware of this article, so added the material about coherent locales to “spectral topological space” instead.
Any opinions as to which should be the name and which the redirect?
I think “coherent space” and “coherent locale” are more common than “spectral space”. Lurie uses “coherent” in his books.
Maybe “coherent space” and “coherent locale” should be split into separate articles, although I do not have strong opinions about this.
It seems to me the only point to separating “coherent space” and “coherent locale” is that one needs a nonconstructive principle (the Boolean prime ideal theorem or equivalent) to establish that coherent locales are spatial. For me personally, this is not a very compelling reason.
It seems reasonable to me to keep them on the same page, although in that case I would rather the page be called “coherent space” rather than the current “coherent topological space” to respect the fact that it also discusses more general notions of “space” (viz. locales that may fail, constructively, to be spatial) than classical topological spaces. Hopefully there will not be too much confusion between that and the renamed coherence space (and we can include disambiguation hatnotes).
What is the procedure for merging? Should the shorter article be deleted, since its content is already present in the longer article?
If the content of one article is indeed entirely duplicated in the other, then it can just be deleted, and an appropriate redirect added to the other. (Plus, as I said I would prefer a renaming to just coherent space.)
I added redirects to the other article. This one should be deleted, but there is no “delete” button as far as I can see.
Yes, there is no direct way to explicitly delete entries. The way to go is to clear the content, remove all links to the entry, and rename it, usually from “name” to “name > history”.
How can one see the list of all links to an entry? We used to have it at the bottom of each page.
I receive
Edit blocked by spam detector
when I try to follow Urs’s instructions.
When merging, there’s no need to manually remove links: since we’ve also created a redirect from the page name to the other page it’s being merged with, all such links will automatically go there instead.
1 to 15 of 15