--------------------------------------------------------------------------------
title:          The spectrum of a distributive lattice
author:         Ayberk Tosun
date-started:   2024-02-21
date-completed: 2024-03-01
--------------------------------------------------------------------------------

We define the spectrum locale over a distributive lattice `L`, the defining
frame of which is the frame of ideals over `L`.

\begin{code}

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

open import UF.PropTrunc
open import UF.FunExt
open import UF.Subsingletons

module Locales.DistributiveLattice.Spectrum
        (fe : Fun-Ext)
        (pe : Prop-Ext)
        (pt : propositional-truncations-exist)
       where

open import Locales.DistributiveLattice.Definition fe pt
open import Locales.DistributiveLattice.Ideal pt fe pe
open import Locales.DistributiveLattice.Properties fe pt
open import Locales.Frame pt fe hiding (is-directed)
open import MLTT.Fin hiding (𝟎; 𝟏)
open import MLTT.List hiding ([_])
open import MLTT.Spartan
open import Slice.Family
open import UF.Logic
open import UF.Powerset-MultiUniverse
open import UF.SubtypeClassifier

open AllCombinators pt fe renaming (_∧_ to _∧ₚ_; _∨_ to _∨ₚ_)
open PropositionalSubsetInclusionNotation fe
open PropositionalTruncation pt hiding (_∨_)

\end{code}

We work with a fixed distributive lattice `L` in this module.

\begin{code}

module DefnOfFrameOfIdeal (L : DistributiveLattice 𝓤) where

 open DistributiveLattice L renaming (X-is-set to σ)

\end{code}

We denote by `_⊆ᵢ_` the inclusion ordering between two ideals.

\begin{code}

 _⊆ᵢ_ : Ideal L → Ideal L → Ω (𝓤)
 ℐ₁ ⊆ᵢ ℐ₂ = Ɐ x ꞉ ∣ L ∣ᵈ , x ∈ₚ I₁ ⇒ x ∈ₚ I₂
  where
   open Ideal ℐ₁ renaming (I to I₁)
   open Ideal ℐ₂ renaming (I to I₂)

 infix 30 _⊆ᵢ_

 ⊆ᵢ-is-reflexive : (I : Ideal L) → I ⊆ᵢ I holds
 ⊆ᵢ-is-reflexive _ _ = id

 ⊆ᵢ-is-transitive : (I₁ I₂ I₃ : Ideal L) → (I₁ ⊆ᵢ I₂ ⇒ I₂ ⊆ᵢ I₃ ⇒ I₁ ⊆ᵢ I₃) holds
 ⊆ᵢ-is-transitive I₁ I₂ I₃ p q x r = q x (p x r)

 ⊆ᵢ-is-antisymmetric : {I₁ I₂ : Ideal L}
                     → I₁ ⊆ᵢ I₂ holds → I₂ ⊆ᵢ I₁ holds → I₁ ＝ I₂
 ⊆ᵢ-is-antisymmetric {I₁} {I₂} = ideal-extensionality L I₁ I₂

 ⊆ᵢ-is-partial-order : is-partial-order (Ideal L) _⊆ᵢ_
 ⊆ᵢ-is-partial-order = (⊆ᵢ-is-reflexive , ⊆ᵢ-is-transitive) , ⊆ᵢ-is-antisymmetric

 poset-of-ideals : Poset (𝓤 ⁺) 𝓤
 poset-of-ideals = Ideal L
                 , _⊆ᵢ_
                 , (⊆ᵢ-is-reflexive  , ⊆ᵢ-is-transitive)
                 , ⊆ᵢ-is-antisymmetric

\end{code}

We denote by `𝟏ᵢ` the top ideal, which is the principal ideal on the top element
of the lattice `L`.

\begin{code}

 open PrincipalIdeals L

 𝟏ᵢ : Ideal L
 𝟏ᵢ = principal-ideal 𝟏

 𝟏ᵢ-is-top : (I : Ideal L) → (I ⊆ᵢ 𝟏ᵢ) holds
 𝟏ᵢ-is-top I x _ = 𝟏ᵈ-is-top L x

\end{code}

The binary meets of two ideals `I₁` and `I₂` is just the set intersection
`I₁ ∩ I₂`. We denote this by `I₁ ∧ᵢ I₂`.

