--------------------------------------------------------------------------------
author:         Ayberk Tosun
date-started:   2024-03-15
date-completed: 2024-05-13
--------------------------------------------------------------------------------

Let D be a Scott domain satisfying the condition that the existence of binary
upper bounds of compact elements is decidable. Denote by Οƒ(D) the Scott locale
of domain D.

By a β€œpoint” of D, we mean a continuous map 𝟏 β†’ Οƒ(D) (where 𝟏 denotes the
terminal locale), or equivalently, a frame homomorphism π’ͺ(Οƒ(D)) β†’ Ξ©.

Given a point F, we define the family of compact elements with principal filters
falling in F, i.e.

  { c : 𝒦(D) ∣ ↑c ∈ F }.

The notation 𝒦(D) above is our notation for the type of compact elements of
the domain.

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc
open import UF.Size
open import UF.Subsingletons

module Locales.LawsonLocale.CompactElementsOfPoint
        (𝓀  : Universe)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
        (pt : propositional-truncations-exist)
        (sr : Set-Replacement pt)
       where

open import DomainTheory.BasesAndContinuity.Bases pt fe 𝓀
open import DomainTheory.BasesAndContinuity.ScottDomain      pt fe 𝓀
open import DomainTheory.Basics.Dcpo pt fe 𝓀 renaming (⟨_⟩ to ⟨_βŸ©βˆ™)
open import DomainTheory.Basics.WayBelow pt fe 𝓀
open import DomainTheory.Topology.ScottTopology pt fe 𝓀
open import DomainTheory.Topology.ScottTopologyProperties pt fe 𝓀
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 Locales.ScottLocale.Definition pt fe 𝓀
open import Locales.ScottLocale.Properties pt fe 𝓀
open import Locales.ScottLocale.ScottLocalesOfScottDomains pt fe sr 𝓀
open import Locales.Point.Definition pt fe
open import Locales.Point.Properties pt fe 𝓀 pe hiding (𝟏L)
open import Locales.TerminalLocale.Properties pt fe sr
open import Slice.Family
open import UF.Logic
open import UF.Powerset
open import UF.SubtypeClassifier renaming (βŠ₯ to βŠ₯β‚š)
open import UF.Univalence

open AllCombinators pt fe renaming (_∧_ to _βˆ§β‚š_; _∨_ to _βˆ¨β‚š_)
open FrameHomomorphismProperties
open FrameHomomorphisms
open Locale
open PropositionalTruncation pt hiding (_∨_)

\end{code}

We work in a module parameterized by a large and locally small locale `X`.

\begin{code}

module Preliminaries (X : Locale (𝓀 ⁺) 𝓀 𝓀) where

 open ContinuousMaps

\end{code}

We use the abbreviation `𝟏L` for the terminal locale of the category of
`𝓀`-locales (i.e. large and locally small locales over universe `𝓀`).

\begin{code}

 𝟏L : Locale (𝓀 ⁺) 𝓀 𝓀
 𝟏L = 𝟏Loc pe

\end{code}

This is the locale given by the frame of opens `Ξ©βˆ™`.

\begin{code}

 Ξ©βˆ™ : Frame (𝓀 ⁺) 𝓀 𝓀
 Ξ©βˆ™ = π’ͺ (𝟏Loc pe)

\end{code}

For the reader who might not be familiar, this is the locale defined by the
frame of opens `Ξ©`.

\begin{code}

 _ : ⟨ π’ͺ 𝟏L ⟩ ＝ Ξ© 𝓀
 _ = refl

\end{code}

By a point of locale, we mean a continuous map from `𝟏L` into `X` as mentioned
in the preamble.

\begin{code}

 Point : 𝓀 ⁺  Μ‡
 Point = 𝟏L ─cβ†’  X

\end{code}

This is definitionally the same thing as a frame homomorphism `π’ͺ(X) β†’ Ξ©`.

\begin{code}

 Pointβ€² : 𝓀 ⁺  Μ‡
 Pointβ€² = π’ͺ X ─fβ†’ Ξ©βˆ™

 _ : Point ＝ Pointβ€²
 _ = refl

