---
title:      Properties of the Scott topology
author:     Ayberk Tosun
start-date: 2023-10-30
---

\begin{code}

{-# OPTIONS --safe --without-K --exact-split #-}

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.SubtypeClassifier

module DomainTheory.Topology.ScottTopologyProperties
(pt : propositional-truncations-exist)
(fe : Fun-Ext)
(π₯  : Universe) where

open import UF.Logic
open Existential pt
open Implication fe
open Universal   fe
open Conjunction

open import UF.Size
open import UF.Equiv

open import UF.Powerset-MultiUniverse
open import Slice.Family

open PropositionalTruncation pt

open import DomainTheory.Topology.ScottTopology        pt fe π₯
open import DomainTheory.Basics.Dcpo                   pt fe π₯
open import DomainTheory.BasesAndContinuity.Continuity pt fe π₯
open import DomainTheory.Basics.WayBelow               pt fe π₯

\end{code}

\begin{code}

principal-filter : (π : DCPO {π€} {π₯}) β β¨ π β© β π β¨ π β©
principal-filter π c x = c ββ¨ π β© x , prop-valuedness π c x

infix 45 principal-filter

syntax principal-filter π x = β[ π ] x

\end{code}

Let D be a dcpo and consider a compact element c : D of it. The
upwards-closure of c is then a Scott open.

\begin{code}

module Properties (π : DCPO {π€} {π₯}) where

open DefnOfScottTopology π π₯

principal-filter-is-upwards-closed : (x : β¨ π β©)
β is-upwards-closed (β[ π ] x) holds
principal-filter-is-upwards-closed x y z p q =
x ββ¨ π β©[ p ] y ββ¨ π β©[ q ] z ββ¨ π β©

compact-implies-principal-filter-is-scott-open : (c : β¨ π β©)
β is-compact π c
β is-scott-open (β[ π ] c) holds
compact-implies-principal-filter-is-scott-open c ΞΊ = β  , β‘
where
β  : is-upwards-closed (β[ π ] c) holds
β  = principal-filter-is-upwards-closed c

β‘ : is-inaccessible-by-directed-joins (β[ π ] c) holds
β‘ (S , Ξ΄) = ΞΊ (index S) (S [_]) Ξ΄

\end{code}

Conversely, if the principal filter is Scott open then c is a compact element.

\begin{code}

principal-filter-scott-open-implies-compact : (c : β¨ π β©)
β is-scott-open (β[ π ] c) holds
β is-compact π c
principal-filter-scott-open-implies-compact c (Ο , ΞΊ) I ΞΉ Ξ΄ p =
ΞΊ ((I , ΞΉ) , Ξ΄) p

\end{code}

We can now record this as a logical equivalence.

\begin{code}

principal-filter-scott-open-iff-compact :
(x : β¨ π β©) β is-scott-open (β[ π ] x) holds β is-compact π x
principal-filter-scott-open-iff-compact x = β  , β‘
where
β  = principal-filter-scott-open-implies-compact x
β‘ = compact-implies-principal-filter-is-scott-open x

\end{code}

Notation for the principal Scott open.

\begin{code}

βΛ’[_] : (Ξ£ c κ β¨ π β© , is-compact π c) β Ξ£ S κ π {π₯} β¨ π β© , is-scott-open S holds
βΛ’[ (c , ΞΊ) ] =
principal-filter π c , compact-implies-principal-filter-is-scott-open c ΞΊ

\end{code}

We now prove some properties of the Scott topology on a dcpo that is algebraic.

\begin{code}

module PropertiesAlgebraic (π : DCPO {π€} {π₯})
(π : structurally-algebraic π) where

open DefnOfScottTopology π π₯

open structurally-algebraic

is-compactβ : β¨ π β© β Ξ© (π€ β π₯ βΊ)
is-compactβ x = is-compact π x , being-compact-is-prop π x

join-of-compact-opens : π {π₯} β¨ π β© β π {π€ β π₯ βΊ} β¨ π β©
join-of-compact-opens U x =
Ζ c κ β¨ π β© , (is-compactβ c β§ c ββ U β§ x ββ (β[ π ] c)) holds

characterization-of-scott-opensβ : (U : π β¨ π β©)
β is-scott-open U holds
β U β join-of-compact-opens U
characterization-of-scott-opensβ U (Ο , ΞΎ) x p = β
where
S : Fam π₯ β¨ π β©
S = index-of-compact-family π x , compact-family π x

Sβ : Famβ
Sβ = S , compact-family-is-directed π x

q : x οΌ β Sβ
q = compact-family-β-οΌ π x β»ΒΉ

ΞΊ : (i : index S) β is-compactβ (S [ i ]) holds
ΞΊ = compact-family-is-compact π x

Ο : is-upperbound (underlying-order π) x (S [_])
Ο i = transport (Ξ» - β (S [ i ]) ββ¨ π β© -) (q β»ΒΉ) (β-is-upperbound Sβ i)

Ο : (β Sβ) β U
Ο = transport (Ξ» - β - β U) q p

β‘ : Ξ£ i κ index S , (S [ i ]) β U
β β cβ κ β¨ π β© , (is-compactβ cβ β§ cβ ββ U β§ x ββ β[ π ] cβ) holds
β‘ (i , ΞΌ) = β£ S [ i ] , ΞΊ i , ΞΌ , Ο i β£

β  : β cβ κ β¨ π β© , (is-compactβ cβ β§ cβ ββ U β§ x ββ β[ π ] cβ) holds
β  = β₯β₯-rec β-is-prop β‘ (ΞΎ Sβ Ο)

characterization-of-scott-opensβ : (U : π β¨ π β©)
β is-scott-open U holds
β join-of-compact-opens U β U
characterization-of-scott-opensβ U (Ο , _) x p =
β₯β₯-rec (holds-is-prop (x ββ U)) β  p
where
β  : Ξ£ c κ β¨ π β© , (is-compactβ c β§ c ββ U β§ principal-filter π c x) holds
β x ββ U holds
β  (c , _ , q , r) = Ο c x q r

characterization-of-scott-opens
: (U : π {π₯} β¨ π β©)
β (is-scott-open U β (β±― x κ β¨ π β© , U x β join-of-compact-opens U x)) holds
characterization-of-scott-opens U Ο x = β¦ββ¦ , β¦ββ¦
where
β¦ββ¦ = characterization-of-scott-opensβ U Ο x
β¦ββ¦ = characterization-of-scott-opensβ U Ο x

resize-join-of-compact-opens : (U : π {π₯} β¨ π β©) (x : β¨ π β©)
β is-scott-open U holds
β (join-of-compact-opens U x holds) is π₯ small
resize-join-of-compact-opens U x Ο = x β U , Ξ΅
where
Ξ΅ : (x β U) β join-of-compact-opens U x holds
Ξ΅ = logically-equivalent-props-are-equivalent
(holds-is-prop (U x))
β-is-prop
(characterization-of-scott-opensβ U Ο x)
(characterization-of-scott-opensβ U Ο x)

\end{code}

The principal filter on the bottom element is the top open of the Scott locale.
We write this down in a different submodule as it requires the additional
assumption of a bottom element in the algebraic dcpo in consideration.

\begin{code}

module BottomLemma (π  : DCPO {π€} {π₯})
(π  : structurally-algebraic π)
(hl : has-least (underlying-order π)) where

β₯α΄° : β¨ π β©
β₯α΄° = prβ hl

β₯α΄°-is-least : is-least (underlying-order π) β₯α΄°
β₯α΄°-is-least = prβ hl

open Properties π

open DefnOfScottTopology π π₯
open PropertiesAlgebraic π π

bottom-principal-filter-is-top : (π : πͺβ) β π .prβ β β[ π ] β₯α΄°
bottom-principal-filter-is-top π x _ = β₯α΄°-is-least x

\end{code}

If a Scott open contains β₯ then it contains everything by upward closure.