Compactness in Locales and in Formal Topology
Research output: Contribution to journal › Article › peer-review
Colleges, School and Institutes
If a locale is presented by a "flat site", it is shown how its frame can be presented by generators and relations as a dcpo. A necessary and suffcient condition is derived for compactness of the locale (and also forits openness). Although its derivation uses impredicative constructions, it is also shown predicatively using the inductive generation of formal topologies. A predicative proof of the binary Tychonoff theorem is given,including a characterization of the finite covers of the product by basic opens. The discussion is then related to the double powerlocale.
|Number of pages||26|
|Journal||Annals of Pure and Applied Logic|
|Publication status||Published - 1 Jan 2006|