\end{code}

We now proceed to the definition of the family mentioned in the preamble. We
work with a dcpo `𝓓` that is assumed to

  - have a bottom element,
  - be a Scott domain, and
  - satisfy the aforementioned decidability condition for upper boundedness.

\begin{code}

open DefinitionOfScottDomain

module Construction
        (𝓓    : DCPO {𝓀 ⁺} {𝓀})
        (ua   : Univalence)
        (hl   : has-least (underlying-order 𝓓))
        (sd   : is-scott-domain 𝓓 holds)
        (dc   : decidability-condition 𝓓) where

 open SpectralScottLocaleConstructionβ‚‚ 𝓓 ua hl sd dc pe
 open SpectralScottLocaleConstruction 𝓓 hl hscb dc bc pe hiding (scb; Ξ²; ϟ)
 open DefnOfScottTopology 𝓓 𝓀

 open Preliminaries σ⦅𝓓⦆
 open Properties 𝓓

\end{code}

We denote by `B𝓓` the basis of `𝓓`.

\begin{code}

 B𝓓 : Fam 𝓀 ⟨ 𝓓 βŸ©βˆ™
 B𝓓 = index-of-compact-basis 𝓓 hscb , family-of-compact-elements 𝓓 hscb

\end{code}

We use the abbreviation `scb` for the proof that `B𝓓` is a small basis
consisting of compact opens.

\begin{code}

 scb : is-small-compact-basis 𝓓 (family-of-compact-elements 𝓓 hscb)
 scb = small-compact-basis 𝓓 hscb

\end{code}

By `Ξ²β‚– i`, we denote the element denoted by an index `i`, packaged up with the
proof that it is compact.

\begin{code}

 open is-small-compact-basis scb
 open BottomLemma 𝓓 𝕒 hl

 Ξ²β‚– : (i : index B𝓓) β†’ Ξ£ c κž‰ ⟨ 𝓓 βŸ©βˆ™ , is-compact 𝓓 c
 Ξ²β‚– i = B𝓓 [ i ] , basis-is-compact i

\end{code}

We now write down the family of compact elements whose principal ideals fall in
a given point `β„±`. We denote this `𝒦-in-point β„±`.

\begin{code}

 𝒦-in-point : Point β†’ Fam 𝓀 ⟨ 𝓓 βŸ©βˆ™
 𝒦-in-point (F , _) =
  ⁅ B𝓓 [ i ] ∣ (i , _) ∢ (Ξ£ i κž‰ index B𝓓 , ↑˒[ Ξ²β‚– i ] βˆˆβ‚š F holds) ⁆

\end{code}

Ideally, the name here would be `𝒦-with-principal-ideals-in-point` but this is
too long, which is why we use the name `𝒦-in-point`.

It makes sense to me to think of this as the family of compact approximants to
the given point, but I'm not sure this geometric view is accurate at the time of
writing. I will improve this name in the future as my understanding of the
underlying geometric intuition increases.

The family `𝒦-in-point` is always inhabited.

