Locales.ScottLocale.Properties

---
title:         Properties of the Scott locale
author:        Ayberk Tosun
date-started:  2023-11-23
dates-updated: [2024-03-16]
---


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

open import MLTT.Spartan
open import Slice.Family
open import UF.FunExt
open import UF.Logic
open import UF.PropTrunc
open import UF.SubtypeClassifier
open import UF.Subsingletons


We assume the existence of propositional truncations as well as function
extensionality.


module Locales.ScottLocale.Properties (pt : propositional-truncations-exist)
                                      (fe : Fun-Ext)
                                      (𝓤  : Universe) where

open import DomainTheory.BasesAndContinuity.Bases            pt fe 𝓤
open import DomainTheory.Basics.Dcpo                         pt fe 𝓤
 renaming (⟨_⟩ to ⟨_⟩∙) hiding   (is-directed)
open import DomainTheory.Basics.WayBelow                     pt fe 𝓤
open import DomainTheory.Topology.ScottTopology              pt fe 𝓤
open import DomainTheory.Topology.ScottTopologyProperties    pt fe 𝓤
open import Locales.Compactness.Definition                              pt fe
 hiding (is-compact)
open import Locales.Frame                                    pt fe
open import Locales.ScottLocale.Definition                   pt fe 𝓤
open import Locales.ScottLocale.ScottLocalesOfAlgebraicDcpos pt fe 𝓤

open AllCombinators pt fe
open Locale
open PropositionalTruncation pt


Moved from the `ScottLocalesOfScottDomains` module to here on 2024-03-16.


bounded-above : (𝓓 : DCPO {𝓤 ⁺} {𝓤}) → ⟨ 𝓓 ⟩∙ → ⟨ 𝓓 ⟩∙ → Ω (𝓤 ⁺)
bounded-above 𝓓 x y = ∥ upper-bound (binary-family 𝓤 x y) ∥Ω
 where
  open Joins (λ a b → a ⊑⟨ 𝓓 ⟩ₚ b)

infix  bounded-above

syntax bounded-above 𝓓 x y = x ↑[ 𝓓 ] y



module ScottLocaleProperties
        (𝓓    : DCPO {𝓤 ⁺} {𝓤})
        (hl   : has-least (underlying-order 𝓓))
        (hscb : has-specified-small-compact-basis 𝓓)
        (pe   : propext 𝓤)
       where

 open ScottLocaleConstruction 𝓓 hscb pe

 private
  B : 𝓤 ̇
  B = index-of-compact-basis 𝓓 hscb

  β : B → ⟨ 𝓓 ⟩∙
  β i = family-of-compact-elements 𝓓 hscb i

 open Properties  𝓓
 open BottomLemma 𝓓 𝕒 hl

 ⊥κ : is-compact 𝓓 ⊥ᴰ
 ⊥κ = ⊥-is-compact (𝓓 , hl)

 Σ⦅𝓓⦆ : Locale (𝓤 ⁺) 𝓤 𝓤
 Σ⦅𝓓⦆ = ScottLocale

 open DefnOfScottLocale 𝓓 𝓤 pe using (_⊆ₛ_)


Recall that `↑ˢ[ x , p ]` denotes the principal filter on a compact element `x`,
(where `p` is the proof that `x` is compact).

Below, we prove that `↑ˢ[ ⊥ᵈ , p ] = 𝟏` where `𝟏` is the top Scott open of the
Scott locale on `𝓓`.


 ↑⊥-is-below-𝟏 : (𝟏[ 𝒪 Σ⦅𝓓⦆ ] ⊆ₛ ↑ˢ[ ⊥ᴰ , ⊥κ ]) holds
 ↑⊥-is-below-𝟏 = bottom-principal-filter-is-top 𝟏[ 𝒪 Σ⦅𝓓⦆ ]

 ↑⊥-is-top : ↑ˢ[ ⊥ᴰ , ⊥κ ] ＝ 𝟏[ 𝒪 Σ⦅𝓓⦆ ]
 ↑⊥-is-top = only-𝟏-is-above-𝟏 (𝒪 Σ⦅𝓓⦆) ↑ˢ[ ⊥ᴰ , ⊥κ ] †
  where
   † : (𝟏[ 𝒪 Σ⦅𝓓⦆ ] ≤[ poset-of (𝒪 Σ⦅𝓓⦆) ] ↑ˢ[ ⊥ᴰ , ⊥κ ]) holds
   † = ⊆ₛ-implies-⊆ₖ 𝟏[ 𝒪 Σ⦅𝓓⦆ ] ↑ˢ[ ⊥ᴰ , ⊥κ ] ↑⊥-is-below-𝟏

 open DefnOfScottTopology 𝓓 𝓤

 contains-bottom-implies-is-𝟏 : (𝔘 : ⟨ 𝒪 Σ⦅𝓓⦆ ⟩)
                              → (⊥ᴰ ∈ₛ 𝔘) holds
                              → 𝔘 ＝ 𝟏[ 𝒪 Σ⦅𝓓⦆ ]
 contains-bottom-implies-is-𝟏 𝔘 μ = only-𝟏-is-above-𝟏 (𝒪 Σ⦅𝓓⦆) 𝔘 †
  where
   † : (𝟏[ 𝒪 ScottLocale ] ⊆ₖ 𝔘) holds
   † = ⊆ₛ-implies-⊆ₖ
        𝟏[ 𝒪 ScottLocale ]
        𝔘
        (λ { x ⋆ → contains-bottom-implies-is-top 𝔘 μ x})