\begin{code}

 _∧ᵢ_ : Ideal L → Ideal L → Ideal L
 ℐ₁ ∧ᵢ ℐ₂ =
  record
   { I                    = I₁ ∩ I₂
   ; I-is-inhabited       = ∣ 𝟎 , I₁-contains-𝟎 , I₂-contains-𝟎 ∣
   ; I-is-downward-closed = †
   ; I-is-closed-under-∨  = ‡
   }
   where
    open Ideal ℐ₁ renaming (I to I₁; I-contains-𝟎 to I₁-contains-𝟎)
    open Ideal ℐ₂ renaming (I to I₂; I-contains-𝟎 to I₂-contains-𝟎)

    † : is-downward-closed L (I₁ ∩ I₂) holds
    † x y p (q₁ , q₂) = Ideal.I-is-downward-closed ℐ₁ x y p q₁
                      , Ideal.I-is-downward-closed ℐ₂ x y p q₂

    ‡ : is-closed-under-binary-joins L (I₁ ∩ I₂) holds
    ‡ x y (p₁ , p₂) (q₁ , q₂) = Ideal.I-is-closed-under-∨ ℐ₁ x y p₁ q₁
                              , Ideal.I-is-closed-under-∨ ℐ₂ x y p₂ q₂

 infix 32 _∧ᵢ_

 open Meets _⊆ᵢ_

 ∧ᵢ-is-lower : (I₁ I₂ : Ideal L)
             → ((I₁ ∧ᵢ I₂) is-a-lower-bound-of (I₁ , I₂)) holds
 ∧ᵢ-is-lower I₁ I₂ = (λ _ → pr₁) , (λ _ → pr₂)

 ∧ᵢ-is-greatest : (I₁ I₂ I₃ : Ideal L)
                → (I₃ is-a-lower-bound-of (I₁ , I₂) ⇒ I₃ ⊆ᵢ (I₁ ∧ᵢ I₂)) holds
 ∧ᵢ-is-greatest I₁ I₂ I₃ (φ , ψ) x p = φ x p , ψ x p

 ∧ᵢ-is-glb : (I₁ I₂ : Ideal L) → ((I₁ ∧ᵢ I₂) is-glb-of (I₁ , I₂)) holds
 ∧ᵢ-is-glb I₁ I₂ = ∧ᵢ-is-lower I₁ I₂ , λ { (I₃ , p) → ∧ᵢ-is-greatest I₁ I₂ I₃ p }

\end{code}

We now begin to do some preparation for the construction of small joins of
ideals. We first define the covering relation `xs ◁ ( Iⱼ )_{j : J}` which
expresses that a list `xs` of elements of the lattice `L` is contained in the
union of ideals `⋃_{j : J} I_j`. Intuitively, this just says: for every `x` in
`xs`, there is an ideal `Iⱼ` with `x ∈ Iⱼ`.

\begin{code}

 open IdealNotation L

 open binary-unions-of-subsets pt

 infix 30 covering-syntax

 covering-syntax : (S : Fam 𝓤 (Ideal L)) → List ∣ L ∣ᵈ → 𝓤  ̇
 covering-syntax S []       = 𝟙
 covering-syntax S (x ∷ xs) =
  (Σ i ꞉ index S , x ∈ᵢ (S [ i ]) holds) × covering-syntax S xs

 syntax covering-syntax S xs = xs ◁ S

\end{code}

Below are some simple lemmas about the covering relation.

