Ayberk Tosun, 11 September 2023

\begin{code}

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

open import MLTT.Spartan hiding (𝟚)
open import UF.PropTrunc
open import UF.FunExt
open import UF.UA-FunExt
open import UF.Size

module Locales.StoneImpliesSpectral (pt : propositional-truncations-exist)
                                    (fe : Fun-Ext)
                                    (sr : Set-Replacement pt) where

\end{code}

Importation of foundational UF stuff.

\begin{code}

open import Slice.Family
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.Logic

open AllCombinators pt fe
open PropositionalTruncation pt

\end{code}

Importations of other locale theory modules.

\begin{code}

open import Locales.AdjointFunctorTheoremForFrames
open import Locales.Frame            pt fe
open import Locales.WayBelowRelation.Definition pt fe
open import Locales.Compactness      pt fe
open import Locales.Complements      pt fe
open import Locales.GaloisConnection pt fe
open import Locales.InitialFrame     pt fe
open import Locales.Spectrality.SpectralLocale pt fe
open import Locales.ZeroDimensionality pt fe sr
open import Locales.Stone              pt fe sr
open import Locales.SmallBasis         pt fe sr
open import Locales.Clopen             pt fe sr
open import Locales.WellInside         pt fe sr
open import Locales.ScottContinuity    pt fe sr

open Locale

\end{code}

The well inside relation implies the way below relation.

\begin{code}

⋜₀-implies-≪-in-compact-frames : (X : Locale 𝓤 𝓥 𝓦)
                               → is-compact X holds
                               → (U V : ⟨ 𝒪 X ⟩)
                               → U ⋜₀[ 𝒪 X ] V
                               → (U ≪[ 𝒪 X ] V) holds
⋜₀-implies-≪-in-compact-frames {𝓦 = 𝓦} X κ U V (W , c₁ , c₂) S d q =
 ∥∥-rec ∃-is-prop θ ζ
  where
   F = 𝒪 X
   open PosetNotation  (poset-of (𝒪 X))
   open PosetReasoning (poset-of (𝒪 X))

   T : Fam 𝓦 ⟨ 𝒪 X ⟩
   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 (𝒪 X) 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 ⁆  ■

   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 ∣

   T-is-directed : (is-directed 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) η

\end{code}

\begin{code}

⋜-implies-≪-in-compact-frames : (X : Locale 𝓤 𝓥 𝓦)
                              → is-compact X holds
                              → (U V : ⟨ 𝒪 X ⟩)
                              → (U ⋜[ 𝒪 X ] V ⇒ U ≪[ 𝒪 X ] V) holds
⋜-implies-≪-in-compact-frames X κ U V =
 ∥∥-rec (holds-is-prop (U ≪[ 𝒪 X ] V)) (⋜₀-implies-≪-in-compact-frames X κ U V)

\end{code}

Clopens are compact in compact locales.

\begin{code}

clopens-are-compact-in-compact-locales : (X : Locale 𝓤 𝓥 𝓦)
                                       → is-compact X holds
                                       → (U : ⟨ 𝒪 X ⟩)
                                       → (is-clopen (𝒪 X) U
                                       ⇒  is-compact-open X U) holds
clopens-are-compact-in-compact-locales X κ U =
 ⋜₀-implies-≪-in-compact-frames X κ U U

\end{code}

Clopens are basic in compact locales.

\begin{code}

clopens-are-basic : (X : Locale 𝓤 𝓥 𝓦) (st : stoneᴰ X)
                  → (𝒷 : directed-basisᴰ (𝒪 X))
                  → (K : ⟨ 𝒪 X ⟩)
                  → (is-clopen (𝒪 X) K ⇒ is-basic X K 𝒷) holds
clopens-are-basic X (κ , _) 𝒷 K 𝕔 =
 compact-opens-are-basic X 𝒷 K (clopens-are-compact-in-compact-locales X κ K 𝕔)

\end{code}

\begin{code}

