Re: separable locale

[Michael Fourman <michael.fourman@ed.ac.uk>]

> Prof. Peter Johnstone wrote:
>> Dear Thomas,
>>
>> I'm pretty sure that what Michael meant by "separable" was what
>> most topologists would call "second countable" -- i.e., countably
>> generated as a frame. (There are some topology textbooks in which
>> this condition is called "completely separable".)
>>
>> Peter Johnstone
>> ---------------------------------
>> On Tue, 30 Jun 2009, Thomas Streicher wrote:
>>
>>> Recently rereading Fourman's "Continuous Truth" I came across the term
>>> "separable locale" but could nowhere find an explanation. Does it mean a
>>> cHa A for which there exists a countable subset B such that ever a in
>>> A is
>>> the supremum of those b in B with b leq a. This would be the point free
>>> account of "second countable", i.e. having a countable basis.
>>> Of course, second countable T_) spaces are separable, i.e. have a
>>> countable
>>> dense set.
>>> Is this reading the "usual" one?
>>>
>>> Thomas
>

Thomas,

Peter is correct about my intention. More precisely, 'separable' is defined in
Formal Spaces (FS) (Fourman & Grayson, Brouwer Centenary Symposium) 3.12(c)
--- although I now find this account unnecessarily obscure.

What you say below is correct classically; constructively there is some subtlety.

A locale is separable iff it is presented (as in FS 1.1) by a countable language
with decidable \leq and countably many *inhabited* basic covers.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]