---
title:          Distributive lattice of compact opens
author:         Ayberk Tosun
date-started:   2024-02-24
date-completed: 2024-02-27
dates-updated:  [2024-04-30]
---

\begin{code}

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.Logic
open import UF.PropTrunc
open import UF.Size
open import UF.SubtypeClassifier
open import UF.UA-FunExt
open import UF.Univalence

module Locales.Spectrality.LatticeOfCompactOpens
        (ua : Univalence)
        (pt : propositional-truncations-exist)
        (sr : Set-Replacement pt)
       where

private
 fe : Fun-Ext
 fe {𝓀} {π“₯} = univalence-gives-funext' 𝓀 π“₯ (ua 𝓀) (ua (𝓀 βŠ” π“₯))

open import Locales.Compactness.Definition pt fe
open import Locales.DistributiveLattice.Definition fe pt
open import Locales.Frame pt fe
open import Locales.SmallBasis pt fe sr
open import Locales.Spectrality.SpectralLocale pt fe
open import UF.Equiv

open AllCombinators pt fe
open Locale
open PropositionalTruncation pt

\end{code}

We fix a large and locally small locale `X`, assumed to be spectral with a small
type of compact opens.

\begin{code}

module 𝒦-Lattice (X  : Locale (𝓀 ⁺) 𝓀 𝓀)
                 (Οƒβ‚€ : is-spectral-with-small-basis ua X holds) where

\end{code}

We define some shorthand notation to simplify the proofs.

\begin{code}

 Οƒ : is-spectral X holds
 Οƒ = ssb-implies-spectral ua X Οƒβ‚€

 𝟏-is-compact : is-compact-open X 𝟏[ π’ͺ X ] holds
 𝟏-is-compact = spectral-locales-are-compact X Οƒ

 πŸβ‚– : 𝒦 X
 πŸβ‚– = 𝟏[ π’ͺ X ] , 𝟏-is-compact

 πŸŽβ‚– : 𝒦 X
 πŸŽβ‚– = 𝟎[ π’ͺ X ] , 𝟎-is-compact X

\end{code}

We now construct the distributive lattice of compact opens.

\begin{code}

 𝒦⦅X⦆ : DistributiveLattice (𝓀 ⁺)
 𝒦⦅X⦆ =
  record
   { X               = 𝒦 X
   ; 𝟏               = πŸβ‚–
   ; 𝟎               = πŸŽβ‚–
   ; _∧_             = _βˆ§β‚–_
   ; _∨_             = _βˆ¨β‚–_
   ; X-is-set        = 𝒦-is-set X
   ; ∧-associative   = α
   ; ∧-commutative   = β
   ; ∧-unit          = γ
   ; ∧-idempotent    = δ
   ; ∧-absorptive    = ϡ
   ; ∨-associative   = ΢
   ; ∨-commutative   = η
   ; ∨-unit          = θ
   ; ∨-idempotent    = ι
   ; ∨-absorptive    = μ
   ; distributivityᡈ = ν
  }
    where
     open OperationsOnCompactOpens X Οƒ

\end{code}

The compact opens obviously satisfy all the distributive lattice laws, since
every frame is a distributive lattice. Because the opens in consideration are
packaged up with their proofs of compactness though, we need to lift these laws
to the subtype consisting of compact opens. We take care of this bureaucracy
below.