\begin{code}

 covering-cons : (S : Fam 𝓤 (Ideal L)) {x : ∣ L ∣ᵈ} {xs : List ∣ L ∣ᵈ}
               → (x ∷ xs) ◁ S → xs ◁ S
 covering-cons S (_ , c) = c

 covering-lemma : (S : Fam 𝓤 (Ideal L)) (xs : List ∣ L ∣ᵈ)
                → xs ◁ S
                → (x : ∣ L ∣ᵈ) → member x xs → Σ i ꞉ index S , x ∈ⁱ (S [ i ])
 covering-lemma S []       p             x  ()
 covering-lemma S (x ∷ xs) ((i , r) , q) x  in-head     = i , r
 covering-lemma S (x ∷ xs) p             x′ (in-tail r) = IH
  where
   IH : Σ i ꞉ index S , x′ ∈ᵢ (S [ i ]) holds
   IH = covering-lemma S xs (covering-cons S p) x′ r

 covering-++ : (S : Fam 𝓤 (Ideal L)) (xs ys : List ∣ L ∣ᵈ)
             → xs ◁ S → ys ◁ S → (xs ++ ys) ◁ S
 covering-++ S    []       []         _ q             = q
 covering-++ S    []       ys@(_ ∷ _) _ q             = q
 covering-++ S xs@(_ ∷ _)  []         p q             = transport
                                                         (λ - → - ◁ S)
                                                         ([]-right-neutral xs)
                                                         p
 covering-++ S    (x ∷ xs) (y ∷ ys)  ((i , r) , p₂) q =
  (i , r) , covering-++ S xs (y ∷ ys) p₂ q

 covering-intersection : (S : Fam 𝓤 (Ideal L)) (I : Ideal L) (xs : List ∣ L ∣ᵈ)
                       → join-listᵈ L xs ∈ⁱ I
                       → xs ◁ S
                       → xs ◁ ⁅ I ∧ᵢ (S [ i ]) ∣ i ∶ index S ⁆
 covering-intersection S I []       _ _             = ⋆
 covering-intersection S I (x ∷ xs) p ((i , r) , c) =
  (i , q , r) , covering-intersection S I xs p′ c
   where
    open Ideal I using (I-is-downward-closed)

    † : (join-listᵈ L xs ≤ᵈ[ L ] join-listᵈ L (x ∷ xs)) holds
    † = ∨-is-an-upper-bound₂ L x (join-listᵈ L xs)

    q : x ∈ⁱ I
    q = I-is-downward-closed
         x
         (join-listᵈ L (x ∷ xs))
         (∨-is-an-upper-bound₁ L x (join-listᵈ L xs)) p

    p′ : join-listᵈ L xs ∈ⁱ I
    p′ = I-is-downward-closed (join-listᵈ L xs) (join-listᵈ L (x ∷ xs)) † p

 covering-∧ : (S : Fam 𝓤 (Ideal L)) (x : ∣ L ∣ᵈ) (xs : List ∣ L ∣ᵈ)
            → xs ◁ S → map (x ∧_) xs ◁ S
 covering-∧ S x []       q             = q
 covering-∧ S y (x ∷ xs) ((i , r) , c) = (i , †) , covering-∧ S y xs c
  where
   open Ideal (S [ i ]) renaming (I to I₁;
                                  I-is-downward-closed to Sᵢ-is-downward-closed)

   † : (y ∧ x) ∈ᵢ (S [ i ]) holds
   † = Sᵢ-is-downward-closed (y ∧ x) x (∧-is-a-lower-bound₂ L y x) r

\end{code}

The lemma below captures the fact that covers of lists always have a finite
subcover.

\begin{code}

 open Locale
 open import Locales.DirectedFamily pt fe _⊆ᵢ_


 finite-subcover : (S : Fam 𝓤 (Ideal L)) (xs : List ∣ L ∣ᵈ)
                 → is-directed S holds
                 → xs ◁ S
                 → ∃ i ꞉ index S , join-listᵈ L xs ∈ᵢ (S [ i ]) holds
 finite-subcover S [] δ c = ∥∥-rec ∃-is-prop γ (directed-implies-inhabited S δ)
  where
   γ : index S → ∃ i ꞉ index S , join-listᵈ L [] ∈ⁱ (S [ i ])
   γ i = ∣ i , Sᵢ-contains-𝟎 ∣
    where
     open Ideal (S [ i ]) renaming (I-contains-𝟎 to Sᵢ-contains-𝟎)
 finite-subcover S (x ∷ xs) δ ((i , μ) , c) = ∥∥-rec ∃-is-prop † IH
  where
   IH : ∃ i ꞉ index S , join-listᵈ L xs ∈ᵢ (S [ i ]) holds
   IH = finite-subcover S xs δ c

   † : Σ i ꞉ index S , join-listᵈ L xs ∈ⁱ (S [ i ])
     → ∃ k ꞉ index S , join-listᵈ L (x ∷ xs) ∈ⁱ (S [ k ])
   † (j , p) = ∥∥-rec ∃-is-prop ‡ (pr₂ δ i j)
    where
     ‡ : Σ k ꞉ index S , ((S [ i ]) ⊆ᵢ (S [ k ]) ∧ₚ (S [ j ]) ⊆ᵢ (S [ k ])) holds
       → ∃ k ꞉ index S , join-listᵈ L (x ∷ xs) ∈ⁱ (S [ k ])
     ‡ (k , μ₁ , μ₂) =
      ∣ k , Sᵢ-is-closed-under-∨ x (join-listᵈ L xs ) (μ₁ x μ) (μ₂ (join-listᵈ L xs) p) ∣
       where
        open Ideal (S [ k ]) renaming (I-is-closed-under-∨ to Sᵢ-is-closed-under-∨)

