The unit interval and all interval coalgebras in constructive mathematics are continuous posets. See the reference

- {#Freyd08} Peter Freyd,
*Algebraic real analysis*, Theory and Applications of Categories, Vol. 20, 2008, No. 10, pp 215-306 (tac:20-10)

Anonymous

]]>Also made clear in the case of frames, that already by definition a frame is locally compact if it continuous.

]]>Added example that the lattice of open subsets of a topological space is a continuous lattice if and only if the sobrification of the topological space is locally compact (i.e. the topology has a basis of compact neighborhoods).

I am going to add this information at a few other places (where it is relevant)

]]>I put in an explicit discussion of possible morphisms. Are there common names for the various categories of continuous lattices?

]]>I added a bit more to continuous poset. One point which hadn’t been made before is that different people mean different things by the *category* of continuous lattices. People who think continuous lattices are monadic over sets think that the morphisms preserve directed joins and arbitrary meets. People who think the category of continuous lattices is cartesian closed think the morphisms are the maps that preserve directed joins.

Section C4.1 of the Elephant remarks “it can be shown using the axiom of choice that if a continuous lattice $A$ is distributive, then the locale $X$ defined by $\mathcal{O}(X)=A$ is spatial, and its space of points is locally compact.” For a proof it cites “The spectral theory of distributive continuous lattices” by Hoffman and Lawson.

]]>Yes, rewriting locally compact space is one thing that I've wanted to do for a while but haven't got around to, for various reasons.

]]>In that case, the page locally compact space would have to be significantly rewritten to be about more general kinds of “space”. If you object to “space” meaning “topological space” then I would be more inclined to rename the page locally compact space to locally compact topological space, have a separate page locally compact locale, and make “locally compact space” a redirect-with-hatnote to locally compact topological space.

]]>I would be inclined to fold locally compact locale into locally compact space anyway, since ‘space’ to me does not necessarily mean a topological space. In particular, the text ‘In classical mathematics, every locally compact locale is spatial, hence a locally compact space.’ now at the former page seems a non sequitur to me; classically or not, locally compact or not, every locale is a space. (This is also a problem with ‘spatial’ as applied to locales, but at least that is a technical term with an established meaning, unlike ‘space’.)

]]>Good call, Mike. I think you’re right.

]]>It sounds like the sort of theorem that might be true classically but not constructively. I don’t have SS in front of me right now to check what’s in there.

]]>Incidentally, I see a gray link to locally compact locale. It might make sense to absorb this proposed article into locally compact space, because it seems to be a theorem that locally compact locales are in fact spatial. See for example Categorical Foundations: Special Topics in Order, Topology, Algebra, and Sheaf Theory (ed. M.C. Pedicchio, W. Tholen), chapter II (Locales, written by Jorge Picado, Aleš Pultr, and Anna Tozzi), section 7 (p.97). Might also be in Johnstone’s Stone Spaces; haven’t checked.

]]>Added to continuous poset the statement that continuous lattices are monadic over sets, via the filter monad.

]]>No, we really did not – but you’ve now ungrayed some links; thank you!

]]>Did we really not have continuous poset?

]]>