Locales.DistributiveLattice.Spectrum-Properties
--- title: Properties of the locale of spectra author: Ayberk Tosun date-started: 2024-03-01 dates-updated: [2024-03-27, 2024-04-08, 2024-04-09, 2024-06-05] --- We define the spectrum locale over a distributive lattice `L`, the defining frame of which is the frame of ideals over `L`.{-# OPTIONS --safe --without-K #-} open import UF.PropTrunc open import UF.FunExt open import UF.Subsingletons open import UF.Size module Locales.DistributiveLattice.Spectrum-Properties (fe : Fun-Ext) (pe : Prop-Ext) (pt : propositional-truncations-exist) (sr : Set-Replacement pt) where open import Locales.Compactness.Definition pt fe open import Locales.DistributiveLattice.Definition fe pt open import Locales.DistributiveLattice.Ideal pt fe pe open import Locales.DistributiveLattice.Ideal-Properties pt fe pe open import Locales.DistributiveLattice.Properties fe pt open import Locales.DistributiveLattice.Spectrum fe pe pt open import Locales.Frame pt fe open import Locales.SmallBasis pt fe sr open import Locales.Spectrality.SpectralLocale pt fe open import MLTT.List hiding ([_]) open import MLTT.Spartan open import Slice.Family open import UF.Classifiers open import UF.Equiv renaming (_■ to _𝐐𝐄𝐃) open import UF.ImageAndSurjection pt open import UF.Logic open import UF.Powerset-MultiUniverse hiding (𝕋) open import UF.SubtypeClassifier open AllCombinators pt fe renaming (_∧_ to _∧ₚ_; _∨_ to _∨ₚ_) open Locale open PropositionalSubsetInclusionNotation fe open PropositionalTruncation pt hiding (_∨_)We work with a fixed distributive 𝓤-lattice `L` in this module.module Spectrality (L : DistributiveLattice 𝓤) where open DefnOfFrameOfIdeal L open DistributiveLattice L renaming (X-is-set to σ) open IdealNotation L open IdealProperties LWe abbreviate the `spectrum` of `L` to `spec-L`.private spec-L : Locale (𝓤 ⁺) 𝓤 𝓤 spec-L = spectrumThe locale `spec-L` is a compact locale.spectrum-is-compact : is-compact spec-L holds spectrum-is-compact S δ p = ∥∥-rec ∃-is-prop † (p 𝟏 (𝟏ᵈ-is-top L 𝟏)) where † : Σ xs ꞉ List X , xs ◁ S × (𝟏 ＝ join-listᵈ L xs) → ∃ i ꞉ index S , (𝟏[ 𝒪 spec-L ] ⊆ᵢ (S [ i ])) holds † (xs , c , r) = ∥∥-rec ∃-is-prop ‡ (finite-subcover S xs δ c) where ‡ : Σ k ꞉ index S , join-listᵈ L xs ∈ⁱ (S [ k ]) → ∃ i ꞉ index S , (𝟏[ 𝒪 spec-L ] ⊆ᵢ (S [ i ])) holds ‡ (k , p) = ∣ k , contains-𝟏-implies-above-𝟏 (S [ k ]) μ ∣ where μ : 𝟏 ∈ⁱ (S [ k ]) μ = transport (λ - → - ∈ⁱ (S [ k ])) (r ⁻¹) pAdded on 2024-03-13. Every ideal `I` is the join of its principal ideals. We call this join the _factorization_ of `I` into its join of principal ideals, and we denote by `factorization` the function implementing this.open PrincipalIdeals L open Joins _⊆ᵢ_ factorization : Ideal L → Ideal L factorization I = ⋁[ 𝒪 spec-L ] principal-ideals-of I ideal-equal-to-factorization : (I : Ideal L) → I ＝ factorization I ideal-equal-to-factorization I = ⋁[ 𝒪 spec-L ]-unique (principal-ideals-of I) I († , ‡) where † : (I is-an-upper-bound-of (principal-ideals-of I)) holds † = ideal-is-an-upper-bound-of-its-principal-ideals I ‡ : ((Iᵤ , _) : upper-bound (principal-ideals-of I)) → I ⊆ᵢ Iᵤ holds ‡ (Iᵤ , υ) = ideal-is-lowerbound-of-upperbounds-of-its-principal-ideals I Iᵤ υThe family of principal ideals in an ideal is a directed family.factorization-is-directed : (I : Ideal L) → is-directed (𝒪 spec-L) (principal-ideals-of I) holds factorization-is-directed = principal-ideals-of-ideal-form-a-directed-familyAdded on 2024-03-27 For every `x : L`, the principal ideal `↓x` is a compact open of the locale of spectra.principal-ideal-is-compact : (x : ∣ L ∣ᵈ) → is-compact-open spec-L (↓ x) holds principal-ideal-is-compact x S δ p = ∥∥-rec ∃-is-prop † μ where μ : x ∈ᵢ (⋁[ 𝒪 spec-L ] S) holds μ = p x (≤ᵈ-is-reflexive L x) † : Σ xs ꞉ List X , xs ◁ S × (x ＝ join-listᵈ L xs) → ∃ i ꞉ index S , ↓ x ⊆ᵢ (S [ i ]) holds † (xs , q , r′) = ∥∥-rec ∃-is-prop ‡ β where β : ∃ i ꞉ index S , join-listᵈ L xs ∈ᵢ (S [ i ]) holds β = finite-subcover S xs δ q ‡ : Σ i ꞉ index S , join-listᵈ L xs ∈ᵢ (S [ i ]) holds → ∃ i ꞉ index S , ↓ x ⊆ᵢ (S [ i ]) holds ‡ (i , r) = ∣ i , γ ∣ where open Ideal (S [ i ]) renaming (I-is-downward-closed to Sᵢ-is-downward-closed) γ : (↓ x ⊆ᵢ (S [ i ])) holds γ y φ = Sᵢ-is-downward-closed y (join-listᵈ L xs) ϵ r where ϵ : (y ≤ᵈ[ L ] join-listᵈ L xs) holds ϵ = transport (λ - → (y ≤ᵈ[ L ] -) holds) r′ φAdded on 2024-06-05.↓ₖ_ : ∣ L ∣ᵈ → Σ I ꞉ Ideal L , (is-compact-open spec-L I holds) ↓ₖ_ x = ↓ x , principal-ideal-is-compact xEnd of addition. Added on 2024-03-13. Every ideal has a directed covering family consisting of compact opens.ideal-has-directed-cover-of-compact-opens : (I : Ideal L) → has-a-directed-cover-of-compact-opens spec-L I holds ideal-has-directed-cover-of-compact-opens I = ∣ principal-ideals-of I , κ , δ , eq ∣ where κ : consists-of-compact-opens spec-L (principal-ideals-of I) holds κ (x , _) = principal-ideal-is-compact x δ : is-directed (𝒪 spec-L) (principal-ideals-of I) holds δ = principal-ideals-of-ideal-form-a-directed-family I eq : I ＝ ⋁[ 𝒪 spec-L ] principal-ideals-of I eq = ideal-equal-to-factorization IAdded on 2024-04-08. We have already proved that every principal ideal is compact. We now prove the converse of this: every compact ideal is the principal ideal on some element `x` of the distributive lattice `L`.compact-ideal-is-principal : (I : Ideal L) → is-compact-open spec-L I holds → ∃ x ꞉ ∣ L ∣ᵈ , I ＝ principal-ideal x compact-ideal-is-principal I κ = ∥∥-rec ∃-is-prop γ (κ (principal-ideals-of I) δ c₀) where c : I ＝ factorization I c = ideal-equal-to-factorization I c₀ : (I ⊆ᵢ factorization I) holds c₀ = reflexivity+ (poset-of (𝒪 spec-L)) c c₁ : (factorization I ⊆ᵢ I) holds c₁ = reflexivity+ (poset-of (𝒪 spec-L)) (c ⁻¹) δ : is-directed (𝒪 spec-L) (principal-ideals-of I) holds δ = factorization-is-directed I γ : (Σ (x , _) ꞉ index (principal-ideals-of I) , (I ⊆ᵢ ↓ x) holds) → ∃ x ꞉ ∣ L ∣ᵈ , I ＝ ↓ x γ ((x , p) , φ) = ∣ x , ≤-is-antisymmetric (poset-of (𝒪 spec-L)) q₁ q₂ ∣ where open Ideal I using (I-is-downward-closed) q₁ : I ⊆ᵢ ↓ x holds q₁ = φ q₂ : ↓ x ⊆ᵢ I holds q₂ y μ = I-is-downward-closed y x μ pAdded on 2024-04-08. The map `↓(-) : L → Idl(L)` preserves meets.principal-ideal-preserves-meets : (x y : ∣ L ∣ᵈ) → ↓ (x ∧ y) ＝ ↓ x ∧[ 𝒪 spec-L ] ↓ y principal-ideal-preserves-meets x y = ≤-is-antisymmetric (poset-of (𝒪 spec-L)) † ‡ where open PosetReasoning (poset-ofᵈ L) † : (↓ (x ∧ y) ⊆ᵢ (↓ x ∧[ 𝒪 spec-L ] ↓ y)) holds † z p = †₁ , †₂ where †₁ : (z ≤ᵈ[ L ] x) holds †₁ = z ≤⟨ p ⟩ x ∧ y ≤⟨ ∧-is-a-lower-bound₁ L x y ⟩ x ■ †₂ : (z ≤ᵈ[ L ] y) holds †₂ = z ≤⟨ p ⟩ x ∧ y ≤⟨ ∧-is-a-lower-bound₂ L x y ⟩ y ■ ‡ : ((↓ x ∧[ 𝒪 spec-L ] ↓ y) ⊆ᵢ ↓ (x ∧ y)) holds ‡ = ∧-is-greatest L x yAdded on 2024-06-05. This has probably been written down somewhere else before.principal-ideal-preserves-top : ↓ 𝟏 ＝ 𝟏[ 𝒪 spec-L ] principal-ideal-preserves-top = only-𝟏-is-above-𝟏 (𝒪 spec-L) (↓ 𝟏) (λ _ → id) principal-ideal-preserves-bottom : ↓ 𝟎 ＝ 𝟎[ 𝒪 spec-L ] principal-ideal-preserves-bottom = only-𝟎-is-below-𝟎 (𝒪 spec-L) (↓ 𝟎) † where † : (↓ 𝟎 ≤[ poset-of (𝒪 spec-L) ] 𝟎[ 𝒪 spectrum ]) holds † x μ = transport (λ - → - ∈ⁱ 𝟎[ 𝒪 spectrum ]) (p ⁻¹) ideal-𝟎-contains-𝟎 where open Ideal 𝟎[ 𝒪 spectrum ] renaming (I-contains-𝟎 to ideal-𝟎-contains-𝟎) p : x ＝ 𝟎 p = only-𝟎-is-below-𝟎ᵈ L x μEnd of addition Added on 2024-04-08. The binary meet of two compact ideals is compact.compacts-of-the-spectrum-are-closed-under-∧ : compacts-of-[ spec-L ]-are-closed-under-binary-meets holds compacts-of-the-spectrum-are-closed-under-∧ K₁ K₂ κ₁ κ₂ = κ where ι₁ : ∃ x₁ ꞉ ∣ L ∣ᵈ , K₁ ＝ ↓ x₁ ι₁ = compact-ideal-is-principal K₁ κ₁ ι₂ : ∃ x₂ ꞉ ∣ L ∣ᵈ , K₂ ＝ ↓ x₂ ι₂ = compact-ideal-is-principal K₂ κ₂ κ : is-compact-open spec-L (K₁ ∧[ 𝒪 spec-L ] K₂) holds κ = ∥∥-rec₂ (holds-is-prop (is-compact-open spec-L (K₁ ∧[ 𝒪 spec-L ] K₂))) † ι₁ ι₂ where † : Σ x₁ ꞉ ∣ L ∣ᵈ , K₁ ＝ ↓ x₁ → Σ x₂ ꞉ ∣ L ∣ᵈ , K₂ ＝ ↓ x₂ → is-compact-open spec-L (K₁ ∧[ 𝒪 spec-L ] K₂) holds † (x₁ , p₁) (x₂ , p₂) = transport (λ - → is-compact-open spec-L - holds) (q ⁻¹) ‡ where q : K₁ ∧[ 𝒪 spec-L ] K₂ ＝ ↓ (x₁ ∧ x₂) q = K₁ ∧[ 𝒪 spec-L ] K₂ ＝⟨ Ⅰ ⟩ ↓ x₁ ∧[ 𝒪 spec-L ] K₂ ＝⟨ Ⅱ ⟩ ↓ x₁ ∧[ 𝒪 spec-L ] ↓ x₂ ＝⟨ Ⅲ ⟩ ↓ (x₁ ∧ x₂) ∎ where Ⅰ = ap (λ - → - ∧[ 𝒪 spec-L ] K₂) p₁ Ⅱ = ap (λ - → ↓ x₁ ∧[ 𝒪 spec-L ] -) p₂ Ⅲ = principal-ideal-preserves-meets x₁ x₂ ⁻¹ ‡ : is-compact-open spec-L (↓ (x₁ ∧ x₂)) holds ‡ = principal-ideal-is-compact (x₁ ∧ x₂)Added on 2024-04-08. Finally, we package everything up into a proof that the spectrum locale is spectral.spec-L-is-spectral : is-spectral spec-L holds spec-L-is-spectral = (κ , ν) , ideal-has-directed-cover-of-compact-opens where κ : is-compact spec-L holds κ = spectrum-is-compact ν : compacts-of-[ spec-L ]-are-closed-under-binary-meets holds ν = compacts-of-the-spectrum-are-closed-under-∧Everything after this line has been added on 2024-04-09. To show that the type of compact ideals is small, we directly construct the intensional specified basis for `Idl(L)` given by the family `↓(-) : L → Idl(L)`.ℬ-spec : Fam 𝓤 ⟨ 𝒪 spec-L ⟩ ℬ-spec = ∣ L ∣ᵈ , principal-ideal open classifier-single-universe ℬ-spec-is-directed-basis : directed-basis-forᴰ (𝒪 spec-L) ℬ-spec ℬ-spec-is-directed-basis ℐ = 𝕋 𝓤 ∣ L ∣ᵈ (_∈ⁱ ℐ) , † , 𝒹 where c : ℐ ＝ ⋁[ 𝒪 spec-L ] ⁅ ↓ x ∣ x ε 𝕋 𝓤 ∣ L ∣ᵈ (_∈ⁱ ℐ) ⁆ c = ideal-equal-to-factorization ℐ † : (ℐ is-lub-of ⁅ ↓ x ∣ x ε 𝕋 𝓤 ∣ L ∣ᵈ (_∈ⁱ ℐ) ⁆) holds † = transport (λ - → (- is-lub-of ⁅ ↓ x ∣ x ε 𝕋 𝓤 ∣ L ∣ᵈ (_∈ⁱ ℐ) ⁆) holds) (c ⁻¹) (⋁[ 𝒪 spec-L ]-upper _ , ⋁[ 𝒪 spec-L ]-least _) 𝒹 : is-directed (𝒪 spec-L) ⁅ ↓ x ∣ x ε (𝕋 𝓤 ∣ L ∣ᵈ (_∈ⁱ ℐ)) ⁆ holds 𝒹 = factorization-is-directed ℐ ℬ-spec-is-basis : basis-forᴰ (𝒪 spec-L) ℬ-spec ℬ-spec-is-basis = directed-basis-is-basis (𝒪 spec-L) ℬ-spec ℬ-spec-is-directed-basisWe denote by `𝒦-fam` the family corresponding to the subset of compact opens.𝒦-fam : Fam (𝓤 ⁺) ⟨ 𝒪 spec-L ⟩ 𝒦-fam = 𝕋 (𝓤 ⁺) ⟨ 𝒪 spec-L ⟩ (_holds ∘ is-compact-open spec-L)We know that the image of `↓(-) : L → Idl(L)` is equivalent to type of compact opens of `spec-L`.image-↓-equiv-to-𝒦 : image principal-ideal ≃ 𝒦 spec-L image-↓-equiv-to-𝒦 = basic-iso-to-𝒦 spec-L (ℬ-spec , ℬ-spec-is-directed-basis) principal-ideal-is-compactWe also know that the image of `↓(-)` is a 𝓤-small type.image-of-↓-is-small : (image principal-ideal) is 𝓤 small image-of-↓-is-small = basic-is-small spec-L (ℬ-spec , ℬ-spec-is-directed-basis) γ where open PosetNotation (poset-of (𝒪 spec-L)) γ : ⟨ 𝒪 spec-L ⟩ is-locally 𝓤 small γ I J = (I ≣ J) holds , s , (r , †) , (r , ‡) where s : (I ≣ J) holds → I ＝ J s (p₁ , p₂) = ≤-is-antisymmetric (poset-of (𝒪 spec-L)) p₁ p₂ r : I ＝ J → (I ≣ J) holds r p = transport (λ - → (- ≣ J) holds) (p ⁻¹) (≣-is-reflexive poset-of-ideals J) † : s ∘ r ∼ id † p = carrier-of-[ poset-of-ideals ]-is-set (s (r p)) p ‡ : r ∘ s ∼ id ‡ p = holds-is-prop (I ≣ J) (r (s p)) pWe use the superscript `(-)⁻` to denote the small copy of the type `image ↓(-)`.image-↓⁻ : 𝓤 ̇ image-↓⁻ = resized (image principal-ideal) image-of-↓-is-smallFrom the previous two equivalences, we can conclude that the type of compact opens of `spec-L` is equivalent to `image-↓⁻`.image-↓⁻-equiv-to-𝒦 : image-↓⁻ ≃ 𝒦 spec-L image-↓⁻-equiv-to-𝒦 = image-↓⁻ ≃⟨ Ⅰ ⟩ image principal-ideal ≃⟨ Ⅱ ⟩ 𝒦 spec-L 𝐐𝐄𝐃 where Ⅰ = resizing-condition image-of-↓-is-small Ⅱ = image-↓-equiv-to-𝒦This means that `𝒦(spec-L)` is 𝓤-small.spec-L-has-small-𝒦 : has-small-𝒦 spec-L spec-L-has-small-𝒦 = image-↓⁻ , image-↓⁻-equiv-to-𝒦