\end{code}

We are now ready to define the join. Given a family `( Iⱼ )_{j : J}` of ideals,
their union is given by the family:

    { (⋁ F) ∣ F ⊆ (⋃_{j : J} I_j), F finite }.

We capture finiteness using lists instead (which amounts to Kuratowski
finiteness).

We start by defining a preliminary version of the join operation that gives the
underlying subset of the ideal. We then proceed to prove that this forms an
ideal.

\begin{code}

 ⋁⁰ᵢ_ : Fam 𝓤 (Ideal L) → 𝓟 {𝓤} ∣ L ∣ᵈ
 ⋁⁰ᵢ_ S = λ y → Ǝ xs ꞉ List ∣ L ∣ᵈ , xs ◁ S × (y ＝ join-listᵈ L xs)

 infix 41 ⋁⁰ᵢ_

\end{code}

It is easy to see that this operation gives subsets that are closed under binary
joins.

\begin{code}

 ideal-join-is-closed-under-∨ : (I : Fam 𝓤 (Ideal L))
                              → is-closed-under-binary-joins L (⋁⁰ᵢ I) holds
 ideal-join-is-closed-under-∨ S x y μ₁ μ₂ =
  ∥∥-rec₂ (holds-is-prop ((x ∨ y) ∈ₚ ⋁⁰ᵢ S)) † μ₁ μ₂
   where
    † : Σ xs ꞉ List X , xs ◁ S × (x ＝ join-listᵈ L xs)
      → Σ ys ꞉ List X , ys ◁ S × (y ＝ join-listᵈ L ys)
      → (x ∨ y) ∈ (⋁⁰ᵢ S)
    † (xs , c₁ , p₁) (ys , c₂ , p₂) = ∣ (xs ++ ys) , c , p ∣
     where
      c : (xs ++ ys) ◁ S
      c = covering-++ S xs ys c₁ c₂

      p : (x ∨ y) ＝ join-listᵈ L (xs ++ ys)
      p = x ∨ y                             ＝⟨ Ⅰ ⟩
          join-listᵈ L xs ∨ y               ＝⟨ Ⅱ ⟩
          join-listᵈ L xs ∨ join-listᵈ L ys ＝⟨ Ⅲ ⟩
          join-listᵈ L (xs ++ ys)           ∎
           where
            Ⅰ = ap (_∨ y) p₁
            Ⅱ = ap (join-listᵈ L xs ∨_) p₂
            Ⅲ = join-list-maps-∨-to-++ L xs ys

\end{code}

The operation `⋁⁰ᵢ_` gives subsets that are downward closed.

\begin{code}

 ideal-join-is-downward-closed : (S : Fam 𝓤 (Ideal L))
                               → is-downward-closed L (⋁⁰ᵢ S) holds
 ideal-join-is-downward-closed S x y q = ∥∥-rec (holds-is-prop (x ∈ₚ ⋁⁰ᵢ S)) †
  where
   open PosetReasoning (poset-ofᵈ L)

   † : Σ ys ꞉ List X , ys ◁ S × (y ＝ join-listᵈ L ys) → x ∈ (⋁⁰ᵢ S)
   † (ys , c , p) = ∣ map (x ∧_) ys , c′ , r ∣
    where
     c′ : map (x ∧_) ys ◁ S
     c′ = covering-∧ S x ys c

     Ⅰ : (x ≤ᵈ[ L ] join-listᵈ L ys) holds
     Ⅰ = x ≤⟨ q ⟩ y ＝⟨ p ⟩ₚ join-listᵈ L ys ■

     Ⅱ = finite-distributivity L ys x

     r : x ＝ join-listᵈ L (map (x ∧_) ys)
     r = x                            ＝⟨ Ⅰ ⁻¹ ⟩
         x ∧ join-listᵈ L ys          ＝⟨ Ⅱ    ⟩
         join-listᵈ L (map (x ∧_) ys) ∎

