Skip to content

Locales.Compactness.CharacterizationOfCompactLocales

---
title:          Characterizations of compact locales
author:         Ayberk Tosun
date-started:   2025-04-23
date-completed: 2024-04-29
---


{-# OPTIONS --safe --without-K --lossy-unification #-}

open import MLTT.Spartan hiding (J)
open import UF.Base
open import UF.Classifiers
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.SubtypeClassifier

module Locales.Compactness.CharacterizationOfCompactLocales
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
        (sr : Set-Replacement pt)
       where

open import Locales.AdjointFunctorTheoremForFrames
open import Locales.CompactRegular pt fe
 using (clopens-are-compact-in-compact-frames;
        is-clopen;
        compacts-are-clopen-in-zero-dimensional-locales;
        frame-homomorphisms-preserve-complements;
        complementation-is-symmetric; is-complement-of)
open import Locales.Compactness.Definition pt fe
open import Locales.ContinuousMap.Definition pt fe
open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe
open import Locales.Frame pt fe renaming (⟨_⟩ to ⟨_βŸ©βˆ™) hiding (βˆ…)
open import Locales.PosetalAdjunction pt fe
open import Locales.InitialFrame pt fe
open import Locales.PerfectMaps pt fe
open import Locales.Spectrality.SpectralityOfOmega pt fe sr
open import Locales.TerminalLocale.Properties pt fe sr
open import Notation.UnderlyingType
open import Slice.Family
open import UF.Logic

open AllCombinators pt fe
open ContinuousMaps
open FrameHomomorphisms
open Locale
open PropositionalTruncation pt

instance
 underlying-type-of-frame : Underlying-Type (Frame 𝓀 π“₯ 𝓦) (𝓀 Μ‡ )
 ⟨_⟩ {{underlying-type-of-frame}} (A , _) = A


\section{Preliminaries}

The universal property of the inital frame gives that there is a unique frame
homomorphism `Ξ© β†’ π’ͺ(X)`, for every locale `X`. We denote this by `!`. We also
define the shorthand notation `!κ™³` for the underlying function of the frame
homomorphism in consideration.


!_ : (X : Locale (𝓀 ⁺) 𝓀 𝓀) β†’ X ─cβ†’ 𝟏Loc pe
! X = center (𝟎-π”½π•£π•ž-initial pe (π’ͺ X))

!κ™³[_]_ : (X : Locale (𝓀 ⁺) 𝓀 𝓀) β†’ Ξ© 𝓀 β†’ ⟨ π’ͺ X ⟩
!κ™³[_]_ X = fun (𝟎-π”½π•£π•ž pe) (π’ͺ X) (! X)


Note here that the notation `_κ™³` is intended to mimic a superscript asterisk.
Sadly, there is no proper superscript asterisk in Unicode so we use the Slavonic
asterisk.

We also define some shorthand notation for the right adjoint of this map, which
we know to exist since the initial frame has a small base. We denote by
`!⁎[ X ]_` the underlying function of the right adjoint of `!κ™³[ X ]_`.


!⁎[_]_ : (X : Locale (𝓀 ⁺) 𝓀 𝓀) β†’ ⟨ π’ͺ X ⟩ β†’ Ξ© 𝓀
!⁎[_]_ {𝓀} X = ! X ⁎·_
 where
  open Spectrality-of-𝟎 𝓀 pe
  open AdjointFunctorTheorem pt fe X (𝟏Loc pe) ∣ β„¬πŸŽβ†‘ , β„¬πŸŽβ†‘-is-basis ∣


Thinking of a frame as a system of finitely verifiable properties, the above map
can be thought of as the **universal quantifier** for these properties: it takes
some open `U : ⟨ π’ͺ X ⟩` and tells if `U ＝ 𝟏[ π’ͺ X ]`.


!⁎-is-universal-quantifier : (X : Locale (𝓀 ⁺) 𝓀 𝓀)
                           β†’ (U : ⟨ π’ͺ X ⟩)
                           β†’ (!⁎[ X ] U) holds ↔ U ＝ 𝟏[ π’ͺ X ]
!⁎-is-universal-quantifier {𝓀} X U = † , ‑
 where
  open Spectrality-of-𝟎 𝓀 pe
  open AdjointFunctorTheorem pt fe X (𝟏Loc pe) ∣ β„¬πŸŽβ†‘ , β„¬πŸŽβ†‘-is-basis ∣
  open PosetReasoning (poset-of (π’ͺ X))

  † : (!⁎[ X ] U) holds β†’ U ＝ 𝟏[ π’ͺ X ]
  † p = only-𝟏-is-above-𝟏 (π’ͺ X) U Ξ³
   where
    β…‘ : (!κ™³[ X ] ⊀ ≀[ poset-of (π’ͺ X) ] U) holds
    β…‘ = adjunction-inequality-backward (! X) U ⊀ Ξ» { ⋆ β†’ p }

    β…  : 𝟏[ π’ͺ X ] ＝ !κ™³[ X ] ⊀
    β…  = frame-homomorphisms-preserve-top (𝟎-π”½π•£π•ž pe) (π’ͺ X) (! X) ⁻¹

    Ξ³ : (𝟏[ π’ͺ X ] ≀[ poset-of (π’ͺ X) ] U) holds
    Ξ³ = 𝟏[ π’ͺ X ]     ＝⟨ β…  βŸ©β‚š
        (!κ™³[ X ] ⊀)  β‰€βŸ¨ β…‘ ⟩
        U            β– 

  ‑ : U ＝ 𝟏[ π’ͺ X ] β†’ (!⁎[ X ] U) holds
  ‑ p = Ξ³ ⋆
   where
    β…  : 𝟏[ π’ͺ X ] ＝ !κ™³[ X ] ⊀
    β…  = frame-homomorphisms-preserve-top (𝟎-π”½π•£π•ž pe) (π’ͺ X) (! X) ⁻¹

    q : (!κ™³[ X ] ⊀ ≀[ poset-of (π’ͺ X) ] U) holds
    q = !κ™³[ X ] ⊀ ＝⟨ β…  ⁻¹ βŸ©β‚š 𝟏[ π’ͺ X ] ＝⟨ p ⁻¹ βŸ©β‚š U β– 

    Ξ³ : (⊀ β‡’ !⁎[ X ] U) holds
    γ = adjunction-inequality-forward (! X) U ⊀ q


Accordingly, we define some suggestive notation, which we use when we want to
highlight this attitude on the right adjoint.


locale-forall-syntax : (X : Locale (𝓀 ⁺) 𝓀 𝓀) β†’ ⟨ π’ͺ X ⟩ β†’ Ξ© 𝓀
locale-forall-syntax X U = !⁎[ X ] U

syntax locale-forall-syntax X U = β±―[ X ] U
infix 7 locale-forall-syntax


\section{Characterization of compactness}

This result was added on 2025-04-29.

We work in a module parameterized by a locale `X`, being the locale whose
compactness we are interested in.


module CharacterizationOfCompactLocales (X : Locale (𝓀 ⁺) 𝓀 𝓀) where

 open Spectrality-of-𝟎 𝓀 pe

 open AdjointFunctorTheorem pt fe X (𝟏Loc pe) ∣ β„¬πŸŽβ†‘ , β„¬πŸŽβ†‘-is-basis ∣
 open PerfectMaps X (𝟏Loc pe) ∣ β„¬πŸŽβ†‘ , β„¬πŸŽβ†‘-is-basis ∣
 open SpectralMaps X (𝟏Loc pe)


An alternative way to express that a locale `X` is compact is by asserting that
the map `! X` is perfect, which is to say that the universal quantifier
`β±―[ X ]_` is Scott continuous.

Because a map into a spectral locale is perfect if and only if it reflects
compact opens (i.e. is β€œspectral”), this is the same thing as saying `! X` is
spectral.


 perfection-of-!-implies-the-spectrality-of-!
  : (is-perfect-map (! X) β‡’ is-spectral-map (! X)) holds
 perfection-of-!-implies-the-spectrality-of-! = perfect-maps-are-spectral (! X)

 spectrality-of-!-implies-the-perfection-of-!
  : (is-spectral-map (! X) β‡’ is-perfect-map (! X)) holds
 spectrality-of-!-implies-the-perfection-of-! Ο† =
  spectral-maps-are-perfect (𝟎-π”½π•£π•ž-is-spectral 𝓀 pe) (! X) Ο†


We now prove that this alternative formulation of compactness implies the
standard one.

The proof is quite simple:

- We have to show that the top `𝟏[ π’ͺ X ]` is compact.
- Because `!κ™³[ X ]` is a frame homomorphism, we have that `𝟏 = !κ™³[ X ] ⊀`,
  so it suffices to show that `!κ™³[ X ] ⊀` is compact.
- Since we are given that `!κ™³[ X ] ⊀` preserves compact opens, we just
  have to show that `⊀` is compact, which we know since the terminal locale
  is compact.


 perfection-of-!-gives-compactness : (is-perfect-map (! X) β‡’ is-compact X) holds
 perfection-of-!-gives-compactness ΞΊ =
  transport (Ξ» - β†’ is-compact-open X - holds) (q ⁻¹) †
   where
    open Spectrality-of-𝟎 𝓀 pe

    q : 𝟏[ π’ͺ X ] ＝ !κ™³[ X ] ⊀
    q = frame-homomorphisms-preserve-top (𝟎-π”½π•£π•ž pe) (π’ͺ X) (! X) ⁻¹

    𝕀 : SpectralMaps.is-spectral-map X (𝟏Loc pe) (! X) holds
    𝕀 = perfect-maps-are-spectral (! X) ΞΊ

    † : is-compact-open X (!κ™³[ X ] ⊀) holds
    † = 𝕀 𝟏[ 𝟎-π”½π•£π•ž pe ] (𝟎Frm-is-compact 𝓀 pe)


We now tackle the other direction.

- Suppose `X` is compact in the standard sense.
- Let `K : Ξ©` be a compact open of the terminal locale.
- We need to show that `!κ™³[ X ] K` is compact.
- Since `X` is a compact locale, and clopens are compact in compact frames, we
  simply have to show that `!κ™³[ X ] K` is a clopen.
- This is easy since we already know that `K` is a clopen in `Ξ©` (since `Ξ©` is
  a Stone locale, in which the clopens and the compact opens coincide) and
  frame homomorphisms preserve complements.


 compactness-gives-perfection-of-! : (is-compact X β‡’ is-perfect-map (! X)) holds
 compactness-gives-perfection-of-! ΞΊ = spectrality-of-!-implies-the-perfection-of-! †
  where
   † : is-spectral-map (! X) holds
   † P 𝕔 = clopens-are-compact-in-compact-frames (π’ͺ X) ΞΊ (!κ™³[ X ] P) ‑
    where
     ΞΎ : is-clopen (𝟎-π”½π•£π•ž pe) P holds
     ΞΎ = compact-implies-clopen pe P 𝕔

     Pβ€² : Ξ© 𝓀
     Pβ€² = pr₁ ΞΎ

     ΞΆ : is-complement-of (π’ͺ X) (!κ™³[ X ] Pβ€²) (!κ™³[ X ] P)
     ΞΆ = frame-homomorphisms-preserve-complements
          (𝟎-π”½π•£π•ž pe)
          (π’ͺ X)
          (! X)(complementation-is-symmetric (𝟎-π”½π•£π•ž pe) _ _ (prβ‚‚ ΞΎ))

     ‑ : is-clopen (π’ͺ X) (!κ™³[ X ] P) holds
     ‑ = !κ™³[ X ] Pβ€² , ΞΆ


\section{Acknowledgements}

I have benefited from Graham Manuell's notes on constructive locale theory [1],
where this characterization of compactness is discussed. The proof here is
different, however, as it uses the machinery of spectral and perfect maps.

[1]: Manuell, Graham. "Pointfree topology and constructive mathematics." arXiv
preprint arXiv:2304.06000 (2023).