\begin{code}

     Ξ± : (𝒦₁ 𝒦₂ 𝒦₃ : 𝒦 X) β†’ 𝒦₁ βˆ§β‚– (𝒦₂ βˆ§β‚– 𝒦₃) ＝ (𝒦₁ βˆ§β‚– 𝒦₂) βˆ§β‚– 𝒦₃
     Ξ± 𝒦₁@(K₁ , κ₁) 𝒦₂@(Kβ‚‚ , ΞΊβ‚‚) 𝒦₃@(K₃ , κ₃) = to-𝒦-＝ X ΞΊ ΞΊβ€² †
      where
       ΞΊ : is-compact-open X (K₁ ∧[ π’ͺ X ] (Kβ‚‚ ∧[ π’ͺ X ] K₃)) holds
       ΞΊ = binary-coherence X Οƒ _ _ κ₁ (binary-coherence X Οƒ Kβ‚‚ K₃ ΞΊβ‚‚ κ₃)

       ΞΊβ€² : is-compact-open X ((K₁ ∧[ π’ͺ X ] Kβ‚‚) ∧[ π’ͺ X ] K₃) holds
       ΞΊβ€² = binary-coherence X Οƒ _ _ (binary-coherence X Οƒ K₁ Kβ‚‚ κ₁ ΞΊβ‚‚) κ₃

       † : K₁ ∧[ π’ͺ X ] (Kβ‚‚ ∧[ π’ͺ X ] K₃) ＝ (K₁ ∧[ π’ͺ X ] Kβ‚‚) ∧[ π’ͺ X ] K₃
       † = ∧[ π’ͺ X ]-is-associative K₁ Kβ‚‚ K₃

     Ξ² : (𝒦₁ 𝒦₂ : 𝒦 X) β†’ 𝒦₁ βˆ§β‚– 𝒦₂ ＝ 𝒦₂ βˆ§β‚– 𝒦₁
     Ξ² (K₁ , κ₁) (Kβ‚‚ , ΞΊβ‚‚) = to-𝒦-＝
                              X
                              (binary-coherence X Οƒ K₁ Kβ‚‚ κ₁ ΞΊβ‚‚)
                              (binary-coherence X Οƒ Kβ‚‚ K₁ ΞΊβ‚‚ κ₁)
                              (∧[ π’ͺ X ]-is-commutative K₁ Kβ‚‚)

     Ξ³ : (𝒦 : 𝒦 X) β†’ 𝒦 βˆ§β‚– πŸβ‚– ＝ 𝒦
     Ξ³ (K , ΞΊ) = to-𝒦-＝
                  X
                  (binary-coherence X Οƒ K 𝟏[ π’ͺ X ] ΞΊ 𝟏-is-compact)
                  ΞΊ
                  (𝟏-right-unit-of-∧ (π’ͺ X) K)

     Ξ΄ : (𝒦 : 𝒦 X) β†’ 𝒦 βˆ§β‚– 𝒦 ＝ 𝒦
     Ξ΄ (K , ΞΊ) = to-𝒦-＝
                  X
                  (binary-coherence X Οƒ K K ΞΊ ΞΊ)
                  ΞΊ
                  (∧[ π’ͺ X ]-is-idempotent K ⁻¹ )

     Ο΅ : (𝒦₁ 𝒦₂ : 𝒦 X) β†’ 𝒦₁ βˆ§β‚– (𝒦₁ βˆ¨β‚– 𝒦₂) ＝ 𝒦₁
     Ο΅ (K₁ , κ₁) (Kβ‚‚ , ΞΊβ‚‚) = to-𝒦-＝ X ΞΊ κ₁ (absorptionα΅’α΅–-right (π’ͺ X) K₁ Kβ‚‚)
      where
       ΞΊ : is-compact-open X (K₁ ∧[ π’ͺ X ] (K₁ ∨[ π’ͺ X ] Kβ‚‚)) holds
       ΞΊ = binary-coherence
            X
            Οƒ
            K₁
            (K₁ ∨[ π’ͺ X ] Kβ‚‚)
            κ₁
            (compact-opens-are-closed-under-∨ X K₁ Kβ‚‚ κ₁ ΞΊβ‚‚)

     ΞΆ : (𝒦₁ 𝒦₂ 𝒦₃ : 𝒦 X) β†’ 𝒦₁ βˆ¨β‚– (𝒦₂ βˆ¨β‚– 𝒦₃) ＝ (𝒦₁ βˆ¨β‚– 𝒦₂) βˆ¨β‚– 𝒦₃
     ΞΆ 𝒦₁@(K₁ , κ₁) 𝒦₂@(Kβ‚‚ , ΞΊβ‚‚) 𝒦₃@(K₃ , κ₃) =
      to-𝒦-＝
       X
       (compact-opens-are-closed-under-∨ X K₁ (Kβ‚‚ ∨[ π’ͺ X ] K₃) κ₁ ΞΊ)
       (compact-opens-are-closed-under-∨ X (K₁ ∨[ π’ͺ X ] Kβ‚‚) K₃ ΞΊβ€² κ₃)
       (∨[ π’ͺ X ]-assoc K₁ Kβ‚‚ K₃ ⁻¹)
        where
         ΞΊ : is-compact-open X (Kβ‚‚ ∨[ π’ͺ X ] K₃) holds
         ΞΊ = compact-opens-are-closed-under-∨ X Kβ‚‚ K₃ ΞΊβ‚‚ κ₃

         ΞΊβ€² : is-compact-open X (K₁ ∨[ π’ͺ X ] Kβ‚‚) holds
         ΞΊβ€² = compact-opens-are-closed-under-∨ X K₁ Kβ‚‚ κ₁ ΞΊβ‚‚

     Ξ· : (𝒦₁ 𝒦₂ : 𝒦 X) β†’ 𝒦₁ βˆ¨β‚– 𝒦₂ ＝ 𝒦₂ βˆ¨β‚– 𝒦₁
     Ξ· 𝒦₁@(K₁ , κ₁) 𝒦₂@(Kβ‚‚ , ΞΊβ‚‚) =
      to-𝒦-＝
       X
       (compact-opens-are-closed-under-∨ X K₁ Kβ‚‚ κ₁ ΞΊβ‚‚)
       (compact-opens-are-closed-under-∨ X Kβ‚‚ K₁ ΞΊβ‚‚ κ₁)
       (∨[ π’ͺ X ]-is-commutative K₁ Kβ‚‚)

     ΞΈ : (𝒦 : 𝒦 X) β†’ 𝒦 βˆ¨β‚– (𝟎[ π’ͺ X ] , 𝟎-is-compact X) ＝ 𝒦
     ΞΈ (K , ΞΊ) =
      to-𝒦-＝
       X
       (compact-opens-are-closed-under-∨ X K 𝟎[ π’ͺ X ] ΞΊ (𝟎-is-compact X))
       ΞΊ
       (𝟎-left-unit-of-∨ (π’ͺ X) K)

     ΞΉ : (𝒦 : 𝒦 X) β†’ 𝒦 βˆ¨β‚– 𝒦 ＝ 𝒦
     ΞΉ (K , ΞΊ) = to-𝒦-＝
                  X
                  (compact-opens-are-closed-under-∨ X K K κ κ)
                  ΞΊ
                  (∨[ π’ͺ X ]-is-idempotent K ⁻¹)

     ΞΌ : (𝒦₁ 𝒦₂ : 𝒦 X) β†’ 𝒦₁ βˆ¨β‚– (𝒦₁ βˆ§β‚– 𝒦₂) ＝ 𝒦₁
     ΞΌ 𝒦₁@(K₁ , κ₁) 𝒦₂@(Kβ‚‚ , ΞΊβ‚‚) =
      to-𝒦-＝
       X
       (compact-opens-are-closed-under-∨ X K₁ (K₁ ∧[ π’ͺ X ] Kβ‚‚) κ₁ ΞΊ)
       κ₁
       (absorption-right (π’ͺ X) K₁ Kβ‚‚)
        where
         ΞΊ : is-compact-open X (K₁ ∧[ π’ͺ X ] Kβ‚‚) holds
         ΞΊ = binary-coherence X Οƒ K₁ Kβ‚‚ κ₁ ΞΊβ‚‚

     Ξ½ : (𝒦₁ 𝒦₂ 𝒦₃ : 𝒦 X) β†’ 𝒦₁ βˆ§β‚– (𝒦₂ βˆ¨β‚– 𝒦₃) ＝ (𝒦₁ βˆ§β‚– 𝒦₂) βˆ¨β‚– (𝒦₁ βˆ§β‚– 𝒦₃)
     Ξ½ 𝒦₁@(K₁ , κ₁) 𝒦₂@(Kβ‚‚ , ΞΊβ‚‚) 𝒦₃@(K₃ , κ₃) = to-𝒦-＝ X ΞΊ ΞΊβ€² †
       where
        ΞΊ  = binary-coherence
              X
              Οƒ
              K₁
              (Kβ‚‚ ∨[ π’ͺ X ] K₃)
              κ₁
              (compact-opens-are-closed-under-∨ X Kβ‚‚ K₃ ΞΊβ‚‚ κ₃)
        ΞΊβ€² = compact-opens-are-closed-under-∨
              X
              (K₁ ∧[ π’ͺ X ] Kβ‚‚)
              (K₁ ∧[ π’ͺ X ] K₃)
              (binary-coherence X Οƒ K₁ Kβ‚‚ κ₁ ΞΊβ‚‚)
              (binary-coherence X Οƒ K₁ K₃ κ₁ κ₃)

        † : K₁ ∧[ π’ͺ X ] (Kβ‚‚ ∨[ π’ͺ X ] K₃) ＝ (K₁ ∧[ π’ͺ X ] Kβ‚‚) ∨[ π’ͺ X ] (K₁ ∧[ π’ͺ X ] K₃)
        † = binary-distributivity (π’ͺ X) K₁ Kβ‚‚ K₃