\end{code}

We package the proofs up into the following join operation `⋁ᵢ_`.

\begin{code}

 ⋁ᵢ_ : Fam 𝓤 (Ideal L) → Ideal L
 ⋁ᵢ S = record
         { I                    = ⋁⁰ᵢ S
         ; I-is-inhabited       = ∣ 𝟎 , ∣ [] , (⋆ , refl) ∣ ∣
         ; I-is-downward-closed = ideal-join-is-downward-closed S
         ; I-is-closed-under-∨  = ideal-join-is-closed-under-∨ S
         }

\end{code}

It is obvious that this gives contains all the ideals in the family.

\begin{code}

 ⋁ᵢ-is-an-upper-bound : (S : Fam 𝓤 (Ideal L))
                      → (i : index S) → (S [ i ]) ⊆ᵢ (⋁ᵢ S) holds
 ⋁ᵢ-is-an-upper-bound S i x p = ∣ (x ∷ []) , † , (∨-unit x ⁻¹) ∣
  where
   open Ideal (S [ i ]) renaming (I-is-downward-closed
                                   to Sᵢ-is-downward-closed)

   † : (x ∷ []) ◁ S
   † = (i , p) , ⋆

\end{code}

The fact that it is a least upper bound is not as trivial and uses the
`covering-lemma` we gave above.

\begin{code}

 open Joins _⊆ᵢ_

 ⋁ᵢ-is-least : (S  : Fam 𝓤 (Ideal L))
             → (Iᵤ : Ideal L)
             → (Iᵤ is-an-upper-bound-of S ⇒ (⋁ᵢ S) ⊆ᵢ Iᵤ) holds
 ⋁ᵢ-is-least S Iᵤ υ x = ∥∥-rec (holds-is-prop (x ∈ᵢ Iᵤ)) †
  where
   † : Σ xs ꞉ List X , xs ◁ S × (x ＝ join-listᵈ L xs) → x ∈ᵢ Iᵤ holds
   † (xs , c , r) = transport
                     (λ - → - ∈ᵢ Iᵤ holds)
                     (r ⁻¹)
                     (ideals-are-closed-under-finite-joins L Iᵤ xs φ)
    where
     φ : ((x , _) : type-from-list xs) → x ∈ᵢ Iᵤ holds
     φ (x , μ) = υ iₓ x ν
      where
       θ : Σ i ꞉ index S , x ∈ᵢ (S [ i ]) holds
       θ = covering-lemma S xs c x μ

       iₓ = pr₁ θ

       ν : (x ∈ᵢ (S [ iₓ ])) holds
       ν = pr₂ θ

\end{code}

Finally, we prove the distributivity law.