\begin{code}

 open ScottLocaleProperties 𝓓 hl hscb pe

 𝒦-in-point-is-inhabited
  : (β„±@(F , _) : Point)
  β†’ is-inhabited (underlying-order 𝓓) (index (𝒦-in-point β„±))
 𝒦-in-point-is-inhabited β„±@(F , _) = βˆ₯βˆ₯-rec βˆƒ-is-prop † Ξ³
  where
   β…’ : F 𝟏[ π’ͺ σ⦅𝓓⦆ ] ＝ ⊀
   β…’ = frame-homomorphisms-preserve-top (π’ͺ σ⦅𝓓⦆) (π’ͺ 𝟏L) β„±

   ΞΆ : 𝟏[ π’ͺ σ⦅𝓓⦆ ] ∈ F
   ΞΆ = equal-⊀-gives-holds (F 𝟏[ π’ͺ σ⦅𝓓⦆ ]) β…’

   † : Ξ£ i κž‰ index B𝓓 , B𝓓 [ i ] ＝ βŠ₯α΄° β†’ βˆƒ i κž‰ index B𝓓 , ↑˒[ Ξ²β‚– i ] βˆˆβ‚š F holds
   † (i , p) = ∣ i , equal-⊀-gives-holds (F ↑˒[ Ξ²β‚– i ]) β€» ∣
    where
     β…  = ap
          F
          (to-subtype-＝
            (holds-is-prop ∘ is-scott-open)
            (ap (principal-filter 𝓓) p))
     β…‘ = ap F ↑βŠ₯-is-top

     β€» : F ↑˒[ Ξ²β‚– i ] ＝ ⊀
     β€» = F ↑˒[ Ξ²β‚– i ]    ＝⟨ β…  ⟩
         F ↑˒[ βŠ₯α΄° , βŠ₯ΞΊ ] ＝⟨ β…‘ ⟩
         F 𝟏[ π’ͺ σ⦅𝓓⦆ ]   ＝⟨ β…’ ⟩
         ⊀               ∎

   Ξ³ : βˆƒ i κž‰ index B𝓓 , B𝓓 [ i ] ＝ βŠ₯α΄°
   Ξ³ = small-compact-basis-contains-all-compact-elements 𝓓 (B𝓓 [_]) scb βŠ₯α΄° βŠ₯ΞΊ

\end{code}

Before we proceed to proving that the family `𝒦-in-point` is always
semidirected, we prove a lemma that we will use in the proof. The reader not
interested in the lemma may jump directly to the proof which is implemented in
the function called `𝒦-in-point-is-semidirected`.

The lemma is simply the fact that
```
    ↑b ∈ F and ↑c ∈ F    implies    (↑b ∧ ↑c) ∈ F
```
for any two compact elements `b` and `c` of `𝓓`.

This is actually something already implemented in the `Locales.Point` directory,
where it is shown that points correspond to completely prime filters.

\begin{code}

 point-preserves-meets : (β„±@(F , _) : Point) (c d : ⟨ 𝓓 βŸ©βˆ™)
                       β†’ (ΞΊc : is-compact 𝓓 c)
                       β†’ (ΞΊd : is-compact 𝓓 d)
                       β†’ (F ↑˒[ (c , ΞΊc) ]
                       β‡’ F ↑˒[ (d , ΞΊd) ]
                       β‡’ F (↑˒[ c , ΞΊc ] ∧[ π’ͺ Σ⦅𝓓⦆ ] ↑˒[ d , ΞΊd ])) holds
 point-preserves-meets β„±@(F , _) c d ΞΊc ΞΊd =
  point-is-closed-under-∧ ↑˒[ c , ΞΊc ] ↑˒[ d , ΞΊd ]
   where
    open DefnOfCPF Σ⦅𝓓⦆
    open Pointα΅£ (to-pointα΅£ Σ⦅𝓓⦆ (𝔰 Σ⦅𝓓⦆ β„±))

\end{code}

The family `𝒦-in-point` is semidirected.

\begin{code}

 𝒦-in-point-is-semidirected
  : (β„± : Point)
  β†’ is-semidirected (underlying-order 𝓓) (𝒦-in-point β„± [_])
 𝒦-in-point-is-semidirected β„± (i , ΞΊα΅’) (j , ΞΊβ±Ό) =

\end{code}

To prove this, we use the assumption that upper boundedness of compact elements
is decidable.

\begin{code}

  let
   Ο‘ : is-decidable (bounded-above 𝓓 (B𝓓 [ i ]) (B𝓓 [ j ]) holds)
   Ο‘ = dc (B𝓓 [ i ]) (B𝓓 [ j ]) (basis-is-compact i) (basis-is-compact j)
  in

\end{code}

We now proceed by case analysis on whether or not the upper bound of `B𝓓 [ i ]`
and `B𝓓 [ j ]` exists. The cases are given in `case₁` and `caseβ‚‚`.

\begin{code}

  cases case₁ caseβ‚‚ Ο‘
   where
    open DefnOfScottLocale 𝓓 𝓀 pe

    F = pr₁ β„±

\end{code}

We denote by `b` and `c`, the elements `B𝓓 [ i ]` and `B𝓓 [ j ]` respectively.

