Ayberk Tosun, 11 September 2023

\begin{code}[hide]

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

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

module Locales.CharacterisationOfContinuity (pt : propositional-truncations-exist)
                                            (fe : Fun-Ext)                          where

open import Locales.Frame               pt fe
open import UF.Logic
open import Slice.Family
open import Locales.Compactness.Definition pt fe
open import Locales.Spectrality.SpectralLocale pt fe
open import Locales.Spectrality.Properties     pt fe

open PropositionalTruncation pt
open Existential pt
open Universal fe
open Implication fe
open Conjunction

open Locale

\end{code}

\begin{code}

continuity-condition : (Y : Locale 𝓀 π“₯ 𝓦) (X : Locale 𝓀' π“₯' 𝓦)
                     β†’ (⟨ π’ͺ Y ⟩ β†’ ⟨ π’ͺ X ⟩) β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺ βŠ” 𝓀' βŠ” π“₯')
continuity-condition Y X h =
 β±― b κž‰ ⟨ π’ͺ X ⟩ , β±― x κž‰ ⟨ π’ͺ Y ⟩ , is-compact-open X b β‡’
  b ≀[ poset-of (π’ͺ X) ] h x β‡’
   (Ǝ a κž‰ ⟨ π’ͺ Y ⟩ , (is-compact-open Y a ∧ (a ≀y x) ∧ (b ≀ₓ h a)) holds)
    where
     open PosetNotation (poset-of (π’ͺ X)) renaming (_≀_ to _≀ₓ_)
     open PosetNotation (poset-of (π’ͺ Y)) renaming (_≀_ to _≀y_)

\end{code}

\begin{code}

characterisation-of-continuity : (Y : Locale 𝓀  π“₯  𝓦)
                               β†’ (X : Locale 𝓀' π“₯' 𝓦)
                               β†’ is-spectral X holds
                               β†’ (h : ⟨ π’ͺ Y ⟩ β†’ ⟨ π’ͺ X ⟩)
                               β†’ is-monotonic (poset-of (π’ͺ Y)) (poset-of (π’ͺ X)) h holds
                               β†’ continuity-condition Y X h holds
                               β†’ is-scott-continuous (π’ͺ Y) (π’ͺ X) h holds
characterisation-of-continuity Y X Οƒ h ΞΌ ΞΆ S Ξ΄ = Ξ² , Ξ³
 where
  open PosetReasoning (poset-of (π’ͺ X))
  open Joins (Ξ» x y β†’ x ≀[ poset-of (π’ͺ X) ] y)

  Ξ² : (h (⋁[ (π’ͺ Y) ] S) is-an-upper-bound-of ⁅ h s ∣ s Ξ΅ S ⁆) holds
  Ξ² i = ΞΌ (S [ i ] , ⋁[ (π’ͺ Y) ] S) (⋁[ (π’ͺ Y) ]-upper S i)

  Ξ³ : (β±― (u , _) κž‰ upper-bound ⁅ h s ∣ s Ξ΅ S ⁆ ,
        h (⋁[ (π’ͺ Y) ] S) ≀[ poset-of (π’ͺ X) ] u) holds
  Ξ³ (u , Ο†) = spectral-yoneda X Οƒ (h (⋁[ π’ͺ Y ] S)) u †
   where
    † : ((K , _) : 𝒦 X)
      β†’ (K ≀[ poset-of (π’ͺ X) ] h (⋁[ π’ͺ Y ] S) β‡’ K  ≀[ poset-of (π’ͺ X) ] u) holds
    † (K , ΞΊ) p = βˆ₯βˆ₯-rec
                   (holds-is-prop (K ≀[ poset-of (π’ͺ X) ] u))
                   ‑
                   (ΞΆ K (⋁[ (π’ͺ Y) ] S) ΞΊ p)
      where
       ‑ : _ β†’ (K ≀[ poset-of (π’ͺ X) ] u) holds
       ‑ (a , κₐ , q , r) =
         K                        β‰€βŸ¨ r                                    ⟩
         h a                      β‰€βŸ¨ β™                                     ⟩
         ⋁[ (π’ͺ X) ] ⁅ h s ∣ s Ξ΅ S ⁆   β‰€βŸ¨ ⋁[ (π’ͺ X) ]-least ⁅ h s ∣ s Ξ΅ S ⁆ (u , Ο†) ⟩
         u                        β– 
          where
           ♣ : (Ξ£ i κž‰ index S , (a ≀[ poset-of (π’ͺ Y) ] (S [ i ])) holds)
             β†’ (h a ≀[ poset-of (π’ͺ X) ] (⋁[ (π’ͺ X) ] ⁅ h s ∣ s Ξ΅ S ⁆)) holds
           ♣ (i , ψ) = h a                    β‰€βŸ¨ ΞΌ (a , S [ i ]) ψ               ⟩
                       h (S [ i ])            β‰€βŸ¨ ⋁[ (π’ͺ X) ]-upper ⁅ h s ∣ s Ξ΅ S ⁆ i  ⟩
                       ⋁[ (π’ͺ X) ] ⁅ h s ∣ s Ξ΅ S ⁆ β– 

           β™  : (h a ≀[ poset-of (π’ͺ X) ] (⋁[ (π’ͺ X) ] ⁅ h s ∣ s Ξ΅ S ⁆)) holds
           β™  = βˆ₯βˆ₯-rec
                (holds-is-prop (h a ≀[ poset-of (π’ͺ X) ] (⋁[ (π’ͺ X) ] ⁅ h s ∣ s Ξ΅ S ⁆)))
                ♣
                (κₐ S Ξ΄ q)

\end{code}