Ayberk Tosun, 9 December 2021
Based on `ayberkt/formal-topology-in-UF`.
\begin{code}[hide]
{-# OPTIONS --safe --without-K --lossy-unification #-}
open import MLTT.List hiding ([_])
open import MLTT.Spartan hiding (𝟚)
open import UF.Base
open import UF.FunExt
open import UF.PropTrunc
module Locales.CompactRegular
(pt : propositional-truncations-exist)
(fe : Fun-Ext)
where
open import Locales.AdjointFunctorTheoremForFrames
open import Locales.ContinuousMap.Definition pt fe
open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe
open import Locales.ContinuousMap.FrameHomomorphism-Properties pt fe
open import Locales.Frame pt fe hiding (is-directed)
open import Locales.InitialFrame pt fe
open import Slice.Family
open import UF.Equiv using (_≃_; logical-equivs-of-props-are-equivs)
open import UF.Logic
open import UF.Subsingletons
open import UF.SubtypeClassifier
open AllCombinators pt fe
open PropositionalTruncation pt
open import Locales.GaloisConnection pt fe
\end{code}
\section{The way below relation}
We first define the notion of a directed family. This is actually
defined in the `Dcpo` module but I am redefining it here to avoid
importing the `Dcpo` module. There are also some things about that
definition that make it a bit inconvenient to work with. It might be
good idea to address this duplication at some point.
\begin{code}
is-directed : (P : Poset 𝓤 𝓥) → (S : Fam 𝓦 ∣ P ∣ₚ) → Ω (𝓥 ⊔ 𝓦)
is-directed P (I , s) =
∥ I ∥Ω
∧ (Ɐ i ꞉ I , Ɐ j ꞉ I , Ǝ k ꞉ I , ((s i ≤ s k) ∧ (s j ≤ s k)) holds)
where open PosetNotation P using (_≤_)
\end{code}
\begin{code}
way-below : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → ⟨ F ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
way-below {𝓤 = 𝓤} {𝓦 = 𝓦} F U V =
Ɐ S ꞉ Fam 𝓦 ⟨ F ⟩ , is-directed (poset-of F) S ⇒
V ≤ (⋁[ F ] S) ⇒ (Ǝ i ꞉ index S , (U ≤ S [ i ]) holds)
where
open PosetNotation (poset-of F) using (_≤_)
infix 5 way-below
syntax way-below F U V = U ≪[ F ] V
\end{code}
A compact open is one that is way below itself.
\begin{code}
is-compact-open : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
is-compact-open F U = U ≪[ F ] U
\end{code}
A compact frame is simply a frame whose top element is finite.
\begin{code}
is-compact : Frame 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
is-compact F = is-compact-open F 𝟏[ F ]
\end{code}
Compacts opens are always closed undery binary joins.
\begin{code}
compacts-are-closed-under-joins : (F : Frame 𝓤 𝓥 𝓦)
→ (U V : ⟨ F ⟩)
→ is-compact-open F U holds
→ is-compact-open F V holds
→ is-compact-open F (U ∨[ F ] V) holds
compacts-are-closed-under-joins F U V κ₁ κ₂ S dir@(_ , up) p =
∥∥-rec₂ ∃-is-prop γ s₁′ s₂′
where
open PosetNotation (poset-of F) using (_≤_)
open PosetReasoning (poset-of F)
\end{code}
We know that both `U` and `V` are covered by `S` by the assumption that `U ∨ V`
is covered by `S`
\begin{code}
q₁ : (U ≤ (⋁[ F ] S)) holds
q₁ = U ≤⟨ ∨[ F ]-upper₁ U V ⟩ U ∨[ F ] V ≤⟨ p ⟩ ⋁[ F ] S ■
q₂ : (V ≤ (⋁[ F ] S)) holds
q₂ = V ≤⟨ ∨[ F ]-upper₂ U V ⟩ U ∨[ F ] V ≤⟨ p ⟩ ⋁[ F ] S ■
\end{code}
Therefore there must exist indices `i₁` and `i₂` such that `U ≤ Sᵢ₁` and `V ≤
Sᵢ₂`.
\begin{code}
s₁′ : ∥ Σ i₁ ꞉ index S , (U ≤ S [ i₁ ]) holds ∥
s₁′ = κ₁ S dir q₁
s₂′ : ∥ Σ i₂ ꞉ index S , (V ≤ S [ i₂ ]) holds ∥
s₂′ = κ₂ S dir q₂
γ : (Σ i₁ ꞉ index S , (U ≤ S [ i₁ ]) holds)
→ (Σ i₂ ꞉ index S , (V ≤ S [ i₂ ]) holds)
→ ∃ i ꞉ index S , ((U ∨[ F ] V) ≤ S [ i ]) holds
γ (i₁ , s₁) (i₂ , s₂) = ∥∥-rec ∃-is-prop δ (up i₁ i₂)
where
δ : Σ i ꞉ index S , ((S [ i₁ ] ≤ S [ i ]) ∧ (S [ i₂ ] ≤ S [ i ])) holds
→ ∃ i ꞉ index S , ((U ∨[ F ] V) ≤ S [ i ]) holds
δ (i , r₁ , r₂) = ∣ i , ∨[ F ]-least ε ζ ∣
where
ε : (U ≤ S [ i ]) holds
ε = U ≤⟨ s₁ ⟩ S [ i₁ ] ≤⟨ r₁ ⟩ S [ i ] ■
ζ : (V ≤ S [ i ]) holds
ζ = V ≤⟨ s₂ ⟩ S [ i₂ ] ≤⟨ r₂ ⟩ S [ i ] ■
\end{code}
\section{Well Inside}
`well-inside₀` is the type family expressing that a given open of a frame is
clopen.
\begin{code}
well-inside₀ : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → ⟨ F ⟩ → 𝓤 ̇
well-inside₀ F U V =
Σ W ꞉ ⟨ F ⟩ , (U ∧[ F ] W ＝ 𝟎[ F ]) × (V ∨[ F ] W ＝ 𝟏[ F ])
infix 4 well-inside₀
syntax well-inside₀ F U V = U ⋜₀[ F ] V
\end{code}
The well inside relation is not propositional in general, even though the “has
complement” predicate (i.e. is well inside itself) is propositional.
\begin{code}
well-inside₀-is-not-prop : propext 𝓤₀
→ Σ F ꞉ Frame 𝓤₁ 𝓤₀ 𝓤₀ ,
(¬ ((U V : ⟨ F ⟩) → is-prop (U ⋜₀[ F ] V)))
well-inside₀-is-not-prop pe = IF , ε
where
IF : Frame 𝓤₁ 𝓤₀ 𝓤₀
IF = 𝟎-𝔽𝕣𝕞 pe
γ₂ : 𝟎[ IF ] ⋜₀[ IF ] 𝟏[ IF ]
γ₂ = 𝟏[ IF ] , (β , γ)
where
abstract
β : 𝟎[ IF ] ∧[ IF ] 𝟏[ IF ] ＝ 𝟎[ IF ]
β = 𝟎-left-annihilator-for-∧ IF 𝟏[ IF ]
γ : 𝟏[ IF ] ∨[ IF ] 𝟏[ IF ] ＝ 𝟏[ IF ]
γ = 𝟏-right-annihilator-for-∨ IF 𝟏[ IF ]
γ₁ : 𝟎[ IF ] ⋜₀[ IF ] 𝟏[ IF ]
γ₁ = 𝟎[ IF ] , (β , γ)
where
abstract
β : 𝟎[ IF ] ∧[ IF ] 𝟎[ IF ] ＝ 𝟎[ IF ]
β = 𝟎-right-annihilator-for-∧ IF 𝟎[ IF ]
γ : 𝟏[ IF ] ∨[ IF ] 𝟎[ IF ] ＝ 𝟏[ IF ]
γ = 𝟏-left-annihilator-for-∨ IF 𝟎[ IF ]
𝟎-is-not-𝟏 : ¬ (𝟎[ IF ] ＝ 𝟏[ IF ])
𝟎-is-not-𝟏 p = γ
where
γ : ⊥ holds
γ = transport _holds (𝟏[ IF ] ＝⟨ p ⁻¹ ⟩ 𝟎[ IF ] ＝⟨ 𝟎-of-IF-is-⊥ pe ⟩ ⊥ ∎) ⋆
ε : ¬ ((U V : ⟨ IF ⟩) → is-prop (well-inside₀ IF U V))
ε ψ = 𝟎-is-not-𝟏 (pr₁ (from-Σ-＝ δ))
where
δ : γ₁ ＝ γ₂
δ = ψ 𝟎[ IF ] 𝟏[ IF ] γ₁ γ₂
\end{code}
Because well inside is not propositional, we have to truncate it to get a
relation.
\begin{code}
well-inside : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → ⟨ F ⟩ → Ω 𝓤
well-inside F U V = ∥ U ⋜₀[ F ] V ∥Ω
infix 4 well-inside
syntax well-inside F U V = U ⋜[ F ] V
\end{code}
\begin{code}
well-inside-implies-below : (F : Frame 𝓤 𝓥 𝓦)
→ (U V : ⟨ F ⟩)
→ (U ⋜[ F ] V ⇒ (U ≤[ poset-of F ] V)) holds
well-inside-implies-below F U V = ∥∥-rec (holds-is-prop (U ≤[ poset-of F ] V)) γ
where
_⊓_ = λ U V → U ∧[ F ] V
γ : U ⋜₀[ F ] V → (U ≤[ poset-of F ] V) holds
γ (W , c₁ , c₂) = connecting-lemma₂ F δ
where
δ : U ＝ U ∧[ F ] V
δ = U ＝⟨ 𝟏-right-unit-of-∧ F U ⁻¹ ⟩
U ⊓ 𝟏[ F ] ＝⟨ ap (U ⊓_) (c₂ ⁻¹) ⟩
U ⊓ (V ∨[ F ] W) ＝⟨ binary-distributivity F U V W ⟩
(U ⊓ V) ∨[ F ] (U ⊓ W) ＝⟨ ap (λ - → binary-join F (U ⊓ V) -) c₁ ⟩
(U ⊓ V) ∨[ F ] 𝟎[ F ] ＝⟨ 𝟎-left-unit-of-∨ F (U ⊓ V) ⟩
U ⊓ V ∎
\end{code}
\begin{code}
↑↑-is-upwards-closed : (F : Frame 𝓤 𝓥 𝓦)
→ {U V W : ⟨ F ⟩}
→ (U ⋜[ F ] V) holds
→ (V ≤[ poset-of F ] W) holds
→ (U ⋜[ F ] W) holds
↑↑-is-upwards-closed F {U} {V} {W} p q =
∥∥-rec (holds-is-prop (U ⋜[ F ] W)) γ p
where
open PosetReasoning (poset-of F)
γ : U ⋜₀[ F ] V → (U ⋜[ F ] W) holds
γ (T , c₁ , c₂) = ∣ T , c₁ , d₂ ∣
where
β : (𝟏[ F ] ≤[ poset-of F ] (W ∨[ F ] T)) holds
β = 𝟏[ F ] ＝⟨ c₂ ⁻¹ ⟩ₚ
V ∨[ F ] T ≤⟨ ∨[ F ]-left-monotone q ⟩
W ∨[ F ] T ■
d₂ : W ∨[ F ] T ＝ 𝟏[ F ]
d₂ = only-𝟏-is-above-𝟏 F (W ∨[ F ] T) β
↓↓-is-downwards-closed : (F : Frame 𝓤 𝓥 𝓦)
→ {U V W : ⟨ F ⟩}
→ (V ⋜[ F ] W) holds
→ (U ≤[ poset-of F ] V) holds
→ (U ⋜[ F ] W) holds
↓↓-is-downwards-closed F {U} {V} {W} p q = ∥∥-rec ∥∥-is-prop γ p
where
open PosetReasoning (poset-of F)
γ : V ⋜₀[ F ] W → (U ⋜[ F ] W) holds
γ (T , c₁ , c₂) = ∣ T , (only-𝟎-is-below-𝟎 F (U ∧[ F ] T) β , c₂) ∣
where
β : ((U ∧[ F ] T) ≤[ poset-of F ] 𝟎[ F ]) holds
β = U ∧[ F ] T ≤⟨ ∧[ F ]-left-monotone q ⟩
V ∧[ F ] T ＝⟨ c₁ ⟩ₚ
𝟎[ F ] ■
\end{code}
An open _U_ in a frame _A_ is *clopen* iff it is well-inside itself.
\begin{code}
is-boolean-complement-of : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → ⟨ F ⟩ → Ω 𝓤
is-boolean-complement-of F U′ U =
(U ∧[ F ] U′ ＝[ iss ]＝ 𝟎[ F ]) ∧ (U ∨[ F ] U′ ＝[ iss ]＝ 𝟏[ F ])
where
iss = carrier-of-[ poset-of F ]-is-set
complementation-is-symmetric : (F : Frame 𝓤 𝓥 𝓦) (x y : ⟨ F ⟩)
→ (is-boolean-complement-of F x y
⇒ is-boolean-complement-of F y x) holds
complementation-is-symmetric F x y (φ , ψ) = † , ‡
where
† : x ∧[ F ] y ＝ 𝟎[ F ]
† = x ∧[ F ] y ＝⟨ ∧[ F ]-is-commutative x y ⟩ y ∧[ F ] x ＝⟨ φ ⟩ 𝟎[ F ] ∎
‡ : x ∨[ F ] y ＝ 𝟏[ F ]
‡ = x ∨[ F ] y ＝⟨ ∨[ F ]-is-commutative x y ⟩ y ∨[ F ] x ＝⟨ ψ ⟩ 𝟏[ F ] ∎
∧-complement : (F : Frame 𝓤 𝓥 𝓦)
→ {x y x′ y′ : ⟨ F ⟩}
→ is-boolean-complement-of F x x′ holds
→ is-boolean-complement-of F y y′ holds
→ is-boolean-complement-of F (x′ ∨[ F ] y′) (x ∧[ F ] y) holds
∧-complement F {x} {y} {x′} {y′} φ ψ = β , γ
where
open PosetReasoning (poset-of F)
_⊓_ = λ x y → x ∧[ F ] y
φ₀ : x ⊓ x′ ＝ 𝟎[ F ]
φ₀ = x ⊓ x′ ＝⟨ ∧[ F ]-is-commutative x x′ ⟩ x′ ⊓ x ＝⟨ pr₁ φ ⟩ 𝟎[ F ] ∎
ψ₀ : y ⊓ y′ ＝ 𝟎[ F ]
ψ₀ = y ⊓ y′ ＝⟨ ∧[ F ]-is-commutative y y′ ⟩ y′ ⊓ y ＝⟨ pr₁ ψ ⟩ 𝟎[ F ] ∎
φ₁ : x ∨[ F ] x′ ＝ 𝟏[ F ]
φ₁ = x ∨[ F ] x′ ＝⟨ ∨[ F ]-is-commutative x x′ ⟩
x′ ∨[ F ] x ＝⟨ pr₂ φ ⟩
𝟏[ F ] ∎
β : (x ∧[ F ] y) ∧[ F ] (x′ ∨[ F ] y′) ＝ 𝟎[ F ]
β = (x ⊓ y) ⊓ (x′ ∨[ F ] y′) ＝⟨ Ⅰ ⟩
((x ⊓ y) ⊓ x′) ∨[ F ] ((x ⊓ y) ⊓ y′) ＝⟨ Ⅱ ⟩
((y ⊓ x) ⊓ x′) ∨[ F ] ((x ⊓ y) ⊓ y′) ＝⟨ Ⅲ ⟩
(y ⊓ (x ⊓ x′)) ∨[ F ] ((x ⊓ y) ⊓ y′) ＝⟨ Ⅳ ⟩
(y ⊓ 𝟎[ F ]) ∨[ F ] ((x ⊓ y) ⊓ y′) ＝⟨ Ⅴ ⟩
𝟎[ F ] ∨[ F ] ((x ⊓ y) ⊓ y′) ＝⟨ Ⅵ ⟩
(x ⊓ y) ⊓ y′ ＝⟨ Ⅶ ⟩
x ⊓ (y ⊓ y′) ＝⟨ Ⅷ ⟩
x ⊓ 𝟎[ F ] ＝⟨ Ⅸ ⟩
𝟎[ F ] ∎
where
Ⅰ = binary-distributivity F (x ⊓ y) x′ y′
Ⅱ = ap (λ - → (- ⊓ x′) ∨[ F ] ((x ⊓ y) ⊓ y′)) (∧[ F ]-is-commutative x y)
Ⅲ = ap (λ - → - ∨[ F ] ((x ⊓ y) ⊓ y′)) (∧[ F ]-is-associative y x x′ ⁻¹)
Ⅳ = ap (λ - → (y ⊓ -) ∨[ F ] ((x ⊓ y) ⊓ y′)) φ₀
Ⅴ = ap (λ - → - ∨[ F ] ((x ⊓ y) ⊓ y′)) (𝟎-right-annihilator-for-∧ F y)
Ⅵ = 𝟎-right-unit-of-∨ F ((x ⊓ y) ⊓ y′)
Ⅶ = ∧[ F ]-is-associative x y y′ ⁻¹
Ⅷ = ap (λ - → x ⊓ -) ψ₀
Ⅸ = 𝟎-right-annihilator-for-∧ F x
γ : (x ⊓ y) ∨[ F ] (x′ ∨[ F ] y′) ＝ 𝟏[ F ]
γ = (x ⊓ y) ∨[ F ] (x′ ∨[ F ] y′) ＝⟨ Ⅰ ⟩
(x′ ∨[ F ] y′) ∨[ F ] (x ⊓ y) ＝⟨ Ⅱ ⟩
((x′ ∨[ F ] y′) ∨[ F ] x) ∧[ F ] ((x′ ∨[ F ] y′) ∨[ F ] y) ＝⟨ Ⅲ ⟩
((y′ ∨[ F ] x′) ∨[ F ] x) ∧[ F ] ((x′ ∨[ F ] y′) ∨[ F ] y) ＝⟨ Ⅳ ⟩
(y′ ∨[ F ] (x′ ∨[ F ] x)) ∧[ F ] ((x′ ∨[ F ] y′) ∨[ F ] y) ＝⟨ Ⅴ ⟩
(y′ ∨[ F ] 𝟏[ F ]) ∧[ F ] ((x′ ∨[ F ] y′) ∨[ F ] y) ＝⟨ Ⅵ ⟩
𝟏[ F ] ∧[ F ] ((x′ ∨[ F ] y′) ∨[ F ] y) ＝⟨ Ⅶ ⟩
(x′ ∨[ F ] y′) ∨[ F ] y ＝⟨ Ⅷ ⟩
x′ ∨[ F ] (y′ ∨[ F ] y) ＝⟨ Ⅸ ⟩
x′ ∨[ F ] 𝟏[ F ] ＝⟨ Ⅹ ⟩
𝟏[ F ] ∎
where
† = ∨[ F ]-is-commutative x′ y′
‡ = 𝟏-right-annihilator-for-∨ F y′
Ⅰ = ∨[ F ]-is-commutative (x ⊓ y) (x′ ∨[ F ] y′)
Ⅱ = binary-distributivity-op F (x′ ∨[ F ] y′) x y
Ⅲ = ap (λ - → (- ∨[ F ] x) ∧[ F ] ((_ ∨[ F ] _) ∨[ F ] y)) †
Ⅳ = ap (λ - → - ∧[ F ] ((x′ ∨[ F ] y′) ∨[ F ] y)) (∨[ F ]-assoc y′ x′ x)
Ⅴ = ap (λ - → (y′ ∨[ F ] -) ∧[ F ] ((x′ ∨[ F ] y′) ∨[ F ] y)) (pr₂ φ)
Ⅵ = ap (λ - → - ∧[ F ] ((x′ ∨[ F ] y′) ∨[ F ] y)) ‡
Ⅶ = 𝟏-left-unit-of-∧ F ((x′ ∨[ F ] y′) ∨[ F ] y)
Ⅷ = ∨[ F ]-assoc x′ y′ y
Ⅸ = ap (λ - → x′ ∨[ F ] -) (pr₂ ψ)
Ⅹ = 𝟏-right-annihilator-for-∨ F x′
is-complement-of : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → ⟨ F ⟩ → 𝓤 ̇
is-complement-of F x′ x = (x ∧[ F ] x′ ＝ 𝟎[ F ]) × (x ∨[ F ] x′ ＝ 𝟏[ F ])
is-clopen₀ : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → 𝓤 ̇
is-clopen₀ F U = Σ W ꞉ ⟨ F ⟩ , is-complement-of F W U
is-clopen₀-is-prop : (F : Frame 𝓤 𝓥 𝓦) → (U : ⟨ F ⟩) → is-prop (is-clopen₀ F U)
is-clopen₀-is-prop F U (W₁ , p₁ , q₁) (W₂ , p₂ , q₂) = to-subtype-＝ β γ
where
P = poset-of F
β : (W : ⟨ F ⟩) → is-prop ((U ∧[ F ] W ＝ 𝟎[ F ]) × (U ∨[ F ] W ＝ 𝟏[ F ]))
β W = ×-is-prop carrier-of-[ P ]-is-set carrier-of-[ P ]-is-set
γ : W₁ ＝ W₂
γ = W₁ ＝⟨ (𝟏-right-unit-of-∧ F W₁) ⁻¹ ⟩
W₁ ∧[ F ] 𝟏[ F ] ＝⟨ ap (λ - → meet-of F W₁ -) (q₂ ⁻¹) ⟩
W₁ ∧[ F ] (U ∨[ F ] W₂) ＝⟨ binary-distributivity F W₁ U W₂ ⟩
(W₁ ∧[ F ] U) ∨[ F ] (W₁ ∧[ F ] W₂) ＝⟨ i ⟩
(U ∧[ F ] W₁) ∨[ F ] (W₁ ∧[ F ] W₂) ＝⟨ ii ⟩
𝟎[ F ] ∨[ F ] (W₁ ∧[ F ] W₂) ＝⟨ iii ⟩
(U ∧[ F ] W₂) ∨[ F ] (W₁ ∧[ F ] W₂) ＝⟨ iv ⟩
(W₂ ∧[ F ] U) ∨[ F ] (W₁ ∧[ F ] W₂) ＝⟨ v ⟩
(W₂ ∧[ F ] U) ∨[ F ] (W₂ ∧[ F ] W₁) ＝⟨ vi ⟩
W₂ ∧[ F ] (U ∨[ F ] W₁) ＝⟨ vii ⟩
W₂ ∧[ F ] 𝟏[ F ] ＝⟨ viii ⟩
W₂ ∎
where
i = ap (λ - → - ∨[ F ] (W₁ ∧[ F ] W₂)) (∧[ F ]-is-commutative W₁ U)
ii = ap (λ - → - ∨[ F ] (W₁ ∧[ F ] W₂)) p₁
iii = ap (λ - → - ∨[ F ] (W₁ ∧[ F ] W₂)) (p₂ ⁻¹)
iv = ap (λ - → - ∨[ F ] (W₁ ∧[ F ] W₂)) (∧[ F ]-is-commutative U W₂)
v = ap (λ - → (W₂ ∧[ F ] U) ∨[ F ] -) (∧[ F ]-is-commutative W₁ W₂)
vi = binary-distributivity F W₂ U W₁ ⁻¹
vii = ap (λ - → W₂ ∧[ F ] -) q₁
viii = 𝟏-right-unit-of-∧ F W₂
complements-are-unique : (F : Frame 𝓤 𝓥 𝓦) (U V₁ V₂ : ⟨ F ⟩)
→ is-complement-of F V₁ U
→ is-complement-of F V₂ U
→ V₁ ＝ V₂
complements-are-unique F U V₁ V₂ p q =
pr₁ (from-Σ-＝ (is-clopen₀-is-prop F U φ ψ))
where
φ : is-clopen₀ F U
φ = V₁ , p
ψ : is-clopen₀ F U
ψ = V₂ , q
is-clopen : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → Ω 𝓤
is-clopen F U = is-clopen₀ F U , is-clopen₀-is-prop F U
clopen-implies-well-inside-itself : (F : Frame 𝓤 𝓥 𝓦)
→ (U : ⟨ F ⟩)
→ (is-clopen F U ⇒ U ⋜[ F ] U) holds
clopen-implies-well-inside-itself F U = ∣_∣
well-inside-itself-implies-clopen : (F : Frame 𝓤 𝓥 𝓦)
→ (U : ⟨ F ⟩)
→ (U ⋜[ F ] U ⇒ is-clopen F U) holds
well-inside-itself-implies-clopen F U =
∥∥-rec (holds-is-prop (is-clopen F U)) id
clopenness-equivalent-to-well-inside-itself : (F : Frame 𝓤 𝓥 𝓦)
→ (U : ⟨ F ⟩)
→ (U ⋜[ F ] U) holds
≃ is-clopen F U holds
clopenness-equivalent-to-well-inside-itself F U =
well-inside-itself-implies-clopen F U
, logical-equivs-of-props-are-equivs
(holds-is-prop (U ⋜[ F ] U))
(holds-is-prop (is-clopen F U))
(well-inside-itself-implies-clopen F U)
(clopen-implies-well-inside-itself F U)
\end{code}
\begin{code}
𝟎-is-clopen : (F : Frame 𝓤 𝓥 𝓦) → 𝟎[ F ] ⋜₀[ F ] 𝟎[ F ]
𝟎-is-clopen F = 𝟏[ F ] , β , γ
where
β : 𝟎[ F ] ∧[ F ] 𝟏[ F ] ＝ 𝟎[ F ]
β = 𝟎-left-annihilator-for-∧ F 𝟏[ F ]
γ : 𝟎[ F ] ∨[ F ] 𝟏[ F ] ＝ 𝟏[ F ]
γ = 𝟏-right-annihilator-for-∨ F 𝟎[ F ]
𝟏-is-clopen : (F : Frame 𝓤 𝓥 𝓦) → 𝟏[ F ] ⋜₀[ F ] 𝟏[ F ]
𝟏-is-clopen F = 𝟎[ F ] , β , γ
where
β : 𝟏[ F ] ∧[ F ] 𝟎[ F ] ＝ 𝟎[ F ]
β = 𝟎-right-annihilator-for-∧ F 𝟏[ F ]
γ : 𝟏[ F ] ∨[ F ] 𝟎[ F ] ＝ 𝟏[ F ]
γ = 𝟏-left-annihilator-for-∨ F 𝟎[ F ]
𝟎-is-compact : (F : Frame 𝓤 𝓥 𝓦) → is-compact-open F 𝟎[ F ] holds
𝟎-is-compact F S (∣i∣ , _) p = ∥∥-rec ∃-is-prop † ∣i∣
where
† : index S
→ ∃ i ꞉ index S , (𝟎[ F ] ≤[ poset-of F ] (S [ i ])) holds
† i = ∣ i , 𝟎-is-bottom F (S [ i ]) ∣
\end{code}
\begin{code}
𝟎-is-well-inside-anything : (F : Frame 𝓤 𝓥 𝓦) (U : ⟨ F ⟩)
→ (𝟎[ F ] ⋜[ F ] U) holds
𝟎-is-well-inside-anything F U =
↑↑-is-upwards-closed F ∣ 𝟎-is-clopen F ∣ (𝟎-is-bottom F U)
\end{code}
\begin{code}
well-inside-is-join-stable : (F : Frame 𝓤 𝓥 𝓦) {U₁ U₂ V : ⟨ F ⟩}
→ (U₁ ⋜[ F ] V) holds
→ (U₂ ⋜[ F ] V) holds
→ ((U₁ ∨[ F ] U₂) ⋜[ F ] V) holds
well-inside-is-join-stable F {U₁} {U₂} {V} =
∥∥-rec₂ (holds-is-prop ((U₁ ∨[ F ] U₂) ⋜[ F ] V)) γ
where
open PosetReasoning (poset-of F)
γ : U₁ ⋜₀[ F ] V → U₂ ⋜₀[ F ] V → ((U₁ ∨[ F ] U₂) ⋜[ F ] V) holds
γ (W₁ , c₁ , d₁) (W₂ , c₂ , d₂) = ∣ (W₁ ∧[ F ] W₂) , c , d ∣
where
δ : (W₁ ∧[ F ] W₂) ∧[ F ] U₂ ＝ 𝟎[ F ]
δ = (W₁ ∧[ F ] W₂) ∧[ F ] U₂ ＝⟨ (∧[ F ]-is-associative W₁ W₂ U₂) ⁻¹ ⟩
W₁ ∧[ F ] (W₂ ∧[ F ] U₂) ＝⟨ † ⟩
W₁ ∧[ F ] (U₂ ∧[ F ] W₂) ＝⟨ ap (λ - → meet-of F W₁ -) c₂ ⟩
W₁ ∧[ F ] 𝟎[ F ] ＝⟨ 𝟎-right-annihilator-for-∧ F W₁ ⟩
𝟎[ F ] ∎
where
† = ap (λ - → W₁ ∧[ F ] -) (∧[ F ]-is-commutative W₂ U₂)
ε : ((W₁ ∧[ F ] W₂) ∧[ F ] U₁) ＝ 𝟎[ F ]
ε = (W₁ ∧[ F ] W₂) ∧[ F ] U₁ ＝⟨ † ⟩
(W₂ ∧[ F ] W₁) ∧[ F ] U₁ ＝⟨ (∧[ F ]-is-associative W₂ W₁ U₁) ⁻¹ ⟩
W₂ ∧[ F ] (W₁ ∧[ F ] U₁) ＝⟨ ‡ ⟩
W₂ ∧[ F ] (U₁ ∧[ F ] W₁) ＝⟨ ap (λ - → W₂ ∧[ F ] -) c₁ ⟩
W₂ ∧[ F ] 𝟎[ F ] ＝⟨ 𝟎-right-annihilator-for-∧ F W₂ ⟩
𝟎[ F ] ∎
where
† = ap (λ - → - ∧[ F ] U₁) (∧[ F ]-is-commutative W₁ W₂)
‡ = ap (λ - → W₂ ∧[ F ] -) (∧[ F ]-is-commutative W₁ U₁)
c : ((U₁ ∨[ F ] U₂) ∧[ F ] (W₁ ∧[ F ] W₂)) ＝ 𝟎[ F ]
c = (U₁ ∨[ F ] U₂) ∧[ F ] (W₁ ∧[ F ] W₂) ＝⟨ i ⟩
(W₁ ∧[ F ] W₂) ∧[ F ] (U₁ ∨[ F ] U₂) ＝⟨ ii ⟩
((W₁ ∧[ F ] W₂) ∧[ F ] U₁) ∨[ F ] ((W₁ ∧[ F ] W₂) ∧[ F ] U₂) ＝⟨ iii ⟩
((W₁ ∧[ F ] W₂) ∧[ F ] U₁) ∨[ F ] 𝟎[ F ] ＝⟨ iv ⟩
(W₁ ∧[ F ] W₂) ∧[ F ] U₁ ＝⟨ ε ⟩
𝟎[ F ] ∎
where
i = ∧[ F ]-is-commutative (U₁ ∨[ F ] U₂) (W₁ ∧[ F ] W₂)
ii = binary-distributivity F (W₁ ∧[ F ] W₂) U₁ U₂
iii = ap (λ - → ((W₁ ∧[ F ] W₂) ∧[ F ] U₁) ∨[ F ] -) δ
iv = 𝟎-left-unit-of-∨ F ((W₁ ∧[ F ] W₂) ∧[ F ] U₁)
d : V ∨[ F ] (W₁ ∧[ F ] W₂) ＝ 𝟏[ F ]
d = V ∨[ F ] (W₁ ∧[ F ] W₂) ＝⟨ i ⟩
(V ∨[ F ] W₁) ∧[ F ] (V ∨[ F ] W₂) ＝⟨ ii ⟩
𝟏[ F ] ∧[ F ] (V ∨[ F ] W₂) ＝⟨ iii ⟩
𝟏[ F ] ∧[ F ] 𝟏[ F ] ＝⟨ iv ⟩
𝟏[ F ] ∎
where
i = binary-distributivity-op F V W₁ W₂
ii = ap (λ - → - ∧[ F ] (V ∨[ F ] W₂)) d₁
iii = ap (λ - → 𝟏[ F ] ∧[ F ] -) d₂
iv = 𝟏-right-unit-of-∧ F 𝟏[ F ]
\end{code}
\begin{code}
open FrameHomomorphisms
open FrameHomomorphismProperties
frame-homomorphisms-preserve-complements : (F G : Frame 𝓤 𝓥 𝓦)
→ (h : F ─f→ G)
→ {x x′ : ⟨ F ⟩}
→ is-complement-of F x′ x
→ is-complement-of G (h .pr₁ x) (h .pr₁ x′)
frame-homomorphisms-preserve-complements F G 𝒽@(h , _ , μ) {x} {x′} (φ , ψ) = † , ‡
where
† : (h x′) ∧[ G ] (h x) ＝ 𝟎[ G ]
† = h x′ ∧[ G ] h x ＝⟨ Ⅰ ⟩
h (x′ ∧[ F ] x) ＝⟨ Ⅱ ⟩
h 𝟎[ F ] ＝⟨ Ⅲ ⟩
𝟎[ G ] ∎
where
Ⅰ = frame-homomorphisms-preserve-meets F G 𝒽 x′ x ⁻¹
Ⅱ = ap h (x′ ∧[ F ] x ＝⟨ ∧[ F ]-is-commutative x′ x ⟩
x ∧[ F ] x′ ＝⟨ φ ⟩
𝟎[ F ] ∎)
Ⅲ = frame-homomorphisms-preserve-bottom F G 𝒽
‡ : h x′ ∨[ G ] h x ＝ 𝟏[ G ]
‡ = h x′ ∨[ G ] h x ＝⟨ Ⅰ ⟩
h (x′ ∨[ F ] x) ＝⟨ Ⅱ ⟩
h 𝟏[ F ] ＝⟨ Ⅲ ⟩
𝟏[ G ] ∎
where
Ⅰ = frame-homomorphisms-preserve-binary-joins F G 𝒽 x′ x ⁻¹
Ⅱ = ap h (x′ ∨[ F ] x ＝⟨ ∨[ F ]-is-commutative x′ x ⟩
x ∨[ F ] x′ ＝⟨ ψ ⟩
𝟏[ F ] ∎)
Ⅲ = frame-homomorphisms-preserve-top F G 𝒽
\end{code}
\section{Some properties}
\begin{code}
∨-is-scott-continuous : (F : Frame 𝓤 𝓥 𝓦)
→ (U : ⟨ F ⟩)
→ is-scott-continuous F F (λ - → U ∨[ F ] -) holds
∨-is-scott-continuous F U S dir = β , γ
where
open PosetNotation (poset-of F) using (_≤_)
open PosetReasoning (poset-of F)
open Joins _≤_
β : ((U ∨[ F ] (⋁[ F ] S)) is-an-upper-bound-of ⁅ U ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆) holds
β i = ∨[ F ]-right-monotone (⋁[ F ]-upper S i)
γ : (Ɐ (U′ , _) ꞉ upper-bound ⁅ U ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆ ,
((U ∨[ F ] (⋁[ F ] S)) ≤ U′)) holds
γ (u′ , p) = ∨[ F ]-least γ₁ γ₂
where
δ₁ : index S → (U ≤ u′) holds
δ₁ i = U ≤⟨ ∨[ F ]-upper₁ U (S [ i ]) ⟩
U ∨[ F ] (S [ i ]) ≤⟨ p i ⟩
u′ ■
γ₁ : (U ≤[ poset-of F ] u′) holds
γ₁ = ∥∥-rec (holds-is-prop (U ≤[ poset-of F ] u′)) δ₁ (pr₁ dir)
γ₂ : ((⋁[ F ] S) ≤[ poset-of F ] u′) holds
γ₂ = ⋁[ F ]-least S (u′ , δ₂)
where
δ₂ : (u′ is-an-upper-bound-of S) holds
δ₂ i = S [ i ] ≤⟨ ∨[ F ]-upper₂ U (S [ i ]) ⟩
U ∨[ F ] (S [ i ]) ≤⟨ p i ⟩
u′ ■
∨-is-scott-continuous-eq : (F : Frame 𝓤 𝓥 𝓦)
→ (U : ⟨ F ⟩)
→ (S : Fam 𝓦 ⟨ F ⟩)
→ (is-directed (poset-of F) S) holds
→ U ∨[ F ] (⋁[ F ] S) ＝ ⋁[ F ] ⁅ U ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆
∨-is-scott-continuous-eq F U S dir =
⋁[ F ]-unique ⁅ U ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆ (U ∨[ F ] (⋁[ F ] S)) (γ , δ)
where
γ = pr₁ ((∨-is-scott-continuous F U) S dir)
δ = pr₂ ((∨-is-scott-continuous F U) S dir)
∨-is-scott-continuous-eq′ : (F : Frame 𝓤 𝓥 𝓦)
→ (U : ⟨ F ⟩)
→ (S : Fam 𝓦 ⟨ F ⟩)
→ (is-directed (poset-of F) S) holds
→ (⋁[ F ] S) ∨[ F ] U ＝ ⋁[ F ] ⁅ Sᵢ ∨[ F ] U ∣ Sᵢ ε S ⁆
∨-is-scott-continuous-eq′ F U S δ =
(⋁[ F ] S) ∨[ F ] U ＝⟨ Ⅰ ⟩
U ∨[ F ] (⋁[ F ] S) ＝⟨ Ⅱ ⟩
⋁[ F ] ⁅ U ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆ ＝⟨ Ⅲ ⟩
⋁[ F ] ⁅ Sᵢ ∨[ F ] U ∣ Sᵢ ε S ⁆ ∎
where
open PosetReasoning (poset-of F)
† : cofinal-in F ⁅ U ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆ ⁅ Sᵢ ∨[ F ] U ∣ Sᵢ ε S ⁆ holds
† i = ∣ i , (U ∨[ F ] (S [ i ]) ＝⟨ ∨[ F ]-is-commutative U (S [ i ]) ⟩ₚ
S [ i ] ∨[ F ] U ■) ∣
‡ : cofinal-in F ⁅ Sᵢ ∨[ F ] U ∣ Sᵢ ε S ⁆ ⁅ U ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆ holds
‡ i = ∣ i , (S [ i ] ∨[ F ] U ＝⟨ ∨[ F ]-is-commutative (S [ i ]) U ⟩ₚ
U ∨[ F ] (S [ i ]) ■) ∣
Ⅰ = ∨[ F ]-is-commutative (⋁[ F ] S) U
Ⅱ = ∨-is-scott-continuous-eq F U S δ
Ⅲ = bicofinal-implies-same-join F _ _ † ‡
∨-is-scott-continuous′ : (F : Frame 𝓤 𝓥 𝓦)
→ (U : ⟨ F ⟩)
→ is-scott-continuous F F (λ - → - ∨[ F ] U) holds
∨-is-scott-continuous′ F U S δ =
transport (λ - → (- is-lub-of ⁅ Sᵢ ∨[ F ] U ∣ Sᵢ ε S ⁆) holds) († ⁻¹) ‡
where
open Joins (λ x y → x ≤[ poset-of F ] y)
† : (⋁[ F ] S) ∨[ F ] U ＝ ⋁[ F ] ⁅ Sᵢ ∨[ F ] U ∣ Sᵢ ε S ⁆
† = ∨-is-scott-continuous-eq′ F U S δ
‡ = ⋁[ F ]-upper ⁅ Sᵢ ∨[ F ] U ∣ Sᵢ ε S ⁆
, ⋁[ F ]-least ⁅ Sᵢ ∨[ F ] U ∣ Sᵢ ε S ⁆
⋜₀-implies-≪-in-compact-frames : (F : Frame 𝓤 𝓥 𝓦)
→ is-compact F holds
→ (U V : ⟨ F ⟩)
→ U ⋜₀[ F ] V
→ (U ≪[ F ] V) holds
⋜₀-implies-≪-in-compact-frames {𝓦 = 𝓦} F κ U V (W , c₁ , c₂) S d q =
∥∥-rec ∃-is-prop θ ζ
where
open PosetNotation (poset-of F)
open PosetReasoning (poset-of F)
T : Fam 𝓦 ⟨ F ⟩
T = ⁅ W ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆
δ : (𝟏[ F ] ≤ (⋁[ F ] T)) holds
δ = 𝟏[ F ] ＝⟨ c₂ ⁻¹ ⟩ₚ
V ∨[ F ] W ≤⟨ ∨[ F ]-left-monotone q ⟩
(⋁[ F ] S) ∨[ F ] W ＝⟨ ∨[ F ]-is-commutative (⋁[ F ] S) W ⟩ₚ
W ∨[ F ] (⋁[ F ] S) ＝⟨ ∨-is-scott-continuous-eq F W S d ⟩ₚ
⋁[ F ] ⁅ W ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆ ■
ε : ((W ∨[ F ] (⋁[ F ] S)) ≤ (⋁[ F ] T)) holds
ε = W ∨[ F ] (⋁[ F ] S) ≤⟨ 𝟏-is-top F (W ∨[ F ] (⋁[ F ] S)) ⟩
𝟏[ F ] ≤⟨ δ ⟩
⋁[ F ] ⁅ W ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆ ■
\end{code}
The family `T` we defined is also directed by the directedness of `S`.
\begin{code}
up : (Ɐ i , Ɐ j ,
Ǝ k , (T [ i ] ≤ T [ k ]) holds × (T [ j ] ≤ T [ k ]) holds) holds
up i j = ∥∥-rec ∃-is-prop r (pr₂ d i j)
where
r = λ (k , p , q) → ∣ k , ∨[ F ]-right-monotone p , ∨[ F ]-right-monotone q ∣
\end{code}
\begin{code}
T-is-directed : (is-directed (poset-of F) ⁅ W ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆) holds
T-is-directed = pr₁ d , up
ζ : ∥ Σ i ꞉ index S , (𝟏[ F ] ≤ (W ∨[ F ] (S [ i ]))) holds ∥
ζ = κ ⁅ W ∨[ F ] Sᵢ ∣ Sᵢ ε S ⁆ T-is-directed δ
θ : Σ i ꞉ index S , (𝟏[ F ] ≤ (W ∨[ F ] S [ i ])) holds
→ ∃ i ꞉ index S , (U ≤ S [ i ]) holds
θ (i , p) = ∣ i , well-inside-implies-below F U (S [ i ]) ∣ W , c₁ , ι ∣ ∣
where
η = 𝟏[ F ] ≤⟨ p ⟩
W ∨[ F ] (S [ i ]) ＝⟨ ∨[ F ]-is-commutative W (S [ i ]) ⟩ₚ
(S [ i ]) ∨[ F ] W ■
ι = only-𝟏-is-above-𝟏 F ((S [ i ]) ∨[ F ] W) η
⋜-implies-≪-in-compact-frames : (F : Frame 𝓤 𝓥 𝓦)
→ is-compact F holds
→ (U V : ⟨ F ⟩) → (U ⋜[ F ] V ⇒ U ≪[ F ] V) holds
⋜-implies-≪-in-compact-frames F κ U V =
∥∥-rec (holds-is-prop (U ≪[ F ] V)) (⋜₀-implies-≪-in-compact-frames F κ U V)
clopens-are-compact-in-compact-frames : (F : Frame 𝓤 𝓥 𝓦)
→ is-compact F holds
→ (U : ⟨ F ⟩)
→ is-clopen F U holds
→ is-compact-open F U holds
clopens-are-compact-in-compact-frames F κ U =
⋜₀-implies-≪-in-compact-frames F κ U U
\end{code}
\section{Regularity}
We would like to be able to express regularity using `↓↓` defined as:
\begin{code}
↓↓[_] : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → Fam 𝓤 ⟨ F ⟩
↓↓[ F ] U = (Σ V ꞉ ⟨ F ⟩ , (V ⋜[ F ] U) holds) , pr₁
\end{code}
but there are size problems with this. Therefore, we define regularity as
follows:
\begin{code}
is-regular₀ : (F : Frame 𝓤 𝓥 𝓦) → (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺) ̇
is-regular₀ {𝓤 = 𝓤} {𝓥} {𝓦} F =
let
open Joins (λ U V → U ≤[ poset-of F ] V)
P : Fam 𝓦 ⟨ F ⟩ → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺ ̇
P ℬ = Π U ꞉ ⟨ F ⟩ ,
Σ J ꞉ Fam 𝓦 (index ℬ) ,
(U is-lub-of ⁅ ℬ [ j ] ∣ j ε J ⁆) holds
× (Π i ꞉ index J , (ℬ [ J [ i ] ] ⋜[ F ] U) holds)
in
Σ ℬ ꞉ Fam 𝓦 ⟨ F ⟩ , P ℬ
\end{code}
\begin{code}
is-regular : (F : Frame 𝓤 𝓥 𝓦) → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
is-regular {𝓤 = 𝓤} {𝓥} {𝓦} F = ∥ is-regular₀ F ∥Ω
\end{code}
Even though this definition is a bit more convenient to work with, it simply
asserts the existence of a regular basis i.e. a basis in which every open in a
basic covering family for some open `U` is well inside `U`.
\begin{code}
is-regular-basis : (F : Frame 𝓤 𝓥 𝓦)
→ (ℬ : Fam 𝓦 ⟨ F ⟩) → (β : is-basis-for F ℬ) → Ω (𝓤 ⊔ 𝓦)
is-regular-basis F ℬ β =
Ɐ U ꞉ ⟨ F ⟩ , let 𝒥 = pr₁ (β U) in Ɐ j ꞉ (index 𝒥) , ℬ [ 𝒥 [ j ] ] ⋜[ F ] U
\end{code}
A projection for easily referring to the basis of a regular frame:
\begin{code}
basisᵣ : (F : Frame 𝓤 𝓥 𝓦)
→ (is-regular F ⇒ has-basis F) holds
basisᵣ F r = ∥∥-rec (holds-is-prop (has-basis F)) γ r
where
γ : is-regular₀ F → has-basis F holds
γ (ℬ , δ)= ∣ ℬ , (λ U → pr₁ (δ U) , pr₁ (pr₂ (δ U))) ∣
\end{code}
When we directify the basis of a regular frame, the directified basis is also
regular:
\begin{code}
directification-preserves-regularity : (F : Frame 𝓤 𝓥 𝓦)
→ (ℬ : Fam 𝓦 ⟨ F ⟩)
→ (β : is-basis-for F ℬ)
→ is-regular-basis F ℬ β holds
→ let
ℬ↑ = directify F ℬ
β↑ = directified-basis-is-basis F ℬ β
in
is-regular-basis F ℬ↑ β↑ holds
directification-preserves-regularity F ℬ β r U = γ
where
ℬ↑ = directify F ℬ
β↑ = directified-basis-is-basis F ℬ β
𝒥 = pr₁ (β U)
𝒥↑ = pr₁ (β↑ U)
γ : (Ɐ js ꞉ index 𝒥↑ , ℬ↑ [ 𝒥↑ [ js ] ] ⋜[ F ] U) holds
γ [] = 𝟎-is-well-inside-anything F U
γ (j ∷ js) = well-inside-is-join-stable F (r U j) (γ js)
\end{code}
This gives us that covering families in a regular frame are directed from
which the result we are interested in follows:
\begin{code}
≪-implies-⋜-in-regular-frames : (F : Frame 𝓤 𝓥 𝓦)
→ (is-regular F) holds
→ (U V : ⟨ F ⟩)
→ (U ≪[ F ] V ⇒ U ⋜[ F ] V) holds
≪-implies-⋜-in-regular-frames {𝓦 = 𝓦} F r U V =
∥∥-rec (holds-is-prop (U ≪[ F ] V ⇒ U ⋜[ F ] V)) γ r
where
γ : is-regular₀ F → (U ≪[ F ] V ⇒ U ⋜[ F ] V) holds
γ (ℬ , δ) κ = ∥∥-rec (holds-is-prop (U ⋜[ F ] V)) ζ (κ S ε c)
where
ℬ↑ : Fam 𝓦 ⟨ F ⟩
ℬ↑ = directify F ℬ
β : is-basis-for F ℬ
β U = pr₁ (δ U) , pr₁ (pr₂ (δ U))
β↑ : is-basis-for F ℬ↑
β↑ = directified-basis-is-basis F ℬ β
ρ : is-regular-basis F ℬ β holds
ρ U = pr₂ (pr₂ (δ U))
ρ↑ : is-regular-basis F ℬ↑ β↑ holds
ρ↑ = directification-preserves-regularity F ℬ β ρ
𝒥 : Fam 𝓦 (index ℬ↑)
𝒥 = pr₁ (β↑ V)
S : Fam 𝓦 ⟨ F ⟩
S = ⁅ ℬ↑ [ i ] ∣ i ε 𝒥 ⁆
ε : is-directed (poset-of F) S holds
ε = covers-of-directified-basis-are-directed F ℬ β V
c : (V ≤[ poset-of F ] (⋁[ F ] S)) holds
c = reflexivity+ (poset-of F) (⋁[ F ]-unique S V (pr₂ (β↑ V)))
ζ : Σ k ꞉ index S , (U ≤[ poset-of F ] (S [ k ])) holds → (U ⋜[ F ] V) holds
ζ (k , q) = ↓↓-is-downwards-closed F (ρ↑ V k) q
\end{code}
\begin{code}
compacts-are-clopen-in-regular-frames : (F : Frame 𝓤 𝓥 𝓦)
→ is-regular F holds
→ (Ɐ U ꞉ ⟨ F ⟩ ,
is-compact-open F U ⇒ is-clopen F U) holds
compacts-are-clopen-in-regular-frames F r U =
well-inside-itself-implies-clopen F U ∘ ≪-implies-⋜-in-regular-frames F r U U
\end{code}
\section{Zero-dimensionality}
A locale L is said to be zero-dimensional iff it has a basis consisting of
clopen elements.
\begin{code}
consists-of-clopens : (F : Frame 𝓤 𝓥 𝓦) → (S : Fam 𝓦 ⟨ F ⟩) → Ω (𝓤 ⊔ 𝓦)
consists-of-clopens F S = Ɐ i ꞉ index S , is-clopen F (S [ i ])
zero-dimensionalᴰ : Frame 𝓤 𝓥 𝓦 → (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺) ̇
zero-dimensionalᴰ {𝓦 = 𝓦} F =
Σ ℬ ꞉ Fam 𝓦 ⟨ F ⟩ , is-directed-basis F ℬ
× consists-of-clopens F ℬ holds
basis-of-zero-dimensionalᴰ-frame : (L : Frame 𝓤 𝓥 𝓦)
→ zero-dimensionalᴰ L
→ Σ ℬ ꞉ Fam 𝓦 ⟨ L ⟩ , is-basis-for L ℬ
basis-of-zero-dimensionalᴰ-frame L (ℬ , (β , _) , _) = ℬ , β
is-zero-dimensional : Frame 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
is-zero-dimensional {𝓦 = 𝓦} F = ∥ zero-dimensionalᴰ F ∥Ω
basis-of-zero-dimensional-frame : (F : Frame 𝓤 𝓥 𝓦)
→ (is-zero-dimensional F ⇒ has-basis F) holds
basis-of-zero-dimensional-frame F =
∥∥-rec (holds-is-prop (has-basis F)) λ { (ℬ , (δ , _) , _) → ∣ ℬ , δ ∣}
\end{code}
\begin{code}
clopens-are-closed-under-∨ : (F : Frame 𝓤 𝓥 𝓦) (x y : ⟨ F ⟩)
→ (is-clopen F x
⇒ is-clopen F y
⇒ is-clopen F (x ∨[ F ] y)) holds
clopens-are-closed-under-∨ F x y (x′ , ϡ₁ , ϟ₁) (y′ , ϡ₂ , ϟ₂) =
(x′ ∧[ F ] y′) , † , ‡
where
open PosetReasoning (poset-of F)
†₁ : (((x ∨[ F ] y) ∧[ F ] (x′ ∧[ F ] y′)) ≤[ poset-of F ] 𝟎[ F ]) holds
†₁ =
(x ∨[ F ] y) ∧[ F ] (x′ ∧[ F ] y′) ＝⟨ Ⅰ ⟩ₚ
(x ∧[ F ] (x′ ∧[ F ] y′)) ∨[ F ] (y ∧[ F ] (x′ ∧[ F ] y′)) ≤⟨ Ⅱ ⟩
(x ∧[ F ] x′) ∨[ F ] (y ∧[ F ] (x′ ∧[ F ] y′)) ≤⟨ Ⅲ ⟩
(x ∧[ F ] x′) ∨[ F ] (y ∧[ F ] y′) ≤⟨ Ⅳ ⟩
𝟎[ F ] ∨[ F ] (y ∧[ F ] y′) ≤⟨ Ⅴ ⟩
𝟎[ F ] ∨[ F ] 𝟎[ F ] ＝⟨ Ⅵ ⟩ₚ
𝟎[ F ] ■
where
Ⅰ = binary-distributivity-right F
Ⅱ = ∨[ F ]-left-monotone (∧[ F ]-right-monotone (∧[ F ]-lower₁ x′ y′))
Ⅲ = ∨[ F ]-right-monotone (∧[ F ]-right-monotone (∧[ F ]-lower₂ x′ y′))
Ⅳ = ∨[ F ]-left-monotone (reflexivity+ (poset-of F) ϡ₁)
Ⅴ = ∨[ F ]-right-monotone (reflexivity+ (poset-of F) ϡ₂)
Ⅵ = ∨[ F ]-is-idempotent 𝟎[ F ] ⁻¹
† : (x ∨[ F ] y) ∧[ F ] (x′ ∧[ F ] y′) ＝ 𝟎[ F ]
† = only-𝟎-is-below-𝟎 F _ †₁
‡₁ : (𝟏[ F ] ≤[ poset-of F ] ((x ∨[ F ] y) ∨[ F ] (x′ ∧[ F ] y′))) holds
‡₁ =
𝟏[ F ] ＝⟨ Ⅰ ⟩ₚ
𝟏[ F ] ∧[ F ] 𝟏[ F ] ≤⟨ Ⅱ ⟩
(x ∨[ F ] x′) ∧[ F ] 𝟏[ F ] ≤⟨ Ⅲ ⟩
(x ∨[ F ] x′) ∧[ F ] (y ∨[ F ] y′) ≤⟨ Ⅳ ⟩
((x ∨[ F ] y ) ∨[ F ] x′)∧[ F ] (y ∨[ F ] y′) ≤⟨ Ⅴ ⟩
((x ∨[ F ] y ) ∨[ F ] x′) ∧[ F ] ((x ∨[ F ] y ) ∨[ F ] y′) ＝⟨ Ⅵ ⟩ₚ
(x ∨[ F ] y) ∨[ F ] (x′ ∧[ F ] y′) ■
where
Ⅰ = ∧[ F ]-is-idempotent 𝟏[ F ]
Ⅱ = ∧[ F ]-left-monotone (reflexivity+ (poset-of F) (ϟ₁ ⁻¹))
Ⅲ = ∧[ F ]-right-monotone (reflexivity+ (poset-of F) (ϟ₂ ⁻¹))
Ⅳ = ∧[ F ]-left-monotone (∨[ F ]-left-monotone (∨[ F ]-upper₁ x y))
Ⅴ = ∧[ F ]-right-monotone (∨[ F ]-left-monotone (∨[ F ]-upper₂ x y))
Ⅵ = binary-distributivity-op F (x ∨[ F ] y) x′ y′ ⁻¹
‡ : (x ∨[ F ] y) ∨[ F ] (x′ ∧[ F ] y′) ＝ 𝟏[ F ]
‡ = only-𝟏-is-above-𝟏 F _ ‡₁
clopens-are-closed-under-∧ : (F : Frame 𝓤 𝓥 𝓦) (x y : ⟨ F ⟩)
→ (is-clopen F x
⇒ is-clopen F y
⇒ is-clopen F (x ∧[ F ] y)) holds
clopens-are-closed-under-∧ F x y ϟ₁@(x′ , φ₁ , φ₂) ϟ₂@(y′ , ψ₁ , ψ₂) = (x′ ∨[ F ] y′) , †
where
ϡ₁ : is-boolean-complement-of F x x′ holds
ϡ₁ = (x′ ∧[ F ] x ＝⟨ ∧[ F ]-is-commutative x′ x ⟩ x ∧[ F ] x′ ＝⟨ φ₁ ⟩ 𝟎[ F ] ∎)
, (x′ ∨[ F ] x ＝⟨ ∨[ F ]-is-commutative x′ x ⟩ x ∨[ F ] x′ ＝⟨ φ₂ ⟩ 𝟏[ F ] ∎)
ϡ₂ : is-boolean-complement-of F y y′ holds
ϡ₂ = (y′ ∧[ F ] y ＝⟨ ∧[ F ]-is-commutative y′ y ⟩ y ∧[ F ] y′ ＝⟨ ψ₁ ⟩ 𝟎[ F ] ∎)
, (y′ ∨[ F ] y ＝⟨ ∨[ F ]-is-commutative y′ y ⟩ y ∨[ F ] y′ ＝⟨ ψ₂ ⟩ 𝟏[ F ] ∎)
† : is-boolean-complement-of F (x′ ∨[ F ] y′) (x ∧[ F ] y) holds
† = ∧-complement F ϡ₁ ϡ₂
directification-preserves-clopenness : (F : Frame 𝓤 𝓥 𝓦)
→ (ℬ : Fam 𝓦 ⟨ F ⟩)
→ (consists-of-clopens F ℬ
⇒ consists-of-clopens F (directify F ℬ))
holds
directification-preserves-clopenness F ℬ ξ [] = 𝟎-is-clopen F
directification-preserves-clopenness F ℬ ξ (i ∷ is) =
clopens-are-closed-under-∨ F (ℬ [ i ]) (directify F ℬ [ is ]) (ξ i) ℐℋ
where
abstract
ℐℋ : is-clopen F (directify F ℬ [ is ]) holds
ℐℋ = directification-preserves-clopenness F ℬ ξ is
\end{code}
Every zero-dimensional locale is regular.
\begin{code}
zero-dimensional-locales-are-regular : (F : Frame 𝓤 𝓥 𝓦)
→ is-zero-dimensional F holds
→ is-regular F holds
zero-dimensional-locales-are-regular {𝓦 = 𝓦} F =
∥∥-rec (holds-is-prop (is-regular F)) γ
where
open Joins (λ x y → x ≤[ poset-of F ] y)
γ : zero-dimensionalᴰ F → is-regular F holds
γ (ℬ , β , ξ) = ∣ ℬ , δ ∣
where
δ : Π U ꞉ ⟨ F ⟩ ,
Σ J ꞉ Fam 𝓦 (index ℬ) ,
(U is-lub-of (fmap-syntax (_[_] ℬ) J)) holds
× (Π i ꞉ index J , (ℬ [ J [ i ] ] ⋜[ F ] U) holds)
δ U = 𝒥 , c , ε
where
𝒥 = pr₁ (pr₁ β U)
c : (U is-lub-of ⁅ ℬ [ j ] ∣ j ε 𝒥 ⁆) holds
c = pr₂ (pr₁ β U)
ε : Π i ꞉ index 𝒥 , (ℬ [ 𝒥 [ i ] ] ⋜[ F ] U) holds
ε i = ↑↑-is-upwards-closed F ∣ ξ (𝒥 [ i ]) ∣ (pr₁ c i)
where
η : ((ℬ [ 𝒥 [ i ] ]) ≤[ poset-of F ] (ℬ [ 𝒥 [ i ] ])) holds
η = ≤-is-reflexive (poset-of F) (ℬ [ 𝒥 [ i ] ])
compacts-are-clopen-in-zero-dimensional-locales : (F : Frame 𝓤 𝓥 𝓦)
→ is-zero-dimensional F holds
→ (C : ⟨ F ⟩)
→ is-compact-open F C holds
→ is-clopen F C holds
compacts-are-clopen-in-zero-dimensional-locales F =
compacts-are-clopen-in-regular-frames F ∘ zero-dimensional-locales-are-regular F
\end{code}
\section{Stone Locales}
A frame F is called Stone iff it is compact and zero-dimensional.
\begin{code}
is-stone : (F : Frame 𝓤 𝓥 𝓦) → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
is-stone F = is-compact F ∧ is-zero-dimensional F
\end{code}
In a Stone locale, an open is a clopen iff it is compact.
\begin{code}
clopen-iff-compact-in-stone-frame : (F : Frame 𝓤 𝓥 𝓦)
→ is-stone F holds
→ (U : ⟨ F ⟩)
→ (is-clopen F U holds)
↔ (is-compact-open F U holds)
clopen-iff-compact-in-stone-frame F (κ , ζ) U = β , γ
where
β : (is-clopen F U ⇒ is-compact-open F U) holds
β = clopens-are-compact-in-compact-frames F κ U
ρ : is-regular F holds
ρ = zero-dimensional-locales-are-regular F ζ
γ : (is-compact-open F U ⇒ is-clopen F U) holds
γ = compacts-are-clopen-in-regular-frames F ρ U
\end{code}
\section{Spectrality}
\begin{code}
contains-top : (F : Frame 𝓤 𝓥 𝓦) → Fam 𝓦 ⟨ F ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦)
contains-top F U = Ǝ t ꞉ index U , is-top F (U [ t ]) holds
closed-under-binary-meets : (F : Frame 𝓤 𝓥 𝓦) → Fam 𝓦 ⟨ F ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦)
closed-under-binary-meets F 𝒮 =
Ɐ i ꞉ index 𝒮 , Ɐ j ꞉ index 𝒮 ,
Ǝ k ꞉ index 𝒮 , ((𝒮 [ k ]) is-glb-of (𝒮 [ i ] , 𝒮 [ j ])) holds
where
open Meets (λ x y → x ≤[ poset-of F ] y)
closed-under-finite-meets : (F : Frame 𝓤 𝓥 𝓦) → Fam 𝓦 ⟨ F ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦)
closed-under-finite-meets F S = contains-top F S ∧ closed-under-binary-meets F S
consists-of-compact-opens : (F : Frame 𝓤 𝓥 𝓦) → Fam 𝓦 ⟨ F ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
consists-of-compact-opens F U = Ɐ i ꞉ index U , is-compact-open F (U [ i ])
\end{code}
We now define the notion of spectrality. Note that closure under finite joins is
not an essential part of the definition. However, it can be assumed *without
loss of generality* and we assume it in the definition for the sake of
convenience.
\begin{code}
spectralᴰ : Frame 𝓤 𝓥 𝓦 → (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺) ̇
spectralᴰ {𝓤 = 𝓤} {𝓥} {𝓦} F =
Σ ℬ ꞉ Fam 𝓦 ⟨ F ⟩ , is-directed-basis F ℬ
× consists-of-compact-opens F ℬ holds
× closed-under-finite-meets F ℬ holds
basisₛ : (F : Frame 𝓤 𝓥 𝓦) → spectralᴰ F → Fam 𝓦 ⟨ F ⟩
basisₛ F (ℬ , _) = ℬ
is-spectral : Frame 𝓤 𝓥 𝓦 → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
is-spectral F = ∥ spectralᴰ F ∥Ω
spectral-frames-have-bases : (F : Frame 𝓤 𝓥 𝓦)
→ (is-spectral F ⇒ has-basis F) holds
spectral-frames-have-bases F σ = ∥∥-rec ∥∥-is-prop γ σ
where
γ : spectralᴰ F → ∥ Σ ℬ ꞉ Fam _ ⟨ F ⟩ , is-basis-for F ℬ ∥
γ (ℬ , p) = ∣ ℬ , pr₁ (pr₁ p) ∣
finite-meet : (F : Frame 𝓤 𝓥 𝓦) → (ℬ : Fam 𝓦 ⟨ F ⟩) → List (index ℬ) → ⟨ F ⟩
finite-meet F ℬ [] = 𝟏[ F ]
finite-meet F ℬ (i ∷ is) = ℬ [ i ] ∧[ F ] finite-meet F ℬ is
coherence-list : (F : Frame 𝓤 𝓥 𝓦)
→ (ℬ : Fam 𝓦 ⟨ F ⟩)
→ closed-under-finite-meets F ℬ holds
→ (is : List (index ℬ))
→ ∥ Σ k ꞉ index ℬ , ℬ [ k ] ＝ finite-meet F ℬ is ∥
coherence-list F ℬ (φ , ψ) [] = ∥∥-rec ∥∥-is-prop † φ
where
† : Σ t ꞉ index ℬ , is-top F (ℬ [ t ]) holds
→ ∥ Σ k ꞉ index ℬ , ℬ [ k ] ＝ finite-meet F ℬ [] ∥
† (t , τ) = ∣ t , 𝟏-is-unique F (ℬ [ t ]) τ ∣
coherence-list F ℬ (φ , ψ) (i ∷ is) = ∥∥-rec ∥∥-is-prop † ih
where
open PosetReasoning (poset-of F)
open Meets (λ x y → x ≤[ poset-of F ] y)
ih : ∥ Σ k ꞉ index ℬ , ℬ [ k ] ＝ finite-meet F ℬ is ∥
ih = coherence-list F ℬ (φ , ψ) is
† : Σ k ꞉ index ℬ , ℬ [ k ] ＝ finite-meet F ℬ is
→ ∥ Σ k ꞉ index ℬ , ℬ [ k ] ＝ finite-meet F ℬ (i ∷ is) ∥
† (k , p) = ∥∥-rec ∥∥-is-prop ※ (ψ i k)
where
※ : _
※ (j , ξ , r) = ∣ j , ∧[ F ]-unique (β , γ) ∣
where
β : ((ℬ [ j ]) is-a-lower-bound-of (ℬ [ i ] , finite-meet F ℬ is)) holds
β = transport (λ - → ((ℬ [ j ]) is-a-lower-bound-of (ℬ [ i ] , -)) holds) p ξ
γ : (Ɐ (l , _) ꞉ lower-bound (ℬ [ i ] , finite-meet F ℬ is) ,
l ≤[ poset-of F ] (ℬ [ j ])) holds
γ (l , ζ) = l ≤⟨ Ⅰ ⟩
ℬ [ i ] ∧[ F ] finite-meet F ℬ is ＝⟨ Ⅱ ⟩ₚ
ℬ [ i ] ∧[ F ] ℬ [ k ] ＝⟨ Ⅲ ⟩ₚ
ℬ [ j ] ■
where
Ⅰ = uncurry (∧[ F ]-greatest (ℬ [ i ]) (finite-meet F ℬ is) l) ζ
Ⅱ = ap (λ - → meet-of F (ℬ [ i ]) -) (p ⁻¹)
Ⅲ = (∧[ F ]-unique (ξ , r)) ⁻¹
\end{code}
\section{Spectral maps}
\begin{code}
is-spectral-map : (F : Frame 𝓤 𝓥 𝓥) (G : Frame 𝓤' 𝓥 𝓥)
→ (F ─f→ G) → Ω (𝓤 ⊔ 𝓤' ⊔ 𝓥 ⁺)
is-spectral-map F G (f , _) =
Ɐ x ꞉ ⟨ F ⟩ , is-compact-open F x ⇒ is-compact-open G (f x)
\end{code}
-- directification-preserves-coherence : (F : Frame 𝓤 𝓥 𝓦)
-- → (ℬ : Fam 𝓦 ⟨ F ⟩)
-- → (σ : closed-under-finite-meets F ℬ holds)
-- → closed-under-finite-meets F (directify F ℬ) holds
-- directification-preserves-coherence F ℬ c@(τ , σ) = β , γ
-- where
-- open PosetReasoning (poset-of F)
-- open Meets (λ x y → x ≤[ poset-of F ] y) hiding (is-top)
-- β : contains-top F (directify F ℬ) holds
-- β = ∥∥-rec (holds-is-prop (contains-top F (directify F ℬ))) † τ
-- where
-- † : Σ t ꞉ index ℬ , is-top F (ℬ [ t ]) holds
-- → contains-top F (directify F ℬ) holds
-- † (t , p) = ∣ (t ∷ []) , transport (λ - → is-top F - holds) (‡ ⁻¹) p ∣
-- where
-- ‡ : directify F ℬ [ t ∷ [] ] ＝ ℬ [ t ]
-- ‡ = ℬ [ t ] ∨[ F ] 𝟎[ F ] ＝⟨ 𝟎-left-unit-of-∨ F (ℬ [ t ]) ⟩
-- ℬ [ t ] ∎
-- γ : closed-under-binary-meets F (directify F ℬ) holds
-- γ is js = ∥∥-rec₂ ∥∥-is-prop δ (coherence-list F ℬ c is) (coherence-list F ℬ c is)
-- where
-- δ : (Σ m ꞉ index ℬ , ℬ [ m ] ＝ finite-meet F ℬ is)
-- → (Σ n ꞉ index ℬ , ℬ [ n ] ＝ finite-meet F ℬ is)
-- → ∥ Σ ks ꞉ index (directify F ℬ) ,
-- ((directify F ℬ [ ks ]) is-glb-of (directify F ℬ [ is ] , directify F ℬ [ js ])) holds ∥
-- δ (m , μ) (n , ν) = ∥∥-rec ∥∥-is-prop ϵ (σ m n )
-- where
-- ϵ : Sigma (index ℬ) (λ k → ((ℬ [ k ]) is-glb-of (ℬ [ m ] , ℬ [ n ])) holds)
-- → ∥ Sigma
-- (index (directify F ℬ))
-- (λ ks → ((directify F ℬ [ ks ]) is-glb-of (directify F ℬ [ is ] , directify F ℬ [ js ])) holds) ∥
-- ϵ (k , ξ) = ∣ (k ∷ []) , (ζ₁ , ζ₂) , θ ∣
-- where
-- ζ₁ : ((directify F ℬ [ k ∷ [] ]) ≤[ poset-of F ] (directify F ℬ [ is ])) holds
-- ζ₁ = ℬ [ k ] ∨[ F ] 𝟎[ F ] ≤⟨ {!!} ⟩
-- ℬ [ k ] ≤⟨ {!!} ⟩
-- ℬ [ m ] ∧[ F ] ℬ [ n ] ≤⟨ {!!} ⟩
-- (finite-meet F ℬ is) ∧[ F ] (finite-meet F ℬ js) ≤⟨ {!!} ⟩
-- finite-meet F ℬ is ≤⟨ {!!} ⟩
-- directify F ℬ [ is ] ■
-- ζ₂ : {!!}
-- ζ₂ = {!!}
-- θ : {!!}
-- θ = {!!}
\end{code}
\begin{code}
compact-rel-syntax : (F : Frame 𝓤 𝓥 𝓦) → ⟨ F ⟩ → ⟨ F ⟩ → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺)
compact-rel-syntax F U V =
Ɐ W ꞉ ⟨ F ⟩ , is-compact-open F W ⇒ W ≤[ poset-of F ] U ⇒ W ≤[ poset-of F ] V
syntax compact-rel-syntax F U V = U ≤ₖ[ F ] V
spectral-yoneda : (F : Frame 𝓤 𝓥 𝓦)
→ is-spectral F holds
→ (U V : ⟨ F ⟩)
→ (U ≤ₖ[ F ] V ⇒ U ≤[ poset-of F ] V) holds
spectral-yoneda {𝓦 = 𝓦} F σ U V χ =
∥∥-rec (holds-is-prop (U ≤[ poset-of F ] V)) γ σ
where
open PosetReasoning (poset-of F)
open Joins (λ x y → x ≤[ poset-of F ] y)
open JoinNotation (λ - → ⋁[ F ] -)
γ : spectralᴰ F → (U ≤[ poset-of F ] V) holds
γ (ℬ , υ , φ , ψ) =
U ＝⟨ I ⟩ₚ
⋁[ F ] ⁅ ℬ [ i ] ∣ i ε ℐ ⁆ ≤⟨ ii ⟩
V ■
where
ℐ : Fam 𝓦 (index ℬ)
ℐ = covering-index-family F ℬ (pr₁ υ) U
I : U ＝ ⋁[ F ] ⁅ ℬ [ i ] ∣ i ε ℐ ⁆
I = ⋁[ F ]-unique ⁅ ℬ [ i ] ∣ i ε ℐ ⁆ U (pr₂ (pr₁ υ U))
ϑ : (i : index ℐ) → ((ℬ [ ℐ [ i ] ]) ≤[ poset-of F ] U) holds
ϑ i = ℬ [ ℐ [ i ] ] ≤⟨ ⋁[ F ]-upper ⁅ ℬ [ i ] ∣ i ε ℐ ⁆ i ⟩
⋁[ F ] ⁅ ℬ [ i ] ∣ i ε ℐ ⁆ ＝⟨ I ⁻¹ ⟩ₚ
U ■
ξ : (V is-an-upper-bound-of ⁅ ℬ [ i ] ∣ i ε ℐ ⁆) holds
ξ i = χ (ℬ [ ℐ [ i ] ]) (φ (ℐ [ i ])) (ϑ i)
ii : ((⋁[ F ] ⁅ ℬ [ i ] ∣ i ε ℐ ⁆) ≤[ poset-of F ] V) holds
ii = ⋁[ F ]-least ⁅ ℬ [ i ] ∣ i ε ℐ ⁆ (V , ξ)
\end{code}
\begin{code}
open Locale
module PerfectMaps (X : Locale 𝓤 𝓥 𝓥) (Y : Locale 𝓤' 𝓥 𝓥)
(𝒷 : has-basis (𝒪 Y) holds) where
open AdjointFunctorTheorem pt fe X Y 𝒷
open ContinuousMapNotation X Y
\end{code}
A continuous map `f : X → Y` is called *perfect* if its right adjoint is
Scott-continuous.
\begin{code}
open ContinuousMaps
is-perfect-map : (X ─c→ Y) → Ω (𝓤 ⊔ 𝓤' ⊔ 𝓥 ⁺)
is-perfect-map f = is-scott-continuous (𝒪 X) (𝒪 Y) (pr₁ (right-adjoint-of f))
\end{code}
\begin{code}
perfect-preserves-way-below : (𝒻 : X ─c→ Y)
→ is-perfect-map 𝒻 holds
→ (U V : ⟨ 𝒪 Y ⟩)
→ (U ≪[ 𝒪 Y ] V) holds
→ (𝒻 ⋆∙ U ≪[ 𝒪 X ] 𝒻 ⋆∙ V) holds
perfect-preserves-way-below f φ U V ϑ S δ p = γ
where
open GaloisConnectionBetween (poset-of (𝒪 Y)) (poset-of (𝒪 X))
open PosetReasoning (poset-of (𝒪 Y))
T : Fam 𝓥 ⟨ 𝒪 Y ⟩
T = ⁅ f ⁎· V ∣ V ε S ⁆
ζ₁ : (V ≤[ poset-of (𝒪 Y) ] (f ⁎· (⋁[ 𝒪 X ] S))) holds
ζ₁ = adjunction-inequality-forward f (join-of (𝒪 X) S) V p
ζ₂ : (V ≤[ poset-of (𝒪 Y) ] (⋁[ 𝒪 Y ] ⁅ f ⁎· V ∣ V ε S ⁆)) holds
ζ₂ = V ≤⟨ ζ₁ ⟩
f ⁎· (⋁[ 𝒪 X ] S) ＝⟨ † ⟩ₚ
⋁[ 𝒪 Y ] ⁅ f ⁎· V ∣ V ε S ⁆ ■
where
† = scott-continuous-join-eq (𝒪 X) (𝒪 Y) (f ⁎·_) φ S δ
T-is-directed : is-directed (poset-of (𝒪 Y)) T holds
T-is-directed =
monotone-image-on-directed-family-is-directed (𝒪 X) (𝒪 Y) S δ (f ⁎·_) μ
where
μ : is-monotonic (poset-of (𝒪 X)) (poset-of (𝒪 Y)) (f ⁎·_) holds
μ = pr₂ (right-adjoint-of f)
γ : (Ǝ k ꞉ index S , ((f ⋆∙ U) ≤[ poset-of (𝒪 X) ] (S [ k ])) holds) holds
γ = ∥∥-rec ∃-is-prop ϵ (ϑ T T-is-directed ζ₂)
where
ϵ : _
ϵ (k , q) = ∣ k , † ∣
where
† : ((f ⋆∙ U) ≤[ poset-of (𝒪 X) ] (S [ k ])) holds
† = adjunction-inequality-backward f (S [ k ]) U q
compact-codomain-of-perfect-map-implies-compact-domain : (𝒻 : X ─c→ Y)
→ is-perfect-map 𝒻 holds
→ is-compact (𝒪 Y) holds
→ is-compact (𝒪 X) holds
compact-codomain-of-perfect-map-implies-compact-domain 𝒻@(f , φ , _) p κ = γ
where
β : (f 𝟏[ 𝒪 Y ] ≪[ 𝒪 X ] f 𝟏[ 𝒪 Y ]) holds
β = perfect-preserves-way-below 𝒻 p 𝟏[ 𝒪 Y ] 𝟏[ 𝒪 Y ] κ
γ : (𝟏[ 𝒪 X ] ≪[ 𝒪 X ] 𝟏[ 𝒪 X ]) holds
γ = transport (λ - → (- ≪[ 𝒪 X ] -) holds) φ β
perfect-maps-are-spectral : (f : X ─c→ Y)
→ (is-perfect-map f ⇒ is-spectral-map (𝒪 Y) (𝒪 X) f) holds
perfect-maps-are-spectral 𝒻@(f , _) φ U κ = perfect-preserves-way-below 𝒻 φ U U κ
spectral-maps-are-perfect : (f : X ─c→ Y)
→ is-spectral (𝒪 Y) holds
→ (is-spectral-map (𝒪 Y) (𝒪 X) f ⇒ is-perfect-map f) holds
spectral-maps-are-perfect f 𝕤 σ S δ = † , ‡
where
open Joins (λ U V → U ≤[ poset-of (𝒪 Y) ] V)
open PosetReasoning (poset-of (𝒪 Y))
f⁺ : 𝒪 Y ─f→ 𝒪 X
f⁺ = f
f₊ : ⟨ 𝒪 X ⟩ → ⟨ 𝒪 Y ⟩
f₊ = right-adjoint-of f⁺ .pr₁
f₊-is-monotone : is-monotonic (poset-of (𝒪 X)) (poset-of (𝒪 Y)) f₊ holds
f₊-is-monotone = right-adjoint-of f⁺ .pr₂
† : (f₊ (⋁[ 𝒪 X ] S) is-an-upper-bound-of ⁅ f₊ V ∣ V ε S ⁆) holds
† i = f₊ (S [ i ]) ≤⟨ ※ ⟩ f₊ (⋁[ 𝒪 X ] S) ■
where
※ = f₊-is-monotone (S [ i ] , ⋁[ 𝒪 X ] S) (⋁[ 𝒪 X ]-upper S i)
‡ : ((W , _) : upper-bound ⁅ f₊ V ∣ V ε S ⁆)
→ (f₊ (⋁[ 𝒪 X ] S) ≤[ poset-of (𝒪 Y) ] W) holds
‡ (W , p) = spectral-yoneda (𝒪 Y) 𝕤 (f₊ (⋁[ 𝒪 X ] S)) W ※
where
※ : (C : ⟨ 𝒪 Y ⟩)
→ is-compact-open (𝒪 Y) C holds
→ (C ≤[ poset-of (𝒪 Y) ] (f₊ (⋁[ 𝒪 X ] S))) holds
→ (C ≤[ poset-of (𝒪 Y) ] W) holds
※ C κ q = ∥∥-rec (holds-is-prop (C ≤[ poset-of (𝒪 Y) ] W)) γ (κ′ S δ β)
where
κ′ : is-compact-open (𝒪 X) (f ⋆∙ C) holds
κ′ = σ C κ
β : (f ⋆∙ C ≤[ poset-of (𝒪 X) ] (⋁[ 𝒪 X ] S)) holds
β = adjunction-inequality-backward f⁺ (⋁[ 𝒪 X ] S) C q
γ : (Σ i ꞉ index S , (f ⋆∙ C ≤[ poset-of (𝒪 X) ] S [ i ]) holds)
→ (C ≤[ poset-of (𝒪 Y) ] W) holds
γ (i , r) = C ≤⟨ Ⅰ ⟩ f₊ (S [ i ]) ≤⟨ Ⅱ ⟩ W ■
where
Ⅰ = adjunction-inequality-forward f (S [ i ]) C r
Ⅱ = p i
\end{code}
\begin{code}
compact-opens-are-basic-in-compact-frames : (F : Frame 𝓤 𝓥 𝓦)
→ (ℬ : Fam 𝓦 ⟨ F ⟩)
→ is-directed-basis F ℬ
→ is-compact F holds
→ (x : ⟨ F ⟩)
→ is-compact-open F x holds
→ ∥ Σ i ꞉ index ℬ , x ＝ ℬ [ i ] ∥
compact-opens-are-basic-in-compact-frames F ℬ β _ x ϟ =
∥∥-rec ∥∥-is-prop † (ϟ ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ ð γ)
where
open PosetReasoning (poset-of F)
β₀ : is-basis-for F ℬ
β₀ = pr₁ β
𝒥 = covering-index-family F ℬ β₀ x
ð : is-directed (poset-of F) ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ holds
ð = pr₂ β x
γ : (x ≤[ poset-of F ] (⋁[ F ] ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆)) holds
γ = reflexivity+ (poset-of F) (covers F ℬ β₀ x)
† : Σ i ꞉ index 𝒥 , (x ≤[ poset-of F ] (ℬ [ 𝒥 [ i ] ])) holds
→ ∥ Σ i ꞉ index ℬ , x ＝ ℬ [ i ] ∥
† (i , p) = ∣ 𝒥 [ i ] , ≤-is-antisymmetric (poset-of F) p q ∣
where
q : ((ℬ [ 𝒥 [ i ] ]) ≤[ poset-of F ] x) holds
q = ℬ [ 𝒥 [ i ] ] ≤⟨ ⋁[ F ]-upper ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ i ⟩
⋁[ F ] ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ ＝⟨ covers F ℬ β₀ x ⁻¹ ⟩ₚ
x ■
\end{code}
\begin{code}
module BasicComplements (L : Frame 𝓤 𝓥 𝓦) (𝕜 : is-compact L holds) (zᴰ : zero-dimensionalᴰ L) where
private
ℬ : Fam 𝓦 ⟨ L ⟩
ℬ = pr₁ zᴰ
¬ₓ_ : Σ c ꞉ ⟨ L ⟩ , is-compact-open L c holds → ⟨ L ⟩
¬ₓ_ (c , κ) = k
where
k : ⟨ L ⟩
k = pr₁ (pr₂ (clopen-iff-compact-in-stone-frame L (𝕜 , ∣ zᴰ ∣ ) c) κ)
¬ₓ-gives-complement : (c : ⟨ L ⟩)
→ (κ : is-compact-open L c holds)
→ is-complement-of L (¬ₓ (c , κ)) c
¬ₓ-gives-complement c κ =
pr₂ (pr₂ (clopen-iff-compact-in-stone-frame L (𝕜 , ∣ zᴰ ∣ ) c) κ)
\end{code}
\begin{code}
spectral-implies-compact : (F : Frame 𝓤 𝓥 𝓦) → (is-spectral F ⇒ is-compact F) holds
spectral-implies-compact F σ = ∥∥-rec (holds-is-prop (is-compact F)) γ σ
where
γ : spectralᴰ F → is-compact F holds
γ (ℬ , _ , (ψ , (p , _))) = ∥∥-rec (holds-is-prop (is-compact F)) β p
where
β : Σ t ꞉ index ℬ , is-top F (ℬ [ t ]) holds
→ is-compact F holds
β (t , φ) = transport (λ - → is-compact-open F - holds) δ (ψ t)
where
δ : ℬ [ t ] ＝ 𝟏[ F ]
δ = only-𝟏-is-above-𝟏 F (ℬ [ t ]) (φ 𝟏[ F ])
clopens-are-basic-in-stone-locales : (F : Frame 𝓤 𝓥 𝓦)
→ is-stone F holds
→ (ℬ : Fam 𝓦 ⟨ F ⟩)
→ is-directed-basis F ℬ
→ (x : ⟨ F ⟩)
→ is-clopen F x holds
→ ∥ Σ i ꞉ index ℬ , x ＝ ℬ [ i ] ∥
clopens-are-basic-in-stone-locales F (κ , _) ℬ δ x ζ =
compact-opens-are-basic-in-compact-frames F ℬ δ κ x †
where
† : is-compact-open F x holds
† = clopens-are-compact-in-compact-frames F κ x ζ
compacts-are-basic-in-spectralᴰ-frames : (F : Frame 𝓤 𝓥 𝓦)
→ (σ : spectralᴰ F)
→ (U : ⟨ F ⟩)
→ is-compact-open F U holds
→ let
ℬ = basisₛ F σ
I = index ℬ
in
∥ Σ i ꞉ I , U ＝ ℬ [ i ] ∥
compacts-are-basic-in-spectralᴰ-frames {𝓦 = 𝓦} F σ@(_ , β , _) U κ =
compact-opens-are-basic-in-compact-frames F (basisₛ F σ) β † U κ
where
† = spectral-implies-compact F ∣ σ ∣
\end{code}
Stone locales are spectral.
\begin{code}
stone-locales-are-spectral : (F : Frame 𝓤 𝓥 𝓦)
→ (is-stone F ⇒ is-spectral F) holds
stone-locales-are-spectral F σ@(κ , ζ) =
∥∥-rec (holds-is-prop (is-spectral F)) ♣ ζ
where
open Meets (λ x y → x ≤[ poset-of F ] y) hiding (is-top)
♣ : zero-dimensionalᴰ F → is-spectral F holds
♣ (ℬ , δ , ψ) = ∣ ℬ , δ , ϑ , † ∣
where
ϑ : consists-of-compact-opens F ℬ holds
ϑ is = pr₁ (clopen-iff-compact-in-stone-frame F σ (ℬ [ is ])) (ψ is)
τ : ∥ Σ i ꞉ index ℬ , 𝟏[ F ] ＝ ℬ [ i ] ∥
τ = compact-opens-are-basic-in-compact-frames F ℬ δ κ 𝟏[ F ] κ
†₁ : contains-top F ℬ holds
†₁ = ∥∥-rec (holds-is-prop (contains-top F ℬ)) ‡₁ τ
where
‡₁ : (Σ i ꞉ index ℬ , 𝟏[ F ] ＝ ℬ [ i ]) → contains-top F ℬ holds
‡₁ (i , p) = ∣ i , transport (λ - → is-top F - holds) p (𝟏-is-top F) ∣
†₂ : closed-under-binary-meets F ℬ holds
†₂ i j = ∥∥-rec ∃-is-prop ‡₂ υ
where
χ : is-clopen F (ℬ [ i ] ∧[ F ] ℬ [ j ]) holds
χ = clopens-are-closed-under-∧ F (ℬ [ i ]) (ℬ [ j ]) (ψ i) (ψ j)
υ : ∥ Σ k ꞉ index ℬ , (ℬ [ i ]) ∧[ F ] (ℬ [ j ]) ＝ ℬ [ k ] ∥
υ = clopens-are-basic-in-stone-locales F σ ℬ δ (ℬ [ i ] ∧[ F ] ℬ [ j ]) χ
‡₂ : (Σ k ꞉ index ℬ , (ℬ [ i ]) ∧[ F ] (ℬ [ j ]) ＝ ℬ [ k ])
→ ∥ Σ k ꞉ index ℬ , ((ℬ [ k ]) is-glb-of (ℬ [ i ] , ℬ [ j ])) holds ∥
‡₂ (k , p) = ∣ k , ‡₃ ∣
where
ρ₁ = ∧[ F ]-lower₁ (ℬ [ i ]) (ℬ [ j ])
ρ₂ = ∧[ F ]-lower₂ (ℬ [ i ]) (ℬ [ j ])
ρ₃ = λ { (z , p , q) → ∧[ F ]-greatest (ℬ [ i ]) (ℬ [ j ]) z p q}
‡₃ : ((ℬ [ k ]) is-glb-of (ℬ [ i ] , ℬ [ j ])) holds
‡₃ = transport
(λ - → (- is-glb-of (ℬ [ i ] , ℬ [ j ])) holds)
p
((ρ₁ , ρ₂) , ρ₃)
† : closed-under-finite-meets F ℬ holds
† = †₁ , †₂
\end{code}
\begin{code}
compacts-closed-under-∧-in-spectral-frames : (F : Frame 𝓤 𝓥 𝓦)
→ is-spectral F holds
→ (K₁ K₂ : ⟨ F ⟩)
→ is-compact-open F K₁ holds
→ is-compact-open F K₂ holds
→ is-compact-open F (K₁ ∧[ F ] K₂) holds
compacts-closed-under-∧-in-spectral-frames F σ K₁ K₂ κ₁ κ₂ = ∥∥-rec † γ σ
where
open Meets (λ x y → x ≤[ poset-of F ] y)
† : is-prop (is-compact-open F (K₁ ∧[ F ] K₂) holds)
† = holds-is-prop (is-compact-open F (K₁ ∧[ F ] K₂))
γ : spectralᴰ F → is-compact-open F (K₁ ∧[ F ] K₂) holds
γ σᴰ@(ℬ , φ , Κ , _ , ψ) =
∥∥-rec₂ (holds-is-prop (is-compact-open F (K₁ ∧[ F ] K₂))) δ K₁b K₂b
where
K₁b : ∥ Σ i ꞉ index ℬ , K₁ ＝ ℬ [ i ] ∥
K₁b = compacts-are-basic-in-spectralᴰ-frames F σᴰ K₁ κ₁
K₂b : ∥ Σ k ꞉ index ℬ , K₂ ＝ ℬ [ k ] ∥
K₂b = compacts-are-basic-in-spectralᴰ-frames F σᴰ K₂ κ₂
δ : Σ j ꞉ index ℬ , K₁ ＝ ℬ [ j ]
→ Σ k ꞉ index ℬ , K₂ ＝ ℬ [ k ]
→ is-compact-open F (K₁ ∧[ F ] K₂) holds
δ (j , pⱼ) (k , pₖ) =
transport (λ - → is-compact-open F - holds) (q ⁻¹) ϵ
where
q : K₁ ∧[ F ] K₂ ＝ ℬ [ j ] ∧[ F ] ℬ [ k ]
q = K₁ ∧[ F ] K₂ ＝⟨ i ⟩
ℬ [ j ] ∧[ F ] K₂ ＝⟨ ii ⟩
ℬ [ j ] ∧[ F ] ℬ [ k ] ∎
where
i = ap (λ - → - ∧[ F ] K₂) pⱼ
ii = ap (λ - → ℬ [ j ] ∧[ F ] -) pₖ
ζ : Σ l ꞉ index ℬ , ((ℬ [ l ]) is-glb-of (ℬ [ j ] , ℬ [ k ])) holds
→ is-compact-open F (ℬ [ j ] ∧[ F ] ℬ [ k ]) holds
ζ (l , θ) =
transport (λ - → is-compact-open F - holds) (∧[ F ]-unique θ) (Κ l)
ϵ : is-compact-open F (ℬ [ j ] ∧[ F ] ℬ [ k ]) holds
ϵ = ∥∥-rec (holds-is-prop (is-compact-open F _)) ζ (ψ j k)
compact-meet-lemma : (F : Frame 𝓤 𝓥 𝓦)
→ (U V K : ⟨ F ⟩)
→ is-compact-open F K holds
→ (K ≤[ poset-of F ] (U ∧[ F ] V)) holds
→ Σ K₁ ꞉ ⟨ F ⟩ , Σ K₂ ꞉ ⟨ F ⟩ ,
is-compact-open F K₁ holds
× is-compact-open F K₂ holds
× ((K ≤[ poset-of F ] (K₁ ∧[ F ] K₂)) holds)
× (((K₁ ≤[ poset-of F ] U) ∧ (K₂ ≤[ poset-of F ] V)) holds)
compact-meet-lemma F U V K κ p = K , K , κ , κ , γ , p₁ , p₂
where
open PosetReasoning (poset-of F)
γ : (K ≤[ poset-of F ] (K ∧[ F ] K)) holds
γ = ∧[ F ]-greatest K K K
(≤-is-reflexive (poset-of F) K)
(≤-is-reflexive (poset-of F) K)
p₁ : (K ≤[ poset-of F ] U) holds
p₁ = K ≤⟨ p ⟩ U ∧[ F ] V ≤⟨ ∧[ F ]-lower₁ U V ⟩ U ■
p₂ : (K ≤[ poset-of F ] V) holds
p₂ = K ≤⟨ p ⟩ U ∧[ F ] V ≤⟨ ∧[ F ]-lower₂ U V ⟩ V ■
\end{code}
## Characterisation of continuity
Let `L` and `M` be two frames and let `h : | L | → | M |` be a function.
Function `h` is said to satisfy the **continuity condition** if *for every `x :
L`, compact `b : M` with `b ≤ h(x)`, there is some compact `a : L` such that `a
≤ x` and `b ≤ h(a)`*.
\begin{code}
continuity-condition : (L : Frame 𝓤 𝓥 𝓦) (M : Frame 𝓤' 𝓥' 𝓦)
→ (⟨ L ⟩ → ⟨ M ⟩) → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺ ⊔ 𝓤' ⊔ 𝓥')
continuity-condition L M h =
Ɐ b ꞉ ⟨ M ⟩ , Ɐ x ꞉ ⟨ L ⟩ , is-compact-open M b ⇒
b ≤[ poset-of M ] h x ⇒
(Ǝ a ꞉ ⟨ L ⟩ ,
((is-compact-open L a ∧ a ≤[ poset-of L ] x ∧ b ≤[ poset-of M ] h a) holds))
\end{code}
Given frames `L` and `M`, with `M` spectral, any monotone function `h : ∣ L ∣ →
∣ M ∣` satisfying the continuity condition is Scott-continuous.
\begin{code}
characterisation-of-continuity : (L : Frame 𝓤 𝓥 𝓦)
→ (M : Frame 𝓤' 𝓥' 𝓦)
→ is-spectral M holds
→ (h : ⟨ L ⟩ → ⟨ M ⟩)
→ is-monotonic (poset-of L) (poset-of M) h holds
→ continuity-condition L M h holds
→ is-scott-continuous L M h holds
characterisation-of-continuity L M σ h μ ζ S δ = β , γ
where
open PosetReasoning (poset-of M)
open Joins (λ x y → x ≤[ poset-of M ] y)
β : (h (⋁[ L ] S) is-an-upper-bound-of ⁅ h s ∣ s ε S ⁆) holds
β i = μ (S [ i ] , ⋁[ L ] S) (⋁[ L ]-upper S i)
γ : (Ɐ (u , _) ꞉ upper-bound ⁅ h s ∣ s ε S ⁆ ,
h (⋁[ L ] S) ≤[ poset-of M ] u) holds
γ (u , φ) = spectral-yoneda M σ (h (⋁[ L ] S)) u ε
where
ε : (h (⋁[ L ] S) ≤ₖ[ M ] u) holds
ε k κ p = ∥∥-rec (holds-is-prop (k ≤[ poset-of M ] u)) † (ζ k (⋁[ L ] S) κ p)
where
† : (Σ a ꞉ ⟨ L ⟩ ,
(is-compact-open L a
∧ (a ≤[ poset-of L ] (⋁[ L ] S))
∧ (k ≤[ poset-of M ] h a)) holds)
→ (k ≤[ poset-of M ] u) holds
† (a , κₐ , q , r) =
k ≤⟨ r ⟩
h a ≤⟨ ♠ ⟩
⋁[ M ] ⁅ h s ∣ s ε S ⁆ ≤⟨ ⋁[ M ]-least ⁅ h s ∣ s ε S ⁆ (u , φ) ⟩
u ■
where
♣ : (Σ i ꞉ index S , (a ≤[ poset-of L ] (S [ i ])) holds)
→ (h a ≤[ poset-of M ] (⋁[ M ] ⁅ h s ∣ s ε S ⁆)) holds
♣ (i , ψ) = h a ≤⟨ μ (a , S [ i ]) ψ ⟩
h (S [ i ]) ≤⟨ ⋁[ M ]-upper ⁅ h s ∣ s ε S ⁆ i ⟩
⋁[ M ] ⁅ h s ∣ s ε S ⁆ ■
♠ : (h a ≤[ poset-of M ] (⋁[ M ] ⁅ h s ∣ s ε S ⁆)) holds
♠ = ∥∥-rec
(holds-is-prop (h a ≤[ poset-of M ] (⋁[ M ] ⁅ h s ∣ s ε S ⁆)))
♣
(κₐ S δ q)
\end{code}
We now prove the converse: given frames `L` and `M`, with `L` spectral, any
Scott-continuous function `h : ∣ L ∣ → ∣ M ∣` satisfies the continuity condition.
\begin{code}
characterisation-of-continuity-op : (L M : Frame 𝓤 𝓥 𝓦)
→ is-spectral L holds
→ (f : ⟨ L ⟩ → ⟨ M ⟩)
→ is-scott-continuous L M f holds
→ continuity-condition L M f holds
characterisation-of-continuity-op {𝓦 = 𝓦} L M σ f ζ =
∥∥-rec (holds-is-prop (continuity-condition L M f)) † σ
where
μ : is-monotonic (poset-of L) (poset-of M) f holds
μ = scott-continuous-implies-monotone L M f ζ
† : spectralᴰ L → continuity-condition L M f holds
† σᴰ K U κ φ = ∥∥-rec ∃-is-prop ‡ (κ ⁅ f (ℬ [ i ]) ∣ i ε 𝒥 ⁆ δ₂ ψ)
where
ℬ : Fam 𝓦 ⟨ L ⟩
ℬ = pr₁ σᴰ
𝒥 : Fam 𝓦 (index ℬ)
𝒥 = pr₁ (pr₁ (pr₁ (pr₂ σᴰ)) U)
cover : U ＝ ⋁[ L ] ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆
cover = ⋁[ L ]-unique ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ U (pr₂ (pr₁ (pr₁ (pr₂ σᴰ)) U))
‡ : (Σ k ꞉ index 𝒥 , ((K ≤[ poset-of M ] f (ℬ [ 𝒥 [ k ] ])) holds))
→ ∃ K′ ꞉ ⟨ L ⟩ , (is-compact-open L K′ holds)
× ((K′ ≤[ poset-of L ] U) holds)
× ((K ≤[ poset-of M ] f K′) holds )
‡ (k , φ) = ∣ ℬ [ 𝒥 [ k ] ] , ♥ , ♠ , φ ∣
where
open PosetReasoning (poset-of L)
♥ : is-compact-open L (ℬ [ 𝒥 [ k ] ]) holds
♥ = pr₁ (pr₂ (pr₂ σᴰ)) (𝒥 [ k ])
♠ : ((ℬ [ 𝒥 [ k ] ]) ≤[ poset-of L ] U) holds
♠ = ℬ [ 𝒥 [ k ] ] ≤⟨ ⋁[ L ]-upper ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ k ⟩
⋁[ L ] ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ ＝⟨ cover ⁻¹ ⟩ₚ
U ■
open PosetReasoning (poset-of M)
δ₁ : is-directed (poset-of L) ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ holds
δ₁ = pr₂ (pr₁ (pr₂ σᴰ)) U
ψ : (K ≤[ poset-of M ] (⋁[ M ] ⁅ f (ℬ [ i ]) ∣ i ε 𝒥 ⁆)) holds
ψ = K ≤⟨ φ ⟩
f U ＝⟨ Ⅰ ⟩ₚ
f (⋁[ L ] ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆) ＝⟨ Ⅱ ⟩ₚ
⋁[ M ] ⁅ f (ℬ [ i ]) ∣ i ε 𝒥 ⁆ ■
where
Ⅰ = ap f cover
Ⅱ = ⋁[ M ]-unique _ _ (ζ ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ δ₁)
δ₂ : is-directed (poset-of M) ⁅ f (ℬ [ i ]) ∣ i ε 𝒥 ⁆ holds
δ₂ = monotone-image-on-directed-family-is-directed L M ⁅ ℬ [ i ] ∣ i ε 𝒥 ⁆ δ₁ f μ
\end{code}
Let `F` be a spectral frame. Given `x, y, : F` and compact `a : F` with `a ≤ x ∨
y`, there exist compact `b, c : F` with `a ≤ b ∨ c` such that `b ≤ x` and `c ≤
y`.
\begin{code}
compact-join-lemma : (F : Frame 𝓤 𝓥 𝓦)
→ is-spectral F holds
→ (x y a : ⟨ F ⟩)
→ is-compact-open F a holds
→ (a ≤[ poset-of F ] (x ∨[ F ] y)) holds
→ ∃ (b , c) ꞉ ⟨ F ⟩ × ⟨ F ⟩ ,
is-compact-open F b holds
× is-compact-open F c holds
× (a ≤[ poset-of F ] (b ∨[ F ] c)) holds
× (b ≤[ poset-of F ] x ∧ c ≤[ poset-of F ] y) holds
compact-join-lemma F σ U V K κ ψ = ∥∥-rec ∃-is-prop † φ₁
where
open Joins (λ x y → x ≤[ poset-of F ] y)
open PosetReasoning (poset-of F)
Θ = ∃ (K₁ , K₂) ꞉ ⟨ F ⟩ × ⟨ F ⟩ ,
is-compact-open F K₁ holds
× is-compact-open F K₂ holds
× (K ≤[ poset-of F ] (K₁ ∨[ F ] K₂)) holds
× (K₁ ≤[ poset-of F ] U ∧ K₂ ≤[ poset-of F ] V) holds
c₁ : ⟨ F ⟩ → ⟨ F ⟩
c₁ = λ - → - ∨[ F ] V
ζ₁ : is-scott-continuous F F c₁ holds
ζ₁ = ∨-is-scott-continuous′ F V
φ₁ : ∃ K₁ ꞉ ⟨ F ⟩ , (is-compact-open F K₁
∧ (K₁ ≤[ poset-of F ] U)
∧ K ≤[ poset-of F ] (K₁ ∨[ F ] V)) holds
φ₁ = characterisation-of-continuity-op F F σ c₁ ζ₁ K U κ ψ
† : Σ K₁ ꞉ ⟨ F ⟩ , (is-compact-open F K₁
∧ (K₁ ≤[ poset-of F ] U)
∧ K ≤[ poset-of F ] (K₁ ∨[ F ] V)) holds
→ Θ
† (K₁ , κ₁ , p₁ , q₁) = ∥∥-rec ∃-is-prop ‡ φ₂
where
c₂ : ⟨ F ⟩ → ⟨ F ⟩
c₂ = λ - → K₁ ∨[ F ] -
ζ₂ : is-scott-continuous F F c₂ holds
ζ₂ = ∨-is-scott-continuous F K₁
‡ : (Σ K₂ ꞉ ⟨ F ⟩ , (is-compact-open F K₂
∧ K₂ ≤[ poset-of F ] V
∧ K ≤[ poset-of F ] (K₁ ∨[ F ] K₂)) holds)
→ Θ
‡ (K₂ , κ₂ , p₂ , q₂) = ∣ (K₁ , K₂) , κ₁ , κ₂ , q₂ , p₁ , p₂ ∣
φ₂ : ∃ K₂ ꞉ ⟨ F ⟩ , (is-compact-open F K₂
∧ K₂ ≤[ poset-of F ] V
∧ (K ≤[ poset-of F ] (K₁ ∨[ F ] K₂))) holds
φ₂ = characterisation-of-continuity-op F F σ c₂ ζ₂ K V κ q₁
\end{code}
\begin{code}
open import Locales.HeytingImplication pt fe
module LemmasAboutHeytingComplementation (X : Locale 𝓤 𝓥 𝓥)
(𝒷 : has-basis (𝒪 X) holds) where
open HeytingImplicationConstruction X 𝒷
complement-is-heyting-complement : (C C′ : ⟨ 𝒪 X ⟩)
→ is-complement-of (𝒪 X) C′ C
→ C′ ＝ C ==> 𝟎[ 𝒪 X ]
complement-is-heyting-complement C C′ (p , q) =
≤-is-antisymmetric (poset-of (𝒪 X)) † ‡
where
open PosetReasoning (poset-of (𝒪 X))
※ : (((C ==> 𝟎[ 𝒪 X ]) ∧[ 𝒪 X ] (C ∨[ 𝒪 X ] C′)) ≤[ poset-of (𝒪 X) ] C′) holds
※ =
(C ==> 𝟎[ 𝒪 X ]) ∧[ 𝒪 X ] (C ∨[ 𝒪 X ] C′) ＝⟨ Ⅰ ⟩ₚ
((C ==> 𝟎[ 𝒪 X ]) ∧[ 𝒪 X ] C) ∨[ 𝒪 X ] ((C ==> 𝟎[ 𝒪 X ]) ∧[ 𝒪 X ] C′) ≤⟨ Ⅱ ⟩
C′ ■
where
Ⅰ = binary-distributivity (𝒪 X) (C ==> 𝟎[ 𝒪 X ]) C C′
Ⅱ = ∨[ 𝒪 X ]-least
((C ==> 𝟎[ 𝒪 X ]) ∧[ 𝒪 X ] C ≤⟨ mp-right C 𝟎[ 𝒪 X ] ⟩
𝟎[ 𝒪 X ] ≤⟨ 𝟎-is-bottom (𝒪 X) C′ ⟩
C′ ■)
(∧[ 𝒪 X ]-lower₂ (C ==> 𝟎[ 𝒪 X ]) C′)
† : (C′ ≤[ poset-of (𝒪 X) ] (C ==> 𝟎[ 𝒪 X ])) holds
† = heyting-implication₁ C 𝟎[ 𝒪 X ] C′ †₁
where
†₁ : ((C′ ∧[ 𝒪 X ] C) ≤[ poset-of (𝒪 X) ] 𝟎[ 𝒪 X ]) holds
†₁ = C′ ∧[ 𝒪 X ] C ＝⟨ ∧[ 𝒪 X ]-is-commutative C′ C ⟩ₚ
C ∧[ 𝒪 X ] C′ ＝⟨ p ⟩ₚ
𝟎[ 𝒪 X ] ■
‡ : (C ==> 𝟎[ 𝒪 X ] ≤[ poset-of (𝒪 X) ] C′) holds
‡ = C ==> 𝟎[ 𝒪 X ] ≤⟨ Ⅰ ⟩
(C ∨[ 𝒪 X ] C′) ==> C′ ＝⟨ Ⅱ ⟩ₚ
𝟏[ 𝒪 X ] ==> C′ ＝⟨ 𝟏-==>-law C′ ⁻¹ ⟩ₚ
C′ ■
where
Ⅰ = heyting-implication₁ (C ∨[ 𝒪 X ] C′) C′ (C ==> 𝟎[ 𝒪 X ]) ※
Ⅱ = ap (λ - → - ==> C′) q
heyting-complement-is-complement : (C C′ : ⟨ 𝒪 X ⟩)
→ is-complement-of (𝒪 X) C′ C
→ is-complement-of (𝒪 X) (C ==> 𝟎[ 𝒪 X ]) C
heyting-complement-is-complement C C′ (p , q) = † , ‡
where
† : C ∧[ 𝒪 X ] (C ==> 𝟎[ 𝒪 X ]) ＝ 𝟎[ 𝒪 X ]
† = C ∧[ 𝒪 X ] (C ==> 𝟎[ 𝒪 X ]) ＝⟨ ※ ⟩
C ∧[ 𝒪 X ] C′ ＝⟨ p ⟩
𝟎[ 𝒪 X ] ∎
where
※ = ap
(λ - → C ∧[ 𝒪 X ] -)
(complement-is-heyting-complement C C′ (p , q) ⁻¹)
‡ : C ∨[ 𝒪 X ] (C ==> 𝟎[ 𝒪 X ]) ＝ 𝟏[ 𝒪 X ]
‡ = C ∨[ 𝒪 X ] (C ==> 𝟎[ 𝒪 X ]) ＝⟨ ※ ⟩
C ∨[ 𝒪 X ] C′ ＝⟨ q ⟩
𝟏[ 𝒪 X ] ∎
where
※ = ap
(λ - → C ∨[ 𝒪 X ] -)
(complement-is-heyting-complement C C′ (p , q) ⁻¹)
material-implication : (C U : ⟨ 𝒪 X ⟩)
→ is-clopen₀ (𝒪 X) C
→ (C ==> U) ＝ (C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U
material-implication C U (C′ , p , q) = ≤-is-antisymmetric (poset-of (𝒪 X)) † ‡
where
open PosetReasoning (poset-of (𝒪 X))
† : ((C ==> U) ≤[ poset-of (𝒪 X) ] ((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U)) holds
† = (C ==> U) ≤⟨ Ⅰ ⟩
(C ∨[ 𝒪 X ] C′) ==> ((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U) ＝⟨ Ⅱ ⟩ₚ
𝟏[ 𝒪 X ] ==> ((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U) ＝⟨ Ⅲ ⟩ₚ
(C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U ■
where
※ = (C ==> U) ∧[ 𝒪 X ] (C ∨[ 𝒪 X ] C′) ＝⟨ Ⅰ ⟩ₚ
((C ==> U) ∧[ 𝒪 X ] C) ∨[ 𝒪 X ] ((C ==> U) ∧[ 𝒪 X ] C′) ≤⟨ Ⅱ ⟩
U ∨[ 𝒪 X ] ((C ==> U) ∧[ 𝒪 X ] C′) ≤⟨ Ⅲ ⟩
U ∨[ 𝒪 X ] C′ ＝⟨ Ⅳ ⟩ₚ
C′ ∨[ 𝒪 X ] U ＝⟨ Ⅴ ⟩ₚ
(C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U ■
where
Ⅰ = binary-distributivity (𝒪 X) (C ==> U) C C′
Ⅱ = ∨[ 𝒪 X ]-left-monotone (mp-right C U)
Ⅲ = ∨[ 𝒪 X ]-right-monotone (∧[ 𝒪 X ]-lower₂ (C ==> U) C′)
Ⅳ = ∨[ 𝒪 X ]-is-commutative U C′
Ⅴ = ap
(λ - → - ∨[ 𝒪 X ] U)
(complement-is-heyting-complement C C′ (p , q))
Ⅰ = heyting-implication₁
(C ∨[ 𝒪 X ] C′)
((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U)
(C ==> U)
※
Ⅱ = ap (λ - → - ==> ((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U)) q
Ⅲ = 𝟏-==>-law ((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U) ⁻¹
‡ : (((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U) ≤[ poset-of (𝒪 X) ] (C ==> U)) holds
‡ = heyting-implication₁ C U ((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U) ‡₁
where
‡₁ : ((((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U) ∧[ 𝒪 X ] C)
≤[ poset-of (𝒪 X) ]
U) holds
‡₁ = ((C ==> 𝟎[ 𝒪 X ]) ∨[ 𝒪 X ] U) ∧[ 𝒪 X ] C ＝⟨ Ⅰ ⟩ₚ
((C ==> 𝟎[ 𝒪 X ]) ∧[ 𝒪 X ] C) ∨[ 𝒪 X ] (U ∧[ 𝒪 X ] C) ≤⟨ Ⅱ ⟩
U ■
where
※ = (C ==> 𝟎[ 𝒪 X ]) ∧[ 𝒪 X ] C ≤⟨ mp-right C 𝟎[ 𝒪 X ] ⟩
𝟎[ 𝒪 X ] ≤⟨ 𝟎-is-bottom (𝒪 X) U ⟩
U ■
Ⅰ = binary-distributivity-right (𝒪 X)
Ⅱ = ∨[ 𝒪 X ]-least ※ (∧[ 𝒪 X ]-lower₁ U C)
double-negation-elimination : (C : ⟨ 𝒪 X ⟩)
→ is-clopen₀ (𝒪 X) C
→ (C ==> 𝟎[ 𝒪 X ]) ==> 𝟎[ 𝒪 X ] ＝ C
double-negation-elimination C (C′ , p , q) =
≤-is-antisymmetric (poset-of (𝒪 X)) † ‡
where
open PosetReasoning (poset-of (𝒪 X))
† : (((C ==> 𝟎[ 𝒪 X ]) ==> 𝟎[ 𝒪 X ]) ≤[ poset-of (𝒪 X) ] C) holds
† = (C ==> 𝟎[ 𝒪 X ]) ==> 𝟎[ 𝒪 X ] ＝⟨ Ⅰ ⟩ₚ
C′ ==> 𝟎[ 𝒪 X ] ＝⟨ Ⅱ ⟩ₚ
C ■
where
Ⅰ = ap
(λ - → - ==> 𝟎[ 𝒪 X ])
(complement-is-heyting-complement C C′ (p , q) ⁻¹)
Ⅱ = complement-is-heyting-complement C′ C (Ⅱ₁ , Ⅱ₂) ⁻¹
where
Ⅱ₁ = C′ ∧[ 𝒪 X ] C ＝⟨ ∧[ 𝒪 X ]-is-commutative C′ C ⟩
C ∧[ 𝒪 X ] C′ ＝⟨ p ⟩
𝟎[ 𝒪 X ] ∎
Ⅱ₂ = C′ ∨[ 𝒪 X ] C ＝⟨ ∨[ 𝒪 X ]-is-commutative C′ C ⟩
C ∨[ 𝒪 X ] C′ ＝⟨ q ⟩
𝟏[ 𝒪 X ] ∎
‡ : (C ≤[ poset-of (𝒪 X) ] (C ==> 𝟎[ 𝒪 X ]) ==> 𝟎[ 𝒪 X ]) holds
‡ = heyting-implication₁ (C ==> 𝟎[ 𝒪 X ]) 𝟎[ 𝒪 X ] C ‡₁
where
‡₁ : ((C ∧[ 𝒪 X ] (C ==> 𝟎[ 𝒪 X ])) ≤[ poset-of (𝒪 X) ] 𝟎[ 𝒪 X ]) holds
‡₁ = mp-left C 𝟎[ 𝒪 X ]
negation-∨-lemma₁ : {U V W : ⟨ 𝒪 X ⟩}
→ is-clopen₀ (𝒪 X) V
→ (U ≤[ poset-of (𝒪 X) ] (V ∨[ 𝒪 X ] W)) holds
→ ((U ∧[ 𝒪 X ] (V ==> 𝟎[ 𝒪 X ]))
≤[ poset-of (𝒪 X) ]
W) holds
negation-∨-lemma₁ {U} {V} {W} (V′ , p , q) φ =
U ∧[ 𝒪 X ] (V ==> 𝟎[ 𝒪 X ]) ＝⟨ Ⅰ ⟩ₚ
U ∧[ 𝒪 X ] V′ ≤⟨ Ⅱ ⟩
(V ∨[ 𝒪 X ] W) ∧[ 𝒪 X ] V′ ＝⟨ Ⅲ ⟩ₚ
(V ∧[ 𝒪 X ] V′) ∨[ 𝒪 X ] (W ∧[ 𝒪 X ] V′) ＝⟨ Ⅳ ⟩ₚ
𝟎[ 𝒪 X ] ∨[ 𝒪 X ] (W ∧[ 𝒪 X ] V′) ＝⟨ Ⅴ ⟩ₚ
W ∧[ 𝒪 X ] V′ ≤⟨ Ⅵ ⟩
W ■
where
open PosetReasoning (poset-of (𝒪 X))
Ⅰ = ap
(λ - → U ∧[ 𝒪 X ] -)
(complement-is-heyting-complement V V′ (p , q) ⁻¹)
Ⅱ = ∧[ 𝒪 X ]-left-monotone φ
Ⅲ = binary-distributivity-right (𝒪 X)
Ⅳ = ap (λ - → - ∨[ 𝒪 X ] (W ∧[ 𝒪 X ] V′)) p
Ⅴ = 𝟎-right-unit-of-∨ (𝒪 X) (W ∧[ 𝒪 X ] V′)
Ⅵ = ∧[ 𝒪 X ]-lower₁ W V′
negation-∨-lemma₂ : {U V W : ⟨ 𝒪 X ⟩}
→ is-clopen₀ (𝒪 X) V
→ ((U ∧[ 𝒪 X ] (V ==> 𝟎[ 𝒪 X ]))
≤[ poset-of (𝒪 X) ]
W) holds
→ (U ≤[ poset-of (𝒪 X) ] (V ∨[ 𝒪 X ] W)) holds
negation-∨-lemma₂ {U} {V} {W} (V′ , p , q) φ =
U ＝⟨ Ⅰ ⟩ₚ
U ∧[ 𝒪 X ] 𝟏[ 𝒪 X ] ＝⟨ Ⅱ ⟩ₚ
U ∧[ 𝒪 X ] (V ∨[ 𝒪 X ] V′) ＝⟨ Ⅲ ⟩ₚ
(U ∧[ 𝒪 X ] V) ∨[ 𝒪 X ] (U ∧[ 𝒪 X ] V′) ＝⟨ Ⅳ ⟩ₚ
(U ∧[ 𝒪 X ] V) ∨[ 𝒪 X ] (U ∧[ 𝒪 X ] (V ==> 𝟎[ 𝒪 X ])) ≤⟨ Ⅴ ⟩
(U ∧[ 𝒪 X ] V) ∨[ 𝒪 X ] W ≤⟨ Ⅵ ⟩
V ∨[ 𝒪 X ] W ■
where
open PosetReasoning (poset-of (𝒪 X))
Ⅰ = 𝟏-right-unit-of-∧ (𝒪 X) U ⁻¹
Ⅱ = ap (λ - → U ∧[ 𝒪 X ] -) (q ⁻¹)
Ⅲ = binary-distributivity (𝒪 X) U V V′
Ⅳ = ap
(λ - → (U ∧[ 𝒪 X ] V) ∨[ 𝒪 X ] (U ∧[ 𝒪 X ] -))
(complement-is-heyting-complement V V′ (p , q))
Ⅴ = ∨[ 𝒪 X ]-right-monotone φ
Ⅵ = ∨[ 𝒪 X ]-left-monotone (∧[ 𝒪 X ]-lower₂ U V)
\end{code}
\section{CNF Transformation for Spectrality}
Section added on 2023-08-17.
Given a basis closed under binary meets, the directification of that basis using
the `directify` function is also closed under binary meets. The reason is that
the meets of joins can be turned into joins of meets. In this section, we prove
this fact.
To define CNF transformation, we need the following function
`conjunct-with-list` which takes some `x` and some list `y₁ , … , yₙ` and
computes `(x ∧ y₁) , … , (x ∧ yₙ)`.
\begin{code}
conjunct-with-list : (F : Frame 𝓤 𝓥 𝓦)
→ ⟨ F ⟩ → List ⟨ F ⟩ → List ⟨ F ⟩
conjunct-with-list F x = map (λ - → x ∧[ F ] -)
cnf-transform : (F : Frame 𝓤 𝓥 𝓦)
→ List ⟨ F ⟩ → List ⟨ F ⟩ → ⟨ F ⟩
cnf-transform F [] ys = 𝟎[ F ]
cnf-transform F (x ∷ xs) ys =
(⋁ₗ[ F ] conjunct-with-list F x ys) ∨[ F ] cnf-transform F xs ys
\end{code}
Given some `x : ⟨ F ⟩` and a list `(y₁ , … , yₙ) : List ⟨ F ⟩`,
`x ∧ (y₁ ∨ … ∨ yₙ) ＝ (x ∧ y₁) ∨ … ∨ (x ∧ yₙ)`, which is of course just an
instance of the distributivity law. We prove this fact next.
\begin{code}
distributivity-list : (F : Frame 𝓤 𝓥 𝓦) (x : ⟨ F ⟩) (ys : List ⟨ F ⟩)
→ x ∧[ F ] (⋁ₗ[ F ] ys) ＝ ⋁ₗ[ F ] (conjunct-with-list F x ys)
distributivity-list F x [] = 𝟎-right-annihilator-for-∧ F x
distributivity-list F x (y ∷ ys) =
x ∧[ F ] (y ∨[ F ] (⋁ₗ[ F ] ys)) ＝⟨ Ⅰ ⟩
(x ∧[ F ] y) ∨[ F ] (x ∧[ F ] (⋁ₗ[ F ] ys)) ＝⟨ Ⅱ ⟩
(x ∧[ F ] y) ∨[ F ] (⋁ₗ[ F ] conjunct-with-list F x ys) ＝⟨ refl ⟩
⋁ₗ[ F ] (conjunct-with-list F x (y ∷ ys)) ∎
where
Ⅰ = binary-distributivity F x y (join-list F ys)
Ⅱ = ap (λ - → (x ∧[ F ] y) ∨[ F ] -) (distributivity-list F x ys)
\end{code}
With `distributivity-list` in hand, we are ready to prove the correctness of the
CNF transformation procedure.
\begin{code}
cnf-transform-correct : (F : Frame 𝓤 𝓥 𝓦) (xs ys : List ⟨ F ⟩)
→ (⋁ₗ[ F ] xs) ∧[ F ] (⋁ₗ[ F ] ys) ＝ cnf-transform F xs ys
cnf-transform-correct F [] ys = 𝟎-left-annihilator-for-∧ F ((⋁ₗ[ F ] ys))
cnf-transform-correct F (x ∷ xs) ys =
(x ∨[ F ] (⋁ₗ[ F ] xs)) ∧[ F ] (⋁ₗ[ F ] ys) ＝⟨ Ⅰ ⟩
(x ∧[ F ] (⋁ₗ[ F ] ys)) ∨[ F ] ((⋁ₗ[ F ] xs) ∧[ F ] (⋁ₗ[ F ] ys)) ＝⟨ Ⅱ ⟩
(x ∧[ F ] (⋁ₗ[ F ] ys)) ∨[ F ] cnf-transform F xs ys ＝⟨ Ⅲ ⟩
(⋁ₗ[ F ] conjunct-with-list F x ys) ∨[ F ] cnf-transform F xs ys ＝⟨ refl ⟩
cnf-transform F (x ∷ xs) ys ∎
where
Ⅰ = binary-distributivity-right F
Ⅱ = ap
(λ - → (x ∧[ F ] (⋁ₗ[ F ] ys)) ∨[ F ] -)
(cnf-transform-correct F xs ys)
Ⅲ = ap (λ - → - ∨[ F ] cnf-transform F xs ys) (distributivity-list F x ys)
\end{code}
We now start proving, making use of `cnf-transform-correct`, that the CNF
transformation of two basic opens is itself basic.
We first prove the analogous fact that the `conjunct-with-list` function:
\begin{code}
conjunct-with-list-is-basic : (F : Frame 𝓤 𝓥 𝓦) (ℬ : Fam 𝓦 ⟨ F ⟩)
→ (β : is-basis-for F ℬ)
→ closed-under-binary-meets F ℬ holds
→ let
ℬ↑ = directify F ℬ
β↑ = directified-basis-is-basis F ℬ β
in
(i : index ℬ) (is : index ℬ↑) →
∃ ks ꞉ index ℬ↑ ,
ℬ↑ [ ks ]
＝ ⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> is))
conjunct-with-list-is-basic F ℬ β p i [] = ∣ [] , refl ∣
conjunct-with-list-is-basic F ℬ β p i (j ∷ js) = ∥∥-rec ∃-is-prop γ μ
where
open Meets (λ x y → x ≤[ poset-of F ] y)
ℬ↑ = directify F ℬ
\end{code}
We know by the closure of `ℬ` under binary meets that the meet of `ℬ[ i ]` and
`ℬ[ j ]` is in the basis, given by some index `k`.
\begin{code}
μ : ∃ k ꞉ index ℬ , ((ℬ [ k ]) is-glb-of (ℬ [ i ] , ℬ [ j ])) holds
μ = p i j
\end{code}
We unpack this truncated sigma inside `γ`:
\begin{code}
γ : Σ k ꞉ index ℬ , ((ℬ [ k ]) is-glb-of (ℬ [ i ] , ℬ [ j ])) holds
→ ∃ ks ꞉ index ℬ↑ ,
ℬ↑ [ ks ] ＝ ⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> (j ∷ js)))
γ (k , q) = ∥∥-rec ∃-is-prop δ IH
where
\end{code}
Now, by the I.H. on `ℬ[ i ]`, we also get some `ks` corresponding to the index
of conjuncting `ℬ[ i ]` with each `ℬ[ j ]` given by `js.`
\begin{code}
IH : ∃ ks ꞉ index ℬ↑ ,
ℬ↑ [ ks ] ＝ ⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> js))
IH = conjunct-with-list-is-basic F ℬ β p i js
\end{code}
Once again, we unpack this truncated sigma inside `δ`:
\begin{code}
δ : Σ ks ꞉ index ℬ↑ ,
ℬ↑ [ ks ] ＝ ⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> js))
→ ∃ ls ꞉ index ℬ↑ ,
ℬ↑ [ ls ] ＝ ⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> (j ∷ js)))
δ (ks , r) = ∣ (k ∷ ks) , † ∣
where
\end{code}
The list of indices that we need for the desired result is then simply `k ∷ ks`.
The proof that this satisfies the desired property is given in `†` below.
\begin{code}
w = ⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> js))
† : ℬ↑ [ k ∷ ks ]
＝ ⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> (j ∷ js)))
† =
ℬ [ k ] ∨[ F ] ℬ↑ [ ks ] ＝⟨ Ⅰ ⟩
ℬ [ k ] ∨[ F ] w ＝⟨ Ⅱ ⟩
(ℬ [ i ] ∧[ F ] ℬ [ j ]) ∨[ F ] w ＝⟨ refl ⟩
⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> (j ∷ js))) ∎
where
Ⅰ = ap (λ - → ℬ [ k ] ∨[ F ] -) r
Ⅱ = ap (λ - → - ∨[ F ] w) (∧[ F ]-unique q)
\end{code}
We are now ready to prove the desired result: that the meet of two basic opens
is basic.
\begin{code}
cnf-transform-is-basic : (F : Frame 𝓤 𝓥 𝓦) (ℬ : Fam 𝓦 ⟨ F ⟩)
→ (β : is-basis-for F ℬ)
→ closed-under-binary-meets F ℬ holds
→ let
ℬ↑ = directify F ℬ
β↑ = directified-basis-is-basis F ℬ β
in
(is js : index ℬ↑) →
∃ ks ꞉ index ℬ↑ ,
ℬ↑ [ ks ] ＝ (ℬ↑ [ is ]) ∧[ F ] (ℬ↑ [ js ])
cnf-transform-is-basic F ℬ β p [] js =
∣ [] , (𝟎-left-annihilator-for-∧ F (directify F ℬ [ js ]) ⁻¹) ∣
cnf-transform-is-basic F ℬ β p (i ∷ is) js =
∥∥-rec ∥∥-is-prop γ (cnf-transform-is-basic F ℬ β p is js)
where
ℬ↑ = directify F ℬ
\end{code}
We first record the following trivial `lemma`:
\begin{code}
lemma : (is js : index ℬ↑)
→ ℬ↑ [ is ] ∧[ F ] ℬ↑ [ js ]
＝ join-in-frame′ F ℬ is ∧[ F ] join-in-frame′ F ℬ js
lemma is js =
let
Ⅰ = ap
(λ - → - ∧[ F ] ℬ↑ [ js ])
(join-in-frame-equality F ℬ is)
Ⅱ = ap
(λ - → (⋁ₗ[ F ] ((ℬ [_]) <$> is)) ∧[ F ] -)
(join-in-frame-equality F ℬ js)
in
ℬ↑ [ is ] ∧[ F ] ℬ↑ [ js ] ＝⟨ Ⅰ ⟩
(⋁ₗ[ F ] ((ℬ [_]) <$> is)) ∧[ F ] ℬ↑ [ js ] ＝⟨ Ⅱ ⟩
(⋁ₗ[ F ] ((ℬ [_]) <$> is)) ∧[ F ] (⋁ₗ[ F ] ((ℬ [_]) <$> js)) ∎
\end{code}
In `γ`, we unpack the truncated sigma given by the I.H.:
\begin{code}
γ : Σ ks ꞉ index ℬ↑ , ℬ↑ [ ks ] ＝ ℬ↑ [ is ] ∧[ F ] ℬ↑ [ js ]
→ ∃ ks ꞉ index ℬ↑ , ℬ↑ [ ks ] ＝ (ℬ [ i ] ∨[ F ] ℬ↑ [ is ]) ∧[ F ] ℬ↑ [ js ]
γ (ks , q) =
let
\end{code}
We know by `conjunct-with-list-is-basic` that there is a basis index
corresponding to `conjunct-with-list (ℬ [ i ]) ((ℬ [_]) <$> js)`. We refer to
this as `ls`.
\begin{code}
† : ∃ ls ꞉ index ℬ↑ ,
ℬ↑ [ ls ] ＝ ⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> js))
† = conjunct-with-list-is-basic F ℬ β p i js
in
\end{code}
We proceed by truncation recursion on this truncated sigma, with the contents
unpacked in the function `δ`.
\begin{code}
∥∥-rec ∃-is-prop δ †
where
\end{code}
As we will have to refer to `(ℬ [_]) <$> is` and `(ℬ [_]) <$> js` frequently,
we introduce abbrevations for them:
\begin{code}
ℬ-is = (ℬ [_]) <$> is
ℬ-js = (ℬ [_]) <$> js
\end{code}
Combining `lemma` and the correctness of `cnf-transform`, we have that `ℬ↑[ ks
]` is the CNF transformation of the meet of the joins of `is` and `js`.
\begin{code}
♣ : ℬ↑ [ ks ] ＝ cnf-transform F ((ℬ [_]) <$> is) ((ℬ [_]) <$> js)
♣ =
ℬ↑ [ ks ] ＝⟨ Ⅰ ⟩
ℬ↑ [ is ] ∧[ F ] ℬ↑ [ js ] ＝⟨ Ⅱ ⟩
(⋁ₗ[ F ] ℬ-is) ∧[ F ] (⋁ₗ[ F ] ((ℬ [_]) <$> js)) ＝⟨ Ⅲ ⟩
cnf-transform F ℬ-is ((ℬ [_]) <$> js) ∎
where
Ⅰ = q
Ⅱ = lemma is js
Ⅲ = cnf-transform-correct F ℬ-is ℬ-js
\end{code}
As `⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> js))` is mentioned
quite frequently, we introduce the abbreviation `w` for it:
\begin{code}
w = ⋁ₗ[ F ] (conjunct-with-list F (ℬ [ i ]) ((ℬ [_]) <$> js))
\end{code}
The desired list of indices is just `ls ++ ks`:
\begin{code}
δ : (Σ ls ꞉ index ℬ↑ , ℬ↑ [ ls ] ＝ w)
→ ∃ ms ꞉ index ℬ↑ ,
ℬ↑ [ ms ] ＝ (ℬ [ i ] ∨[ F ] ℬ↑ [ is ]) ∧[ F ] ℬ↑ [ js ]
δ (ls , r) = ∣ (ls ++ ks) , ‡ ∣
where
\end{code}
\begin{code}
‡ : ℬ↑ [ ls ++ ks ] ＝ (ℬ [ i ] ∨[ F ] ℬ↑ [ is ]) ∧[ F ] ℬ↑ [ js ]
‡ =
ℬ↑ [ ls ++ ks ] ＝⟨ Ⅰ ⟩
ℬ↑ [ ls ] ∨[ F ] ℬ↑ [ ks ] ＝⟨ Ⅱ ⟩
w ∨[ F ] ℬ↑ [ ks ] ＝⟨ Ⅲ ⟩
w ∨[ F ] (cnf-transform F ℬ-is ℬ-js) ＝⟨ refl ⟩
cnf-transform F ((ℬ [_]) <$> (i ∷ is)) ℬ-js ＝⟨ Ⅳ ⟩
(⋁ₗ[ F ] ((ℬ [_]) <$> (i ∷ is))) ∧[ F ] (⋁ₗ[ F ] ℬ-js) ＝⟨ Ⅴ ⟩
(ℬ↑ [ i ∷ is ]) ∧[ F ] join-list F ℬ-js ＝⟨ Ⅵ ⟩
(ℬ↑ [ i ∷ is ]) ∧[ F ] (ℬ↑ [ js ]) ＝⟨ refl ⟩
(ℬ [ i ] ∨[ F ] ℬ↑ [ is ]) ∧[ F ] (ℬ↑ [ js ]) ∎
where
Ⅰ = directify-functorial F ℬ ls ks
Ⅱ = ap (λ - → - ∨[ F ] ℬ↑ [ ks ]) r
Ⅲ = ap (λ - → w ∨[ F ] -) ♣
Ⅳ = cnf-transform-correct F ((ℬ [_]) <$> (i ∷ is)) ℬ-js ⁻¹
Ⅴ = ap
(λ - → - ∧[ F ] (⋁ₗ[ F ] ℬ-js))
(join-in-frame-equality F ℬ (i ∷ is) ⁻¹)
Ⅵ = ap
(λ - → (ℬ↑ [ i ∷ is ]) ∧[ F ] -)
(join-in-frame-equality F ℬ js ⁻¹)
\end{code}
This is the result that we wanted: directification of a basis preserves its
closure under binary meets. In the following definition, we make this a bit more
explicit:
\begin{code}
directify-preserves-closure-under-∧ : (F : Frame 𝓤 𝓥 𝓦)
→ (ℬ : Fam 𝓦 ⟨ F ⟩)
→ (β : is-basis-for F ℬ)
→ closed-under-binary-meets F ℬ holds
→ let
ℬ↑ = directify F ℬ
β↑ = directified-basis-is-basis F ℬ β
in
closed-under-binary-meets F ℬ↑ holds
directify-preserves-closure-under-∧ F ℬ β ϑ is js =
∥∥-rec ∃-is-prop γ (cnf-transform-is-basic F ℬ β ϑ is js)
where
open Meets (λ x y → x ≤[ poset-of F ] y)
ℬ↑ = directify F ℬ
x = ℬ↑ [ is ]
y = ℬ↑ [ js ]
γ : Σ ks ꞉ (index ℬ↑) , ℬ↑ [ ks ] ＝ ℬ↑ [ is ] ∧[ F ] ℬ↑ [ js ]
→ ∃ ks ꞉ index ℬ↑ , (((ℬ↑ [ ks ]) is-glb-of (x , y)) holds)
γ (ks , p) =
let
† : ((x ∧[ F ] y) is-glb-of (x , y)) holds
† = (∧[ F ]-lower₁ x y , ∧[ F ]-lower₂ x y)
, λ (z , p) → uncurry (∧[ F ]-greatest x y z) p
in
∣ ks , transport (λ - → (- is-glb-of (x , y)) holds) (p ⁻¹) † ∣
\end{code}
Section added on 2023-08-17.
\section{Spectrality of the initial frame}
\begin{code}
module SpectralityOfTheInitialFrame (𝓤 : Universe) (pe : propext 𝓤) where
open Spectrality-of-𝟎 𝓤 pe
bottom-of-𝟎Frm-is-⊥ : ⊥ ＝ 𝟎[ 𝟎-𝔽𝕣𝕞 pe ]
bottom-of-𝟎Frm-is-⊥ = only-𝟎-is-below-𝟎 (𝟎-𝔽𝕣𝕞 pe) ⊥ (λ ())
𝟎Frm-is-compact : is-compact (𝟎-𝔽𝕣𝕞 pe) holds
𝟎Frm-is-compact S (∣i∣ , u) p = ∥∥-rec ∃-is-prop † (p ⋆)
where
† : (Σ j ꞉ index S , ((S [ j ]) holds))
→ ∃ j ꞉ index S , (𝟏[ 𝟎-𝔽𝕣𝕞 pe ] ≤[ poset-of (𝟎-𝔽𝕣𝕞 pe) ] S [ j ]) holds
† (j , q) = ∣ j , (λ _ → q) ∣
ℬ𝟎-consists-of-compact-opens : consists-of-compact-opens (𝟎-𝔽𝕣𝕞 pe) ℬ𝟎 holds
ℬ𝟎-consists-of-compact-opens (inl ⋆) =
transport
(λ - → is-compact-open (𝟎-𝔽𝕣𝕞 pe) - holds)
(bottom-of-𝟎Frm-is-⊥ ⁻¹)
(𝟎-is-compact (𝟎-𝔽𝕣𝕞 pe))
ℬ𝟎-consists-of-compact-opens (inr ⋆) = 𝟎Frm-is-compact
and₂-lemma₁ : (x y : 𝟚 𝓤) → (ℬ𝟎 [ and₂ x y ] ≤[ poset-of (𝟎-𝔽𝕣𝕞 pe) ] ℬ𝟎 [ x ]) holds
and₂-lemma₁ (inl ⋆) y = λ ()
and₂-lemma₁ (inr ⋆) (inl ⋆) = λ ()
and₂-lemma₁ (inr ⋆) (inr ⋆) = λ { ⋆ → ⋆}
and₂-lemma₂ : (x y : 𝟚 𝓤) → (ℬ𝟎 [ and₂ x y ] ≤[ poset-of (𝟎-𝔽𝕣𝕞 pe) ] ℬ𝟎 [ y ]) holds
and₂-lemma₂ (inl ⋆) y = λ ()
and₂-lemma₂ (inr ⋆) (inl ⋆) = λ ()
and₂-lemma₂ (inr ⋆) (inr ⋆) = λ { ⋆ → ⋆}
open Meets (λ x y → x ≤[ poset-of (𝟎-𝔽𝕣𝕞 pe) ] y) hiding (is-top)
and₂-lemma₃ : (x y : 𝟚 𝓤) ((z , _) : lower-bound (ℬ𝟎 [ x ] , ℬ𝟎 [ y ]))
→ (z ≤[ poset-of (𝟎-𝔽𝕣𝕞 pe) ] ℬ𝟎 [ and₂ x y ]) holds
and₂-lemma₃ (inl ⋆) y (z , p₁ , p₂) = p₁
and₂-lemma₃ (inr ⋆) y (z , p₁ , p₂) = p₂
ℬ𝟎-is-closed-under-binary-meets : closed-under-binary-meets (𝟎-𝔽𝕣𝕞 pe) ℬ𝟎 holds
ℬ𝟎-is-closed-under-binary-meets i j = ∣ and₂ i j , (†₁ , †₂) , and₂-lemma₃ i j ∣
where
†₁ : (ℬ𝟎 [ and₂ i j ] ≤[ poset-of (𝟎-𝔽𝕣𝕞 pe) ] ℬ𝟎 [ i ]) holds
†₁ = and₂-lemma₁ i j
†₂ : (ℬ𝟎 [ and₂ i j ] ≤[ poset-of (𝟎-𝔽𝕣𝕞 pe) ] ℬ𝟎 [ j ]) holds
†₂ = and₂-lemma₂ i j
𝟎-𝔽𝕣𝕞-is-spectral : is-spectral (𝟎-𝔽𝕣𝕞 pe) holds
𝟎-𝔽𝕣𝕞-is-spectral = ∣ ℬ𝟎↑ , ℬ𝟎-is-directed-basis-for-𝟎 , κ , γ ∣
where
κ : consists-of-compact-opens (𝟎-𝔽𝕣𝕞 pe) ℬ𝟎↑ holds
κ [] = 𝟎-is-compact (𝟎-𝔽𝕣𝕞 pe)
κ (i ∷ is) = compacts-are-closed-under-joins
(𝟎-𝔽𝕣𝕞 pe)
(ℬ𝟎 [ i ])
(ℬ𝟎↑ [ is ])
(ℬ𝟎-consists-of-compact-opens i)
(κ is)
t : is-top (𝟎-𝔽𝕣𝕞 pe) (𝟏[ 𝟎-𝔽𝕣𝕞 pe ] ∨[ 𝟎-𝔽𝕣𝕞 pe ] 𝟎[ 𝟎-𝔽𝕣𝕞 pe ]) holds
t = transport
(λ - → is-top (𝟎-𝔽𝕣𝕞 pe) - holds)
(𝟎-left-unit-of-∨ (𝟎-𝔽𝕣𝕞 pe) 𝟏[ 𝟎-𝔽𝕣𝕞 pe ] ⁻¹)
(𝟏-is-top (𝟎-𝔽𝕣𝕞 pe))
c : closed-under-binary-meets (𝟎-𝔽𝕣𝕞 pe) ℬ𝟎↑ holds
c = directify-preserves-closure-under-∧
(𝟎-𝔽𝕣𝕞 pe)
ℬ𝟎
ℬ𝟎-is-basis-for-𝟎
ℬ𝟎-is-closed-under-binary-meets
γ : closed-under-finite-meets (𝟎-𝔽𝕣𝕞 pe) ℬ𝟎↑ holds
γ = ∣ (inr ⋆ ∷ []) , t ∣ , c
\end{code}