\begin{code}

    b  = B𝓓 [ i ]
    κᡇ = basis-is-compact i
    c  = B𝓓 [ j ]
    κᢜ = basis-is-compact j

\end{code}

We now proceed with the case analysis.

Case 1: the upper bound of `b` and `c` exists.

\begin{code}

    case₁ : bounded-above 𝓓 (B𝓓 [ i ]) (B𝓓 [ j ]) holds
          β†’ βˆƒ k κž‰ index (𝒦-in-point β„±)
                , (𝒦-in-point β„± [ i , ΞΊα΅’ ]) βŠ‘βŸ¨ 𝓓 ⟩ (𝒦-in-point β„± [ k ])
                Γ— (𝒦-in-point β„± [ j , ΞΊβ±Ό ]) βŠ‘βŸ¨ 𝓓 ⟩ (𝒦-in-point β„± [ k ])
    case₁ Ο… = βˆ₯βˆ₯-functor ‑₁ π’·α΅ˆ
     where
      π“ˆ : has-sup (underlying-order 𝓓) (binary-family 𝓀 b c [_])
      π“ˆ = bc (binary-family 𝓀 b c) Ο…

\end{code}

Thanks to bounded completeness, the fact that an upper bound exists means that
the least upper bound exists. We denote this by `d`.

\begin{code}

      d : ⟨ 𝓓 βŸ©βˆ™
      d = pr₁ π“ˆ

      p : b βŠ‘βŸ¨ 𝓓 ⟩ d
      p = pr₁ (prβ‚‚ π“ˆ) (inl ⋆)

      q : c βŠ‘βŸ¨ 𝓓 ⟩ d
      q = pr₁ (prβ‚‚ π“ˆ) (inr ⋆)

      κᡈ : is-compact 𝓓 d
      κᡈ = sup-is-compact b c d κᡇ κᢜ (prβ‚‚ π“ˆ)

      π’·α΅ˆ : (d ∈imageβ‚š (B𝓓 [_])) holds
      π’·α΅ˆ = small-compact-basis-contains-all-compact-elements 𝓓 (B𝓓 [_]) scb d κᡈ

      ‑₁ : Ξ£ k κž‰ index B𝓓 , B𝓓 [ k ] ＝ d
         β†’ Ξ£ k κž‰ index (𝒦-in-point β„±) ,
                 ((𝒦-in-point β„± [ i , ΞΊα΅’ ]) βŠ‘βŸ¨ 𝓓 ⟩ (B𝓓 [ pr₁ k ]))
               Γ— ((𝒦-in-point β„± [ j , ΞΊβ±Ό ]) βŠ‘βŸ¨ 𝓓 ⟩ (B𝓓 [ pr₁ k ]))
      ‑₁ (k , ψ) = (k , β€») , β™  , ♣
       where
        r : ↑˒[ d , κᡈ ] ＝ ↑˒[ b , κᡇ ] ∧[ π’ͺ Ξ£[𝓓] ] ↑˒[ c , κᢜ ]
        r = principal-filter-reflects-joins b c d κᡇ κᢜ (prβ‚‚ π“ˆ)

        β™₯ : ↑˒[ d , κᡈ ] ∈ F
        β™₯ = transport
             (Ξ» - β†’ - ∈ F)
             (r ⁻¹)
             (point-preserves-meets β„± b c κᡇ κᢜ ΞΊα΅’ ΞΊβ±Ό)

        β€» : ↑˒[ Ξ²β‚– k ] ∈ F
        β€» = transport
             (Ξ» - β†’ ↑˒[ - ] ∈ F)
             (to-subtype-＝ (being-compact-is-prop 𝓓) (ψ ⁻¹))
             β™₯

        -- Seems to be necessary for the termination of typechecking within a
        -- reasonable time
        abstract
         β™  : (B𝓓 [ i ]) βŠ‘βŸ¨ 𝓓 ⟩ (B𝓓 [ k ])
         β™  = transport (Ξ» - β†’ (B𝓓 [ i ]) βŠ‘βŸ¨ 𝓓 ⟩ -) (ψ ⁻¹) p

         ♣ : (B𝓓 [ j ]) βŠ‘βŸ¨ 𝓓 ⟩ (B𝓓 [ k ])
         ♣ = transport (Ξ» - β†’ (B𝓓 [ j ]) βŠ‘βŸ¨ 𝓓 ⟩ -) (ψ ⁻¹) q