stoneᴰ-implies-spectralᴰ : (X : Locale 𝓤 𝓥 𝓦) → stoneᴰ X → spectralᴰ X
stoneᴰ-implies-spectralᴰ {_} {_} {𝓦} X (κₓ , zdₓ) = ℬ , β , κ , μ
 where
  open Joins (λ x y → x ≤[ poset-of (𝒪 X) ] y)

  ℬ : Fam 𝓦 ⟨ 𝒪 X ⟩
  ℬ = basis-zd (𝒪 X) zdₓ

  φ : consists-of-clopens (𝒪 X) ℬ holds
  φ = basis-zd-consists-of-clopens (𝒪 X) zdₓ

  β : directed-basis-forᴰ (𝒪 X) ℬ
  β U = cover-index-zd (𝒪 X) zdₓ U , † , d
   where
    𝒥 : Fam 𝓦 (index ℬ)
    𝒥 = cover-index-zd (𝒪 X) zdₓ U

    † : (U is-lub-of ⁅ ℬ [ j ] ∣ j ε 𝒥 ⁆) holds
    † = basis-zd-covers-do-cover (𝒪 X) zdₓ U

    d : is-directed (𝒪 X) ⁅ ℬ [ j ] ∣ j ε 𝒥 ⁆ holds
    d = basis-zd-covers-are-directed (𝒪 X) zdₓ U

  X-is-compact : is-compact X holds
  X-is-compact =
   clopens-are-compact-in-compact-locales X κₓ 𝟏[ 𝒪 X ] (𝟏-is-clopen (𝒪 X))

  κ : consists-of-compact-opens X ℬ holds
  κ i = clopens-are-compact-in-compact-locales X κₓ (ℬ [ i ]) 𝕔
   where
    𝕔 : is-clopen (𝒪 X) (ℬ [ i ]) holds
    𝕔 = basis-zd-consists-of-clopens (𝒪 X) zdₓ i

  μ₀ : contains-top (𝒪 X) ℬ holds
  μ₀ = ∥∥-rec
        (holds-is-prop (contains-top (𝒪 X) ℬ))
        (λ { (j , p) → ∣ j , transport (λ - → is-top (𝒪 X) - holds) (p ⁻¹) (𝟏-is-top (𝒪 X)) ∣ })
        (clopens-are-basic X (κₓ , zdₓ) (ℬ , β) 𝟏[ 𝒪 X ] (𝟏-is-clopen (𝒪 X)))

  open Meets (λ x y → x ≤[ poset-of (𝒪 X) ] y)

  μ₂ : closed-under-binary-meets (𝒪 X) ℬ holds
  μ₂ i j = ∥∥-rec ∃-is-prop † ξ
   where
    ν : is-clopen (𝒪 X) (ℬ [ i ] ∧[ 𝒪 X ] ℬ [ j ]) holds
    ν = clopens-are-closed-under-∧ (𝒪 X) (ℬ [ i ]) (ℬ [ j ]) (φ i) (φ j)

    ξ : is-basic X (ℬ [ i ] ∧[ 𝒪 X ] ℬ [ j ]) (ℬ , β) holds
    ξ = clopens-are-basic X (κₓ , zdₓ) (ℬ , β) (ℬ [ i ] ∧[ 𝒪 X ] ℬ [ j ]) ν

    † : Σ k ꞉ index ℬ , ℬ [ k ] ＝ ℬ [ i ] ∧[ 𝒪 X ] ℬ [ j ]
      → (Ǝ k ꞉ index ℬ , ((ℬ [ k ]) is-glb-of (ℬ [ i ] , ℬ [ j ])) holds) holds
    † (k , p) = ∣ k , ∧[ 𝒪 X ]-is-glb⋆ p ∣

  μ : closed-under-finite-meets (𝒪 X) ℬ holds
  μ = μ₀ , μ₂

\end{code}

`stoneᴰ X` implies that `X` is spectral.

\begin{code}

stone-locales-are-spectral : (X : Locale 𝓤 𝓥 𝓦) → stoneᴰ X → is-spectral X holds
stone-locales-are-spectral X σ@(κ , ζ) = spectralᴰ-gives-spectrality X σᴰ
 where
  σᴰ : spectralᴰ X
  σᴰ = stoneᴰ-implies-spectralᴰ X σ

\end{code}