\end{code}

The lattice `𝒦⦅X⦆` is a small distributive lattice because we assumed the type
of compact opens to be small.

\begin{code}

 𝒦⦅X⦆-is-small : is-small ∣ 𝒦⦅X⦆ ∣ᡈ
 𝒦⦅X⦆-is-small = smallness-of-𝒦 ua X Οƒβ‚€

\end{code}

Added on 2024-04-12.

\begin{code}

 𝒦⁻ : 𝓀  Μ‡
 𝒦⁻ = resized ∣ 𝒦⦅X⦆ ∣ᡈ 𝒦⦅X⦆-is-small

 to-small-copy : ∣ 𝒦⦅X⦆ ∣ᡈ β†’ 𝒦⁻
 to-small-copy K =
  let
   e = resizing-condition 𝒦⦅X⦆-is-small
  in
   inverse ⌜ e ⌝ (⌜⌝-is-equiv e) K

 to-original : 𝒦⁻ β†’ ∣ 𝒦⦅X⦆ ∣ᡈ
 to-original = ⌜ resizing-condition 𝒦⦅X⦆-is-small ⌝

\end{code}

Added on 2024-04-30.

\begin{code}

 open OperationsOnCompactOpens X Οƒ

 open DistributiveLattice hiding (X)

 ΞΉβ‚–-preserves-∨ : (K₁ Kβ‚‚ : ∣ 𝒦⦅X⦆ ∣ᡈ) β†’ pr₁ (K₁ βˆ¨β‚– Kβ‚‚) ＝ pr₁ K₁ ∨[ π’ͺ X ] pr₁ Kβ‚‚
 ΞΉβ‚–-preserves-∨ K₁ Kβ‚‚ = ≀-is-antisymmetric (poset-of (π’ͺ X)) † ‑
  where
   † : (ΞΉβ‚– (K₁ βˆ¨β‚– Kβ‚‚) ≀[ poset-of (π’ͺ X) ] (ΞΉβ‚– K₁ ∨[ π’ͺ X ] ΞΉβ‚– Kβ‚‚)) holds
   † = ∨[ π’ͺ X ]-least
        (∨[ π’ͺ X ]-upper₁ (ΞΉβ‚– K₁) (ΞΉβ‚– Kβ‚‚))
        (∨[ π’ͺ X ]-upperβ‚‚ (ΞΉβ‚– K₁) (ΞΉβ‚– Kβ‚‚))

   ‑ : ((ΞΉβ‚– K₁ ∨[ π’ͺ X ] ΞΉβ‚– Kβ‚‚) ≀[ poset-of (π’ͺ X) ] ΞΉβ‚– (K₁ βˆ¨β‚– Kβ‚‚)) holds
   ‑ = ∨[ π’ͺ X ]-least
        (∨[ π’ͺ X ]-upper₁ (ΞΉβ‚– K₁) (ΞΉβ‚– Kβ‚‚))
        (∨[ π’ͺ X ]-upperβ‚‚ (ΞΉβ‚– K₁) (ΞΉβ‚– Kβ‚‚))

 ΞΉβ‚–-preserves-∧ : (K₁ Kβ‚‚ : ∣ 𝒦⦅X⦆ ∣ᡈ)
                β†’ pr₁ (K₁ βˆ§β‚– Kβ‚‚) ＝ pr₁ K₁ ∧[ π’ͺ X ] pr₁ Kβ‚‚
 ΞΉβ‚–-preserves-∧ K₁ Kβ‚‚ = ≀-is-antisymmetric (poset-of (π’ͺ X)) † ‑
  where
   † : (pr₁ (K₁ βˆ§β‚– Kβ‚‚) ≀[ poset-of (π’ͺ X) ] (pr₁ K₁ ∧[ π’ͺ X ] pr₁ Kβ‚‚)) holds
   † = ∧[ π’ͺ X ]-greatest
        (ΞΉβ‚– K₁)
        (ΞΉβ‚– Kβ‚‚)
        (pr₁ (K₁ βˆ§β‚– Kβ‚‚))
        (∧[ π’ͺ X ]-lower₁ (ΞΉβ‚– K₁) (ΞΉβ‚– Kβ‚‚))
        (∧[ π’ͺ X ]-lowerβ‚‚ (pr₁ K₁) (pr₁ Kβ‚‚))

   ‑ : ((pr₁ K₁ ∧[ π’ͺ X ] pr₁ Kβ‚‚) ≀[ poset-of (π’ͺ X) ] pr₁ (K₁ βˆ§β‚– Kβ‚‚)) holds
   ‑ = ∧[ π’ͺ X ]-greatest
        (pr₁ K₁)
        (pr₁ Kβ‚‚)
        (pr₁ (K₁ βˆ§β‚– Kβ‚‚))
        (∧[ π’ͺ X ]-lower₁ (ΞΉβ‚– K₁) (ΞΉβ‚– Kβ‚‚))
        (∧[ π’ͺ X ]-lowerβ‚‚ (pr₁ K₁) (pr₁ Kβ‚‚))

\end{code}