Moved from the `ScottLocalesOfScottDomains` module to here on 2024-03-16.

The principal filter `↑(x)` on any `x : 𝓓` is a compact Scott open.


 principal-filter-is-compact₀ : (c : ⟨ 𝓓 ⟩∙)
                              → (κ : is-compact 𝓓 c)
                              → is-compact-open Σ⦅𝓓⦆ ↑ˢ[ (c , κ) ] holds
 principal-filter-is-compact₀ c κ S δ p = ∥∥-functor † μ
  where
   μ : (c ∈ₛ (⋁[ 𝒪 Σ⦅𝓓⦆ ] S)) holds
   μ = ⊆ₖ-implies-⊆ₛ ↑ˢ[ (c , κ) ] (⋁[ 𝒪 Σ⦅𝓓⦆ ] S) p c (reflexivity 𝓓 c)

   † : Σ i ꞉ index S , (c ∈ₛ (S [ i ])) holds
     → Σ i ꞉ index S , (↑ˢ[ (c , κ) ] ≤[ poset-of (𝒪 Σ⦅𝓓⦆) ] S [ i ]) holds
   † (i , r) = i , ‡
    where
     ‡ :  (↑ˢ[ c , κ ] ≤[ poset-of (𝒪 Σ⦅𝓓⦆) ] (S [ i ])) holds
     ‡ d = upward-closure (S [ i ]) c (β d) r


Moved from the `ScottLocalesOfScottDomains` module to here on 2024-03-16.

The Scott locale is always compact.


 ⊤-is-compact : is-compact-open Σ⦅𝓓⦆ 𝟏[ 𝒪 Σ⦅𝓓⦆ ] holds
 ⊤-is-compact = transport (λ - → is-compact-open Σ⦅𝓓⦆ - holds) ↑⊥-is-top †
  where
   † : is-compact-open ScottLocale ↑ˢ[ ⊥ᴰ , ⊥κ ] holds
   † = principal-filter-is-compact₀ ⊥ᴰ ⊥κ


Moved from the `ScottLocalesOfScottDomains` module to here on 2024-03-16.

If two compact elements `c` and `d` do not have an upper bound, then the meet
of their principal filters is the empty Scott open.


 not-bounded-lemma : (c d : ⟨ 𝓓 ⟩∙)
                   → (κᶜ : is-compact 𝓓 c)
                   → (κᵈ : is-compact 𝓓 d)
                   → ¬ ((c ↑[ 𝓓 ] d) holds)
                   → ↑ˢ[ c , κᶜ ] ∧[ 𝒪 Σ⦅𝓓⦆ ] ↑ˢ[ d , κᵈ ] ＝ 𝟎[ 𝒪 Σ⦅𝓓⦆ ]
 not-bounded-lemma c d κᶜ κᵈ ν =
  only-𝟎-is-below-𝟎 (𝒪 Σ⦅𝓓⦆) (↑ˢ[ c , κᶜ ] ∧[ 𝒪 Σ⦅𝓓⦆ ] ↑ˢ[ d , κᵈ ]) †
   where
    † : ((↑ˢ[ c , κᶜ ] ∧[ 𝒪 Σ⦅𝓓⦆ ] ↑ˢ[ d , κᵈ ]) ⊆ₖ 𝟎[ 𝒪 Σ⦅𝓓⦆ ]) holds
    † i (p₁ , p₂) = 𝟘-elim (ν ∣ β i , (λ { (inl ⋆) → p₁ ; (inr ⋆) → p₂}) ∣)