\end{code}

Case 2: the upper bound of `b` and `c` _does not_ exist. We derive a
contradiction in this case.

\begin{code}

    caseβ‚‚ : Β¬ ((B𝓓 [ i ]) ↑[ 𝓓 ] (B𝓓 [ j ]) holds)
          β†’ βˆƒ k κž‰ index (𝒦-in-point β„±)
                , (𝒦-in-point β„± [ i , ΞΊα΅’ ]) βŠ‘βŸ¨ 𝓓 ⟩ (𝒦-in-point β„± [ k ])
                Γ— (𝒦-in-point β„± [ j , ΞΊβ±Ό ]) βŠ‘βŸ¨ 𝓓 ⟩ (𝒦-in-point β„± [ k ])
    caseβ‚‚ Ξ½ = 𝟘-elim (βŠ₯-is-not-⊀ ϟ)
     where

\end{code}

We have that `↑(b) ∧ ↑(c) ＝ 𝟎`, given by `not-bounded-lemma`.

\begin{code}

      Ξ² : ↑˒[ b , κᡇ ] ∧[ π’ͺ Σ⦅𝓓⦆ ] ↑˒[ c , κᢜ ] ＝ 𝟎[ π’ͺ Σ⦅𝓓⦆ ]
      Ξ² = not-bounded-lemma b c κᡇ κᢜ Ξ½

\end{code}

Because the point `F` is a frame homomorphism, we have that

```
  F(↑b) ∧ F(↑c) ＝ F(↑b ∧ ↑c) ＝ F(𝟎)
```

Because we know that `F(↑b)` and `F(↑c)` hold, we know that `F(𝟎)` holds, which
is a contradiction since `F(𝟎) ＝ βŠ₯`.

\begin{code}

      β…  = 𝟎-is-βŠ₯ pe
      β…‘ = frame-homomorphisms-preserve-bottom (π’ͺ Σ⦅𝓓⦆) (𝟎-π”½π•£π•ž pe) β„± ⁻¹
      β…’ = ap F (Ξ² ⁻¹)
      β…£ = holds-gives-equal-⊀
           pe
           fe
           (F (↑˒[ b , κᡇ ] ∧[ π’ͺ Σ⦅𝓓⦆ ] ↑˒[ c , κᢜ ]))
           (point-preserves-meets β„± b c κᡇ κᢜ ΞΊα΅’ ΞΊβ±Ό)

      ϟ : βŠ₯β‚š ＝ ⊀
      ϟ = βŠ₯β‚š                                          ＝⟨ β…  ⟩
          𝟎[ 𝟎-π”½π•£π•ž pe ]                               ＝⟨ β…‘ ⟩
          F 𝟎[ π’ͺ Σ⦅𝓓⦆ ]                               ＝⟨ β…’ ⟩
          F (↑˒[ b , κᡇ ] ∧[ π’ͺ Σ⦅𝓓⦆ ] ↑˒[ c , κᢜ ])   ＝⟨ β…£ ⟩
          ⊀                                           ∎

\end{code}

We now have everything required to record the proof that the family
`𝒦-in-point β„±` is directed.

\begin{code}

 𝒦-in-point-is-directed : (β„± : Point)
                        β†’ is-directed (underlying-order 𝓓) (𝒦-in-point β„± [_])
 𝒦-in-point-is-directed β„± = 𝒦-in-point-is-inhabited β„±
                          , 𝒦-in-point-is-semidirected β„±

\end{code}

Added on 2024-05-23.

\begin{code}

 𝒦-in-point↑ : (β„± : Point) β†’ Fam↑
 𝒦-in-point↑ β„± = 𝒦-in-point β„± , 𝒦-in-point-is-directed β„±

\end{code}