\begin{code}

 distributivityᵢ : (I : Ideal L) (S : Fam 𝓤 (Ideal L))
                 → I ∧ᵢ (⋁ᵢ S) ＝ ⋁ᵢ ⁅ I ∧ᵢ (S [ i ]) ∣ i ∶ index S ⁆
 distributivityᵢ I S = ⊆ᵢ-is-antisymmetric † ‡
  where
   † : I ∧ᵢ (⋁ᵢ S) ⊆ᵢ (⋁ᵢ ⁅ I ∧ᵢ (S [ i ]) ∣ i ∶ index S ⁆) holds
   † x (μ₁ , μ₂) =
    ∥∥-rec (holds-is-prop (x ∈ᵢ (⋁ᵢ ⁅ I ∧ᵢ (S [ i ]) ∣ i ∶ index S ⁆))) γ μ₂
     where
      γ : Σ xs ꞉ List X , xs ◁ S × (x ＝ join-listᵈ L xs)
       → x ∈ᵢ (⋁ᵢ ⁅ I ∧ᵢ (S [ i ]) ∣ i ∶ index S ⁆) holds
      γ (xs , c , r) = ∣ xs , c′ , r ∣
       where
        μ : join-listᵈ L xs ∈ᵢ I holds
        μ = transport (λ - → - ∈ᵢ I holds) r μ₁

        c′ : xs ◁ ⁅ I ∧ᵢ (S [ i ]) ∣ i ∶ index S ⁆
        c′ = covering-intersection S I xs μ c

   ‡ : (⋁ᵢ ⁅ I ∧ᵢ (S [ i ]) ∣ i ∶ index S ⁆) ⊆ᵢ (I ∧ᵢ (⋁ᵢ S)) holds
   ‡ x p = ∥∥-rec (holds-is-prop (x ∈ᵢ (I ∧ᵢ (⋁ᵢ S)))) γ p
    where
     open PosetReasoning (poset-ofᵈ L)

     γ : Σ xs ꞉ List X ,
          xs ◁ ⁅ I ∧ᵢ (S [ i ]) ∣ i ∶ index S ⁆ × (x ＝ join-listᵈ L xs)
       → x ∈ᵢ I ∧ᵢ (⋁ᵢ S) holds
     γ (xs , c , r) = μ₁ , μ₂
      where
       ϟ : (x : ∣ L ∣ᵈ)
         → member x xs
         → Σ i ꞉ index S , x ∈ᵢ I ∧ᵢ (S [ i ]) holds
       ϟ x μ = covering-lemma ⁅ I ∧ᵢ (S [ i ]) ∣ i ∶ index S ⁆ xs c x μ

       ϵ : ((x , μ) : type-from-list xs) → x ∈ⁱ I
       ϵ (x , μ) = pr₁ (pr₂ (ϟ x μ))

       δ : join-listᵈ L xs ∈ⁱ I
       δ = ideals-are-closed-under-finite-joins L I xs ϵ

       μ₁ : x ∈ᵢ I holds
       μ₁ = transport (λ - → (- ∈ᵢ I) holds) (r ⁻¹) δ

       ι : ((x , μ) : type-from-list xs) → x ∈ᵢ (⋁ᵢ S) holds
       ι (x , μ) = ⋁ᵢ-is-an-upper-bound S iₓ x μ′
        where
         ν : Σ i ꞉ index S , x ∈ⁱ I ∧ᵢ (S [ i ])
         ν = ϟ x μ

         iₓ : index S
         iₓ = pr₁ ν

         μ′ : x ∈ⁱ (S [ iₓ ])
         μ′ = pr₂ (pr₂ ν)

       θ : join-listᵈ L xs ∈ⁱ (⋁ᵢ S)
       θ = ideals-are-closed-under-finite-joins L (⋁ᵢ S) xs ι

       μ₂ : x ∈ᵢ (⋁ᵢ S) holds
       μ₂ = transport (λ - → - ∈ᵢ (⋁ᵢ S) holds) (r ⁻¹) θ

\end{code}

We are now ready to package everything up as a frame.

\begin{code}

 frame-of-ideals : Frame (𝓤 ⁺) 𝓤 𝓤
 frame-of-ideals =
   Ideal L
  , (_⊆ᵢ_ , 𝟏ᵢ , _∧ᵢ_ , ⋁ᵢ_)
  , ⊆ᵢ-is-partial-order
  , 𝟏ᵢ-is-top
  , (λ (I₁ , I₂) → ∧ᵢ-is-lower I₁ I₂ , λ (I₃ , lb) → ∧ᵢ-is-greatest I₁ I₂ I₃ lb)
  , (λ S → ⋁ᵢ-is-an-upper-bound S , λ (I , ub) → ⋁ᵢ-is-least S I ub)
  , λ { (I , S) → distributivityᵢ I S }

\end{code}

This is the frame of opens of the “spectrum space” of the distributive lattice
`L`. Because we work with locales as our notion of space, we just take the
locale that this frame defines as the spectrum over the distributive lattice
`L`.

\begin{code}

 spectrum : Locale (𝓤 ⁺) 𝓤 𝓤
 spectrum = record
             { ⟨_⟩ₗ         = Ideal L
             ; frame-str-of = pr₂ frame-of-ideals }

\end{code}
