Ayberk Tosun.
Originally started 7th of December 2022.
Rewritten from scratch on 26th of April 2023.
Completed on the 2nd of June 2023.
\begin{code}[hide]
{-# OPTIONS --safe --without-K --lossy-unification #-}
open import MLTT.List hiding ([_])
open import MLTT.Spartan hiding (𝟚)
open import Slice.Family
open import UF.Base
open import UF.Embeddings
open import UF.Equiv renaming (_■ to _𝔔𝔈𝔇)
open import UF.FunExt
open import UF.PropTrunc
open import UF.PropTrunc
open import UF.Retracts
open import UF.EquivalenceExamples
open import UF.Size
module Locales.UniversalPropertyOfPatch
(pt : propositional-truncations-exist)
(fe : Fun-Ext)
(sr : Set-Replacement pt)
where
open import Locales.AdjointFunctorTheoremForFrames pt fe
open import Locales.Clopen pt fe sr
open import Locales.Compactness.Definition pt fe
open import Locales.Complements 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
open import Locales.GaloisConnection pt fe
open import Locales.HeytingComplementation pt fe sr
open import Locales.HeytingImplication pt fe
open import Locales.Nucleus pt fe
open import Locales.PatchLocale pt fe sr
open import Locales.PatchProperties pt fe sr
open import Locales.PerfectMaps pt fe
open import Locales.ScottContinuity pt fe sr
open import Locales.SmallBasis pt fe sr
open import Locales.Spectrality.Properties pt fe
open import Locales.Spectrality.SpectralLocale pt fe
open import Locales.Spectrality.SpectralMap pt fe
open import Locales.Stone pt fe sr
open import Locales.StoneImpliesSpectral pt fe sr
open import Locales.ZeroDimensionality pt fe sr
open import UF.ImageAndSurjection
open import UF.Logic
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open ContinuousMaps
open FrameHomomorphismProperties
open FrameHomomorphisms hiding (fun; fun-syntax)
open PropositionalTruncation pt
open AllCombinators pt fe
\end{code}
\begin{code}
open Locale
\end{code}
\section{Proof of the Universal Property}
In this module, we prove the following universal property:
given any continuous `f : X → A` from a Stone locale `X` into
a spectral locale `A`, there exists a unique map `f⁻` satisfying
`f⁺(U) = f⁻⁺(‘ U ’)` for any open `U : 𝒪(A)`.
This proof is given at the very end of the module and is called `ump-of-patch`.
In the following submodule `UniversalProperty` we assume the structures involved
in spectrality and zero-dimensionality and use this to prove the universal
property for the small version of Patch (which we often denote `Patchₛ`).
\begin{code}
module UniversalProperty (A : Locale (𝓤 ⁺) 𝓤 𝓤)
(X : Locale (𝓤 ⁺) 𝓤 𝓤)
(σᴰ : spectralᴰ A)
(𝕫ᴰ : zero-dimensionalᴰ (𝒪 X))
(𝕜 : is-compact X holds)
(𝒻 : X ─c→ A)
(μ : is-spectral-map A X 𝒻 holds) where
\end{code}
As prevoiusly mentioned, we assume
* `A` and `X`: large and locally small locales,
* `σᴰ`: the spectrality data of `A`,
* `𝕫ᴰ`: the zero-dimensioality structure of `X`
* `𝕜`: compactness of `X`
* `𝒻`: an arbitrary spectral continuous map from `X` into a `A` (which amounts
to a spectral frame homomorphisms from frame `𝒪(A)` into frame `𝒪(X)`.
* `μ`: proof that `𝒻` is a spectral map.
\begin{code}
σ : is-spectral A holds
σ = spectralᴰ-gives-spectrality A σᴰ
sk : 𝒦 A is 𝓤 small
sk = spectralᴰ-implies-small-𝒦 A σᴰ
open PatchConstruction A σ using (nucleus-of; _≼_; _$_; perfect-nuclei-eq;
idₙ; 𝔡𝔦𝔯)
open ClosedNucleus A σ
open OpenNucleus A σᴰ sk
open SmallPatchConstruction A σᴰ
using (𝟎-is-id; ≼-implies-≼ᵏ; ≼ᵏ-implies-≼; _≼ᵏ_)
renaming (SmallPatch to Patchₛ-A)
open ContinuousMapNotation X A hiding (_⋆)
\end{code}
\begin{code}
X-has-basis : has-basis (𝒪 X) holds
X-has-basis = ∣ zero-dimensionalᴰ-implies-has-basis (𝒪 X) 𝕫ᴰ ∣
\end{code}
We denote by `Bₐ` the index set of the basis of `A` and by `β` the enumeration
function of the basis.
\begin{code}
Bₐ : 𝓤 ̇
Bₐ = pr₁ (pr₁ σᴰ)
βₐ : Bₐ → ⟨ 𝒪 A ⟩
βₐ = pr₂ (pr₁ σᴰ)
\end{code}
Similarly by `Bₓ`, we denote the index set of the basis of `X` and by `βₓ`
the enumeration function.
\begin{code}
Bₓ : 𝓤 ̇
Bₓ = pr₁ (pr₁ 𝕫ᴰ)
βₓ : Bₓ → ⟨ 𝒪 X ⟩
βₓ = pr₂ (pr₁ 𝕫ᴰ)
\end{code}
\begin{code}
β-is-directed-basis : is-directed-basis (𝒪 A) (Bₐ , βₐ)
β-is-directed-basis = basisₛ-is-basis A σᴰ , basisₛ-covers-are-directed A σᴰ
A-directed-basisᴰ : directed-basisᴰ (𝒪 A)
A-directed-basisᴰ = basisₛ A σᴰ , †
where
† : directed-basis-forᴰ (𝒪 A) (Bₐ , βₐ)
† U = pr₁ Σ-assoc (basisₛ-is-basis A σᴰ U , basisₛ-covers-are-directed A σᴰ U)
β-is-basis-for-A : is-basis-for (𝒪 A) (Bₐ , βₐ)
β-is-basis-for-A = pr₁ β-is-directed-basis
A-has-basis : has-basis (𝒪 A) holds
A-has-basis = ∣ (Bₐ , βₐ) , β-is-basis-for-A ∣
infixl 4 _∧ₓ_
_∧ₓ_ : ⟨ 𝒪 X ⟩ → ⟨ 𝒪 X ⟩ → ⟨ 𝒪 X ⟩
U ∧ₓ V = U ∧[ 𝒪 X ] V
infix 5 _≤ₓ_
_≤ₓ_ : ⟨ 𝒪 X ⟩ → ⟨ 𝒪 X ⟩ → Ω 𝓤
_≤ₓ_ = λ U V → U ≤[ poset-of (𝒪 X) ] V
\end{code}
\begin{code}
open HeytingImplicationConstruction X X-has-basis
open HeytingImplicationConstruction A A-has-basis
using ()
renaming (_==>_ to _==>ₐ_; H₈ to H₈ₐ;
heyting-implication-identity to heyting-implication-identityₐ;
heyting-implication₁ to heyting-implication₁ₐ;
==>-right-monotone to ==>ₐ-right-monotone;
ex-falso-quodlibet to ex-falso-quodlibetₐ)
\end{code}
It is often convenient to have a version of `βₐ` that also gives the proof
of compactness of the basic open it returns.
\begin{code}
κₐ : (i : Bₐ) → is-compact-open A (βₐ i) holds
κₐ = basisₛ-consists-of-compact-opens A σᴰ
βₖ : Bₐ → 𝒦 A
βₖ i = βₐ i , κₐ i
\end{code}
The following is shorthand notation for the negation of `𝒻 ⋆∙ U` which we know
to be the complement of `𝒻 ⋆∙ U`.
\begin{code}
¬𝒻⋆ : ⟨ 𝒪 A ⟩ → ⟨ 𝒪 X ⟩
¬𝒻⋆ U = (𝒻 ⋆∙ U) ==> 𝟎[ 𝒪 X ]
¬𝒻⋆𝟎-is-𝟏 : ¬𝒻⋆ 𝟎[ 𝒪 A ] ＝ 𝟏[ 𝒪 X ]
¬𝒻⋆𝟎-is-𝟏 = only-𝟏-is-above-𝟏 (𝒪 X) (¬𝒻⋆ 𝟎[ 𝒪 A ]) †
where
open PosetReasoning (poset-of (𝒪 X))
‡ : ((𝟏[ 𝒪 X ] ∧[ 𝒪 X ] 𝒻 ⋆∙ 𝟎[ 𝒪 A ]) ≤[ poset-of (𝒪 X) ] 𝟎[ 𝒪 X ]) holds
‡ = 𝟏[ 𝒪 X ] ∧[ 𝒪 X ] 𝒻 ⋆∙ 𝟎[ 𝒪 A ] ≤⟨ Ⅰ ⟩
𝒻 ⋆∙ 𝟎[ 𝒪 A ] ＝⟨ Ⅱ ⟩ₚ
𝟎[ 𝒪 X ] ■
where
Ⅰ = ∧[ 𝒪 X ]-lower₂ 𝟏[ 𝒪 X ] (𝒻 ⋆∙ 𝟎[ 𝒪 A ])
Ⅱ = frame-homomorphisms-preserve-bottom (𝒪 A) (𝒪 X) 𝒻
† : (𝟏[ 𝒪 X ] ≤[ poset-of (𝒪 X) ] ¬𝒻⋆ 𝟎[ 𝒪 A ]) holds
† = heyting-implication₁ (𝒻 ⋆∙ 𝟎[ 𝒪 A ]) 𝟎[ 𝒪 X ] 𝟏[ 𝒪 X ] ‡
\end{code}
The following is a ternary relation expressing, for a basic open
`‘β(m)’ ∧ ¬‘β(n)’` to be below some perfect nucleus.
TODO: improve the naming.
\begin{code}
𝔏 : ⟨ 𝒪 Patchₛ-A ⟩ → Bₐ → Bₐ → Ω 𝓤
𝔏 𝒿 m n = (‘ βₐ m ’ ∧[ 𝒪 Patchₛ-A ] ¬‘ βₖ n ’) ≼ᵏ 𝒿
below : ⟨ 𝒪 Patchₛ-A ⟩ → 𝓤 ̇
below 𝒿 = Σ m ꞉ Bₐ , Σ n ꞉ Bₐ , 𝔏 𝒿 m n holds
\end{code}
This is the unique function that we define that makes our diagram commute.
\begin{code}
f⁻⁺ : ⟨ 𝒪 Patchₛ-A ⟩ → ⟨ 𝒪 X ⟩
f⁻⁺ 𝒿 = ⋁[ 𝒪 X ] ⁅ (𝒻 ⋆∙ βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n) ∣ (m , n , p) ∶ below 𝒿 ⁆
\end{code}
There is an equivalent way to define `f⁻⁺`, given in `f⁻⁺₂` below. The
equivalence of the two is quite important and is used in the proofs below.
\begin{code}
f⁻⁺₂ : ⟨ 𝒪 Patchₛ-A ⟩ → ⟨ 𝒪 X ⟩
f⁻⁺₂ 𝒿@(j , _) = ⋁[ 𝒪 X ] ⁅ 𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆
f⁻⁺₂-equiv-f⁻⁺₁ : (𝒿 : ⟨ 𝒪 Patchₛ-A ⟩) → f⁻⁺ 𝒿 ＝ f⁻⁺₂ 𝒿
f⁻⁺₂-equiv-f⁻⁺₁ 𝒿@(j , _) = ≤-is-antisymmetric (poset-of (𝒪 X)) † ‡
where
S : Fam 𝓤 ⟨ 𝒪 X ⟩
S = ⁅ (𝒻 ⋆∙ βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n) ∣ (m , n , p) ∶ below 𝒿 ⁆
T : Fam 𝓤 ⟨ 𝒪 X ⟩
T = ⁅ 𝒻 ⋆∙ j (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆
†₀ : cofinal-in (𝒪 X) S T holds
†₀ (m , n , p) = ∣ n , ※ ∣
where
open PosetReasoning (poset-of (𝒪 A))
Ⅰ = ∨[ 𝒪 A ]-upper₁ (βₐ m) (βₐ n)
Ⅱ = 𝟏-right-unit-of-∧ (𝒪 A) (βₐ m ∨[ 𝒪 A ] βₐ n) ⁻¹
Ⅲ = ap
(λ - → (βₐ m ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 A ] -)
(heyting-implication-identityₐ (βₐ n) ⁻¹)
q : (βₐ m ≤[ poset-of (𝒪 A) ] j (βₐ n)) holds
q = βₐ m ≤⟨ Ⅰ ⟩
βₐ m ∨[ 𝒪 A ] βₐ n ＝⟨ Ⅱ ⟩ₚ
(βₐ m ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 A ] 𝟏[ 𝒪 A ] ＝⟨ Ⅲ ⟩ₚ
(βₐ m ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 A ] (βₐ n ==>ₐ βₐ n) ＝⟨ refl ⟩ₚ
(βₐ m ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 A ] (¬‘ βₖ n ’ .pr₁ (βₐ n)) ＝⟨ refl ⟩ₚ
(‘ βₐ m ’ ∧[ 𝒪 Patchₛ-A ] ¬‘ βₖ n ’) .pr₁ (βₐ n) ≤⟨ p n ⟩
j (βₐ n) ■
※ : ((𝒻 ⋆∙ βₐ m ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n))
≤[ poset-of (𝒪 X) ]
(𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] (¬𝒻⋆ (βₐ n)))) holds
※ = ∧[ 𝒪 X ]-left-monotone
(frame-morphisms-are-monotonic
(𝒪 A)
(𝒪 X)
(𝒻 ⋆∙_)
(𝒻 .pr₂)
(βₐ m , j (βₐ n)) q)
† : ((⋁[ 𝒪 X ] S) ≤[ poset-of (𝒪 X) ] (⋁[ 𝒪 X ] T)) holds
† = cofinal-implies-join-covered (𝒪 X) S T †₀
‡ : ((⋁[ 𝒪 X ] T) ≤[ poset-of (𝒪 X) ] (⋁[ 𝒪 X ] S)) holds
‡ = ⋁[ 𝒪 X ]-least T ((⋁[ 𝒪 X ] S) , ‡₁)
where
open Joins (λ x y → x ≤[ poset-of (𝒪 X) ] y)
‡₁ : ((⋁[ 𝒪 X ] S) is-an-upper-bound-of T) holds
‡₁ n =
let
open PosetReasoning (poset-of (𝒪 X))
in
𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ＝⟨ Ⅰ ⟩ₚ
𝒻 ⋆∙ (⋁[ 𝒪 A ] ⁅ βₐ i ∣ i ε 𝒥 ⁆) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ＝⟨ Ⅱ ⟩ₚ
(⋁[ 𝒪 X ] ⁅ 𝒻 ⋆∙ (βₐ i) ∣ i ε 𝒥 ⁆) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ＝⟨ Ⅲ ⟩ₚ
⋁[ 𝒪 X ] ⁅ 𝒻 ⋆∙ (βₐ i) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ i ε 𝒥 ⁆ ≤⟨ Ⅳ ⟩
⋁[ 𝒪 X ] S ■
where
𝒥 : Fam 𝓤 Bₐ
𝒥 = cover-indexₛ A σᴰ (j (βₐ n))
♠ : ((⋁[ 𝒪 X ] S)
is-an-upper-bound-of
⁅ 𝒻 ⋆∙ (βₐ i) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ i ε 𝒥 ⁆) holds
♠ i = ⋁[ 𝒪 X ]-upper S (𝒥 [ i ] , n , ♢)
where
open PosetReasoning (poset-of (𝒪 A))
open NucleusHeytingImplicationLaw A A-has-basis (nucleus-of 𝒿)
♢ : 𝔏 𝒿 (𝒥 [ i ]) n holds
♢ m =
(‘ βₐ (𝒥 [ i ]) ’ ∧[ 𝒪 Patchₛ-A ] ¬‘ βₖ n ’) .pr₁ (βₐ m) ＝⟨ refl ⟩ₚ
((βₐ (𝒥 [ i ]) ∨[ 𝒪 A ] βₐ m) ∧[ 𝒪 A ] (βₐ n ==>ₐ βₐ m)) ≤⟨ Ⅰ ⟩
(j (βₐ n) ∨[ 𝒪 A ] βₐ m) ∧[ 𝒪 A ] (βₐ n ==>ₐ βₐ m) ≤⟨ Ⅱ ⟩
(j (βₐ n) ∨[ 𝒪 A ] βₐ m) ∧[ 𝒪 A ] (βₐ n ==>ₐ j (βₐ m)) ＝⟨ Ⅲ ⟩ₚ
(j (βₐ n) ∨[ 𝒪 A ] βₐ m) ∧[ 𝒪 A ] (j (βₐ n) ==>ₐ j (βₐ m)) ≤⟨ Ⅳ ⟩
(j (βₐ n) ∨[ 𝒪 A ] j (βₐ m)) ∧[ 𝒪 A ] (j (βₐ n) ==>ₐ j (βₐ m)) ＝⟨ Ⅴ ⟩ₚ
(j (βₐ m) ∨[ 𝒪 A ] j (βₐ n)) ∧[ 𝒪 A ] (j (βₐ n) ==>ₐ j (βₐ m)) ＝⟨ Ⅵ ⟩ₚ
j (βₐ m) ■
where
♣ = βₐ (𝒥 [ i ]) ≤⟨ 𝕒 ⟩ ⋁[ 𝒪 A ] ⁅ βₐ i ∣ i ε 𝒥 ⁆ ＝⟨ 𝕓 ⟩ₚ j (βₐ n) ■
where
𝕒 = ⋁[ 𝒪 A ]-upper ⁅ βₐ i ∣ i ε 𝒥 ⁆ i
𝕓 = covers (𝒪 A) (Bₐ , βₐ) β-is-basis-for-A (j (βₐ n)) ⁻¹
Ⅰ = ∧[ 𝒪 A ]-left-monotone (∨[ 𝒪 A ]-left-monotone ♣)
Ⅱ = ∧[ 𝒪 A ]-right-monotone
(==>ₐ-right-monotone (𝓃₁ (𝒪 A) (nucleus-of 𝒿) (βₐ m)))
Ⅲ = ap
(λ - → (j (βₐ n) ∨[ 𝒪 A ] βₐ m) ∧[ 𝒪 A ] -)
(nucleus-heyting-implication-law (βₐ n) (βₐ m))
Ⅳ = ∧[ 𝒪 A ]-left-monotone
(∨[ 𝒪 A ]-right-monotone (𝓃₁ (𝒪 A) (nucleus-of 𝒿) (βₐ m)))
Ⅴ = ap
(λ - → - ∧[ 𝒪 A ] (j (βₐ n) ==>ₐ j (βₐ m)))
(∨[ 𝒪 A ]-is-commutative (j (βₐ n)) (j (βₐ m)))
Ⅵ = H₈ₐ (j (βₐ m)) (j (βₐ n)) ⁻¹
Ⅰ = ap
(λ - → 𝒻 ⋆∙ - ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n))
(covers (𝒪 A) (Bₐ , βₐ) β-is-basis-for-A (j (βₐ n)))
Ⅱ = ap
(λ - → - ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n))
(frame-homomorphisms-preserve-all-joins′ (𝒪 A) (𝒪 X) 𝒻 ⁅ βₐ i ∣ i ε 𝒥 ⁆)
Ⅲ = distributivity′-right (𝒪 X) (¬𝒻⋆ (βₐ n)) ⁅ 𝒻 ⋆∙ (βₐ i) ∣ i ε 𝒥 ⁆
Ⅳ = ⋁[ 𝒪 X ]-least ⁅ 𝒻 ⋆∙ (βₐ i) ∧ₓ ¬𝒻⋆ (βₐ n) ∣ i ε 𝒥 ⁆ ((⋁[ 𝒪 X ] S) , ♠)
\end{code}
The function `f⁻⁺` is monotone. This of course follows from both meet and join
preservation but I have proved it separately for reasons that I don't remember.
TODO: investigate if there was a good reason why this had to be done in a
separate proof
\begin{code}
f⁻⁺-is-monotone : is-monotonic (poset-of (𝒪 Patchₛ-A)) (poset-of (𝒪 X)) f⁻⁺
holds
f⁻⁺-is-monotone (𝒿 , 𝓀) p = cofinal-implies-join-covered (𝒪 X) 𝒮 𝒯 †
where
𝒮 : Fam 𝓤 ⟨ 𝒪 X ⟩
𝒮 = ⁅ (𝒻 ⋆∙ βₐ m) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)
∣ (m , n , p) ∶ Σ m ꞉ Bₐ , Σ n ꞉ Bₐ , 𝔏 𝒿 m n holds ⁆
𝒯 : Fam 𝓤 ⟨ 𝒪 X ⟩
𝒯 = ⁅ (𝒻 ⋆∙ βₐ m) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)
∣ (m , n , p) ∶ Σ m ꞉ Bₐ , Σ n ꞉ Bₐ , 𝔏 𝓀 m n holds ⁆
† : cofinal-in (𝒪 X) 𝒮 𝒯 holds
† (m , n , q) = ∣ (m , n , ‡) , ♣ ∣
where
open PosetReasoning (poset-of (𝒪 A))
‡ : 𝔏 𝓀 m n holds
‡ l = (‘ βₐ m ’ ∧[ 𝒪 Patchₛ-A ] ¬‘ βₖ n ’) .pr₁ (βₐ l) ≤⟨ q l ⟩
𝒿 $ (βₐ l) ≤⟨ p l ⟩
𝓀 $ (βₐ l) ■
♣ : (_ ≤[ poset-of (𝒪 X) ] _) holds
♣ = ≤-is-reflexive (poset-of (𝒪 X)) ((𝒻 ⋆∙ βₐ m) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n))
f⁻⁺ₘ : poset-of (𝒪 Patchₛ-A) ─m→ poset-of (𝒪 X)
f⁻⁺ₘ = f⁻⁺ , f⁻⁺-is-monotone
\end{code}
\begin{code}
open PatchStoneᴰ A σᴰ
Patchₛ-A-basisᴰ : basisᴰ (𝒪 Patchₛ-A)
Patchₛ-A-basisᴰ =
spectralᴰ-implies-basisᴰ Patchₛ-A patchₛ-spectralᴰ
\end{code}
Some horrible import bureaucracy below 😬
\begin{code}
open AdjointFunctorTheorem X Patchₛ-A ∣ Patchₛ-A-basisᴰ ∣
hiding (f₊-is-right-adjoint-of-f⁺)
open AdjointFunctorTheorem Patchₛ-A X X-has-basis
using ()
renaming (adjunction-inequality-forward to adjunction-inequality-forward₀)
open AdjointFunctorTheorem X A A-has-basis
using (f₊-is-right-adjoint-of-f⁺)
renaming (right-adjoint-of to right-adjoint-ofₓ;
f₊-preserves-binary-meets to f₊-preserves-binary-meetsₓ;
adjunction-inequality-forward to adjunction-inequality-forwardₓ;
adjunction-inequality-backward to adjunction-inequality-backwardₓ)
open GaloisConnectionBetween (poset-of (𝒪 Patchₛ-A)) (poset-of (𝒪 X))
open GaloisConnectionBetween (poset-of (𝒪 X)) (poset-of (𝒪 A))
using () renaming (counit to counitₓ)
open GaloisConnectionBetween (poset-of (𝒪 A)) (poset-of (𝒪 X))
using () renaming (counit to counitₐ)
\end{code}
We now define some notation that will keep coming up.
We denote by `𝒻₊` the right adjoint of `𝒻⁺`, which is monotonic map denote by
`𝒻₊ₘ`.
\begin{code}
𝒻₊ : ⟨ 𝒪 X ⟩ → ⟨ 𝒪 A ⟩
𝒻₊ = pr₁ (right-adjoint-ofₓ 𝒻)
𝒻₊ₘ : poset-of (𝒪 X) ─m→ poset-of (𝒪 A)
𝒻₊ₘ = right-adjoint-ofₓ 𝒻
\end{code}
\begin{code}
𝒻⁺ₘ : poset-of (𝒪 A) ─m→ poset-of (𝒪 X)
𝒻⁺ₘ = pr₁ 𝒻 , frame-morphisms-are-monotonic (𝒪 A) (𝒪 X) (𝒻 ⋆∙_) (pr₂ 𝒻)
\end{code}
We prove that `f⁻⁺` preserves the top element of `𝒪(Patchₛ-A)`.
\begin{code}
𝒻⁻-α : f⁻⁺ 𝟏[ 𝒪 Patchₛ-A ] ＝ 𝟏[ 𝒪 X ]
𝒻⁻-α = only-𝟏-is-above-𝟏 (𝒪 X) (f⁻⁺ 𝟏[ 𝒪 Patchₛ-A ]) †
where
open PosetReasoning (poset-of (𝒪 X))
† : (𝟏[ 𝒪 X ] ≤[ poset-of (𝒪 X) ] f⁻⁺ 𝟏[ 𝒪 Patchₛ-A ]) holds
† =
∥∥-rec
(holds-is-prop (𝟏[ 𝒪 X ] ≤[ poset-of (𝒪 X) ] f⁻⁺ 𝟏[ 𝒪 Patchₛ-A ]))
‡
(compact-opens-are-basic A A-directed-basisᴰ 𝟎[ 𝒪 A ] (𝟎-is-compact A))
where
‡ : Σ i ꞉ Bₐ , βₐ i ＝ 𝟎[ 𝒪 A ]
→ (𝟏[ 𝒪 X ] ≤[ poset-of (𝒪 X) ] f⁻⁺ 𝟏[ 𝒪 Patchₛ-A ]) holds
‡ (i , p′) =
𝟏[ 𝒪 X ] ＝⟨ Ⅰ ⟩ₚ
𝟏[ 𝒪 X ] ∧[ 𝒪 X ] 𝟏[ 𝒪 X ] ＝⟨ Ⅱ ⟩ₚ
𝒻 ⋆∙ 𝟏[ 𝒪 A ] ∧[ 𝒪 X ] 𝟏[ 𝒪 X ] ＝⟨ Ⅲ ⟩ₚ
𝒻 ⋆∙ 𝟏[ 𝒪 A ] ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ i) ≤⟨ Ⅳ ⟩
⋁[ 𝒪 X ] ⁅ 𝒻 ⋆∙ 𝟏[ 𝒪 A ] ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆ ＝⟨ refl ⟩ₚ
f⁻⁺₂ 𝟏[ 𝒪 Patchₛ-A ] ＝⟨ Ⅴ ⟩ₚ
f⁻⁺ 𝟏[ 𝒪 Patchₛ-A ] ■
where
p = p′ ⁻¹
𝕒 = heyting-implication-identity 𝟎[ 𝒪 X ] ⁻¹
𝕓 = ap
(λ - → - ==> 𝟎[ 𝒪 X ])
(frame-homomorphisms-preserve-bottom (𝒪 A) (𝒪 X) 𝒻 ⁻¹)
𝕔 = ap (λ - → (𝒻 ⋆∙ -) ==> 𝟎[ 𝒪 X ]) p
Ⅰ = ∧[ 𝒪 X ]-is-idempotent 𝟏[ 𝒪 X ]
Ⅲ = ap
(λ - → 𝒻 ⋆∙ 𝟏[ 𝒪 A ] ∧[ 𝒪 X ] -)
(𝟏[ 𝒪 X ] ＝⟨ 𝕒 ⟩
𝟎[ 𝒪 X ] ==> 𝟎[ 𝒪 X ] ＝⟨ 𝕓 ⟩
(𝒻 ⋆∙ 𝟎[ 𝒪 A ]) ==> 𝟎[ 𝒪 X ] ＝⟨ 𝕔 ⟩
(𝒻 ⋆∙ βₐ i) ==> 𝟎[ 𝒪 X ] ＝⟨ refl ⟩
¬𝒻⋆ (βₐ i) ∎)
Ⅳ = ⋁[ 𝒪 X ]-upper ⁅ 𝒻 ⋆∙ 𝟏[ 𝒪 A ] ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆ i
Ⅱ = ap
(λ - → - ∧[ 𝒪 X ] 𝟏[ 𝒪 X ])
(frame-homomorphisms-preserve-top (𝒪 A) (𝒪 X) 𝒻 ⁻¹)
Ⅴ = f⁻⁺₂-equiv-f⁻⁺₁ 𝟏[ 𝒪 Patchₛ-A ] ⁻¹
\end{code}
The function `f⁻⁺` preserves binary meets.
\begin{code}
𝒻⁻-β : preserves-binary-meets (𝒪 Patchₛ-A) (𝒪 X) f⁻⁺ holds
𝒻⁻-β 𝒿@(j , _) 𝓀@(k , _) =
f⁻⁺ (𝒿 ∧[ 𝒪 Patchₛ-A ] 𝓀)
＝⟨ Ⅰ ⟩
f⁻⁺₂ (𝒿 ∧[ 𝒪 Patchₛ-A ] 𝓀)
＝⟨ refl ⟩
⋁[ 𝒪 X ] ⁅ 𝒻 ⋆∙ (j (βₐ n) ∧[ 𝒪 A ] k (βₐ n)) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆
＝⟨ Ⅱ ⟩
⋁[ 𝒪 X ] ⁅ (𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] 𝒻 ⋆∙ k (βₐ n)) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆
＝⟨ Ⅲ ⟩
⋁[ 𝒪 X ] ⁅ (𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n))
∧[ 𝒪 X ]
(𝒻 ⋆∙ k (βₐ n) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)) ∣ n ∶ Bₐ ⁆
＝⟨ Ⅳ ⟩
⋁[ 𝒪 X ] ⁅ (𝒻 ⋆∙ j (βₐ m) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ m))
∧[ 𝒪 X ]
(𝒻 ⋆∙ k (βₐ n) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)) ∣ (m , n) ∶ Bₐ × Bₐ ⁆
＝⟨ Ⅴ ⟩
(⋁[ 𝒪 X ] ⁅ (𝒻 ⋆∙ j (βₐ n)) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆)
∧[ 𝒪 X ]
(⋁[ 𝒪 X ] ⁅ (𝒻 ⋆∙ k (βₐ n)) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆)
＝⟨ refl ⟩
f⁻⁺₂ 𝒿 ∧[ 𝒪 X ] f⁻⁺₂ 𝓀
＝⟨ Ⅵ ⟩
f⁻⁺ 𝒿 ∧[ 𝒪 X ] f⁻⁺ 𝓀
∎
where
Ⅰ = f⁻⁺₂-equiv-f⁻⁺₁ (𝒿 ∧[ 𝒪 Patchₛ-A ] 𝓀)
Ⅱ = ap
(λ - → ⋁[ 𝒪 X ] (Bₐ , -))
(dfunext fe λ n →
ap
(λ - → - ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n))
(frame-homomorphisms-preserve-meets (𝒪 A) (𝒪 X) 𝒻 (j (βₐ n)) (k (βₐ n))))
Ⅲ = ap
(λ - → ⋁[ 𝒪 X ] (Bₐ , -))
(dfunext fe λ n →
let
𝕒 = ap
(λ - → (𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] 𝒻 ⋆∙ k (βₐ n)) ∧[ 𝒪 X ] -)
(∧[ 𝒪 X ]-is-idempotent (¬𝒻⋆ (βₐ n)))
𝕓 = ∧[ 𝒪 X ]-is-associative
(𝒻 ⋆∙ j (βₐ n))
(𝒻 ⋆∙ k (βₐ n))
(¬𝒻⋆ (βₐ n) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)) ⁻¹
𝕔 = ap
(λ - → 𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] -)
(∧[ 𝒪 X ]-is-associative (𝒻 ⋆∙ k (βₐ n)) (¬𝒻⋆ (βₐ n)) (¬𝒻⋆ (βₐ n)))
𝕕 = ap
(λ - → 𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] (- ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)))
(∧[ 𝒪 X ]-is-commutative (𝒻 ⋆∙ k (βₐ n)) (¬𝒻⋆ (βₐ n)))
𝕖 = ap
(λ - → 𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] -)
(∧[ 𝒪 X ]-is-associative (¬𝒻⋆ (βₐ n)) (𝒻 ⋆∙ k (βₐ n)) (¬𝒻⋆ (βₐ n)) ⁻¹)
𝕗 = ∧[ 𝒪 X ]-is-associative
(𝒻 ⋆∙ j (βₐ n))
(¬𝒻⋆ (βₐ n))
(𝒻 ⋆∙ k (βₐ n) ∧[ 𝒪 X ] (¬𝒻⋆ (βₐ n)))
in
𝒻 ⋆∙ j (βₐ n) ∧ₓ 𝒻 ⋆∙ k (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)
＝⟨ 𝕒 ⟩
𝒻 ⋆∙ j (βₐ n) ∧ₓ 𝒻 ⋆∙ k (βₐ n) ∧ₓ (¬𝒻⋆ (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n))
＝⟨ 𝕓 ⟩
𝒻 ⋆∙ j (βₐ n) ∧ₓ (𝒻 ⋆∙ k (βₐ n) ∧ₓ (¬𝒻⋆ (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)))
＝⟨ 𝕔 ⟩
𝒻 ⋆∙ j (βₐ n) ∧ₓ (((𝒻 ⋆∙ k (βₐ n)) ∧ₓ ¬𝒻⋆ (βₐ n)) ∧ₓ ¬𝒻⋆ (βₐ n))
＝⟨ 𝕕 ⟩
𝒻 ⋆∙ j (βₐ n) ∧ₓ ((¬𝒻⋆ (βₐ n) ∧ₓ 𝒻 ⋆∙ (k (βₐ n))) ∧ₓ ¬𝒻⋆ (βₐ n))
＝⟨ 𝕖 ⟩
𝒻 ⋆∙ j (βₐ n) ∧ₓ (¬𝒻⋆ (βₐ n) ∧ₓ ((𝒻 ⋆∙ k (βₐ n)) ∧ₓ ¬𝒻⋆ (βₐ n)))
＝⟨ 𝕗 ⟩
(𝒻 ⋆∙ j (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)) ∧ₓ (𝒻 ⋆∙ k (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n))
∎)
lhs₁ = ⁅ (𝒻 ⋆∙ j (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)) ∧ₓ (𝒻 ⋆∙ k (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)) ∣ n ∶ Bₐ ⁆
rhs₁ = ⁅ (𝒻 ⋆∙ j (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ m)) ∧ₓ (𝒻 ⋆∙ k (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n))
∣ (m , n) ∶ Bₐ × Bₐ ⁆
† : cofinal-in (𝒪 X) lhs₁ rhs₁ holds
† n = ∣ (n , n) , ≤-is-reflexive (poset-of (𝒪 X)) (lhs₁ [ n ]) ∣
‡ : cofinal-in (𝒪 X) rhs₁ lhs₁ holds
‡ (m , n) = ∥∥-rec ∃-is-prop ϡ ※
where
ϡ : (Σ o ꞉ Bₐ , βₐ o ＝ βₐ m ∨[ 𝒪 A ] βₐ n)
→ ∃ o ꞉ Bₐ , (rhs₁ [ (m , n) ] ≤[ poset-of (𝒪 X) ] lhs₁ [ o ]) holds
ϡ (o , p) = ∣ o , ϟ ∣
where
𝕒₁ = ∧[ 𝒪 X ]-is-associative
(𝒻 ⋆∙ j (βₐ m))
(¬𝒻⋆ (βₐ m))
(𝒻 ⋆∙ k (βₐ n) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)) ⁻¹
𝕒₂ = ap
(λ - → 𝒻 ⋆∙ j (βₐ m) ∧[ 𝒪 X ] -)
(∧[ 𝒪 X ]-is-associative (¬𝒻⋆ (βₐ m)) (𝒻 ⋆∙ k (βₐ n)) (¬𝒻⋆ (βₐ n)))
𝕒₃ = ap
(λ - → 𝒻 ⋆∙ j (βₐ m) ∧[ 𝒪 X ] (- ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)))
(∧[ 𝒪 X ]-is-commutative (¬𝒻⋆ (βₐ m)) (𝒻 ⋆∙ k (βₐ n)))
𝕒₄ = ap
(λ - → 𝒻 ⋆∙ j (βₐ m) ∧[ 𝒪 X ] -)
(∧[ 𝒪 X ]-is-associative (𝒻 ⋆∙ k (βₐ n)) (¬𝒻⋆ (βₐ m)) (¬𝒻⋆ (βₐ n)) ⁻¹)
𝕒₅ = ∧[ 𝒪 X ]-is-associative
(𝒻 ⋆∙ j (βₐ m))
(𝒻 ⋆∙ k (βₐ n))
(¬𝒻⋆ (βₐ m) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n))
𝕒₆ = ap
(λ - → - ∧[ 𝒪 X ] (¬𝒻⋆ (βₐ m) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)))
(frame-homomorphisms-preserve-meets (𝒪 A) (𝒪 X) 𝒻 (j (βₐ m)) (k (βₐ n)) ⁻¹)
𝕒 = (𝒻 ⋆∙ j (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ m)) ∧ₓ (𝒻 ⋆∙ k (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)) ＝⟨ 𝕒₁ ⟩
𝒻 ⋆∙ j (βₐ m) ∧ₓ (¬𝒻⋆ (βₐ m) ∧ₓ (𝒻 ⋆∙ k (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n))) ＝⟨ 𝕒₂ ⟩
𝒻 ⋆∙ j (βₐ m) ∧ₓ ((¬𝒻⋆ (βₐ m) ∧ₓ 𝒻 ⋆∙ k (βₐ n)) ∧ₓ ¬𝒻⋆ (βₐ n)) ＝⟨ 𝕒₃ ⟩
𝒻 ⋆∙ j (βₐ m) ∧ₓ (𝒻 ⋆∙ (k (βₐ n)) ∧ₓ ¬𝒻⋆ (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n)) ＝⟨ 𝕒₄ ⟩
𝒻 ⋆∙ j (βₐ m) ∧ₓ (𝒻 ⋆∙ (k (βₐ n)) ∧ₓ (¬𝒻⋆ (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n))) ＝⟨ 𝕒₅ ⟩
(𝒻 ⋆∙ j (βₐ m) ∧ₓ 𝒻 ⋆∙ (k (βₐ n))) ∧ₓ (¬𝒻⋆ (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n)) ＝⟨ 𝕒₆ ⟩
(𝒻 ⋆∙ (j (βₐ m) ∧[ 𝒪 A ] k (βₐ n))) ∧ₓ (¬𝒻⋆ (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n)) ∎
𝕓₁ = j (βₐ m) ∧[ 𝒪 A ] k (βₐ n) ≤⟨ ∧[ 𝒪 A ]-lower₁ (j (βₐ m)) (k (βₐ n)) ⟩
j (βₐ m) ≤⟨ ♠ ⟩
j (βₐ m ∨[ 𝒪 A ] βₐ n) ＝⟨ ap j p ⁻¹ ⟩ₚ
j (βₐ o) ■
where
open PosetReasoning (poset-of (𝒪 A))
♠ = nuclei-are-monotone
(𝒪 A)
(nucleus-of 𝒿)
(_ , _)
(∨[ 𝒪 A ]-upper₁ (βₐ m) (βₐ n))
𝕓₂ = j (βₐ m) ∧[ 𝒪 A ] k (βₐ n) ≤⟨ ∧[ 𝒪 A ]-lower₂ (j (βₐ m)) (k (βₐ n)) ⟩
k (βₐ n) ≤⟨ ♠ ⟩
k (βₐ m ∨[ 𝒪 A ] βₐ n) ＝⟨ ap k p ⁻¹ ⟩ₚ
k (βₐ o) ■
where
open PosetReasoning (poset-of (𝒪 A))
♠ = nuclei-are-monotone
(𝒪 A)
(nucleus-of 𝓀)
(_ , _)
(∨[ 𝒪 A ]-upper₂ (βₐ m) (βₐ n))
𝕓 = ∧[ 𝒪 X ]-left-monotone
(frame-morphisms-are-monotonic
(𝒪 A)
(𝒪 X)
(pr₁ 𝒻)
(pr₂ 𝒻)
((j (βₐ m) ∧[ 𝒪 A ] k (βₐ n)) , (j (βₐ o) ∧[ 𝒪 A ] k (βₐ o)))
(∧[ 𝒪 A ]-greatest
(j (βₐ o))
(k (βₐ o))
(j (βₐ m) ∧[ 𝒪 A ] k (βₐ n))
𝕓₁
𝕓₂))
♣ : ((¬𝒻⋆ (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n)) ≤[ poset-of (𝒪 X) ] ¬𝒻⋆ (βₐ o)) holds
♣ = ¬𝒻⋆ (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n) ＝⟨ refl ⟩ₚ
((𝒻 ⋆∙ βₐ m) ==> 𝟎[ 𝒪 X ]) ∧ₓ ((𝒻 ⋆∙ βₐ n) ==> 𝟎[ 𝒪 X ]) ＝⟨ 𝟏 ⟩ₚ
((𝒻 ⋆∙ (βₐ m) ∨[ 𝒪 X ] (𝒻 ⋆∙ (βₐ n))) ==> 𝟎[ 𝒪 X ]) ＝⟨ 𝟐 ⟩ₚ
((𝒻 ⋆∙ (βₐ m ∨[ 𝒪 A ] βₐ n)) ==> 𝟎[ 𝒪 X ]) ＝⟨ 𝟑 ⟩ₚ
¬𝒻⋆ (βₐ o) ■
where
open PosetReasoning (poset-of (𝒪 X))
𝟏 = ==>-left-reverses-joins (𝒻 ⋆∙ (βₐ m)) (𝒻 ⋆∙ (βₐ n)) 𝟎[ 𝒪 X ]
𝟐 = ap
(λ - → - ==> 𝟎[ 𝒪 X ])
(frame-homomorphisms-preserve-binary-joins (𝒪 A) (𝒪 X) 𝒻 (βₐ m) (βₐ n) ⁻¹)
𝟑 = ap (λ - → (𝒻 ⋆∙ -) ==> 𝟎[ 𝒪 X ]) (p ⁻¹)
𝕔 = ∧[ 𝒪 X ]-right-monotone ♣
𝕕 = ap
(λ - → - ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ o))
(frame-homomorphisms-preserve-meets
(𝒪 A)
(𝒪 X)
𝒻
(j (βₐ o))
(k (βₐ o)))
𝕖 =
(𝒻 ⋆∙ j (βₐ o) ∧ₓ 𝒻 ⋆∙ k (βₐ o)) ∧ₓ ¬𝒻⋆ (βₐ o) ＝⟨ 𝟏 ⟩
(𝒻 ⋆∙ j (βₐ o) ∧ₓ 𝒻 ⋆∙ k (βₐ o)) ∧ₓ (¬𝒻⋆ (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o)) ＝⟨ 𝟐 ⟩
𝒻 ⋆∙ j (βₐ o) ∧ₓ (𝒻 ⋆∙ k (βₐ o) ∧ₓ (¬𝒻⋆ (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o))) ＝⟨ 𝟑 ⟩
𝒻 ⋆∙ j (βₐ o) ∧ₓ ((𝒻 ⋆∙ k (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o)) ∧ₓ ¬𝒻⋆ (βₐ o)) ＝⟨ 𝟒 ⟩
𝒻 ⋆∙ j (βₐ o) ∧ₓ ((¬𝒻⋆ (βₐ o) ∧ₓ 𝒻 ⋆∙ k (βₐ o)) ∧ₓ ¬𝒻⋆ (βₐ o)) ＝⟨ 𝟓 ⟩
𝒻 ⋆∙ j (βₐ o) ∧ₓ (¬𝒻⋆ (βₐ o) ∧ₓ (𝒻 ⋆∙ k (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o))) ＝⟨ 𝟔 ⟩
(𝒻 ⋆∙ j (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o)) ∧ₓ (𝒻 ⋆∙ k (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o)) ∎
where
𝟏 = ap
(λ - → (𝒻 ⋆∙ j (βₐ o) ∧ₓ 𝒻 ⋆∙ k (βₐ o)) ∧ₓ -)
(∧[ 𝒪 X ]-is-idempotent (¬𝒻⋆ (βₐ o)))
𝟐 = ∧[ 𝒪 X ]-is-associative
(𝒻 ⋆∙ j (βₐ o))
(𝒻 ⋆∙ k (βₐ o))
(¬𝒻⋆ (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o)) ⁻¹
𝟑 = ap
(λ - → 𝒻 ⋆∙ (j (βₐ o)) ∧ₓ -)
(∧[ 𝒪 X ]-is-associative (𝒻 ⋆∙ k (βₐ o)) (¬𝒻⋆ (βₐ o)) (¬𝒻⋆ (βₐ o)))
𝟒 = ap
(λ - → 𝒻 ⋆∙ j (βₐ o) ∧ₓ (- ∧ₓ ¬𝒻⋆ (βₐ o)))
(∧[ 𝒪 X ]-is-commutative (𝒻 ⋆∙ k (βₐ o)) (¬𝒻⋆ (βₐ o)))
𝟓 = ap
(λ - → 𝒻 ⋆∙ j (βₐ o) ∧ₓ -)
(∧[ 𝒪 X ]-is-associative (¬𝒻⋆ (βₐ o)) (𝒻 ⋆∙ k (βₐ o)) (¬𝒻⋆ (βₐ o)) ⁻¹)
𝟔 = ∧[ 𝒪 X ]-is-associative
(𝒻 ⋆∙ j (βₐ o))
(¬𝒻⋆ (βₐ o))
(𝒻 ⋆∙ k (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o))
open PosetReasoning (poset-of (𝒪 X))
ϟ = (𝒻 ⋆∙ j (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ m)) ∧ₓ (𝒻 ⋆∙ k (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)) ＝⟨ 𝕒 ⟩ₚ
(𝒻 ⋆∙ (j (βₐ m) ∧[ 𝒪 A ] k (βₐ n))) ∧ₓ (¬𝒻⋆ (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n)) ≤⟨ 𝕓 ⟩
𝒻 ⋆∙ (j (βₐ o) ∧[ 𝒪 A ] k (βₐ o)) ∧ₓ (¬𝒻⋆ (βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n)) ≤⟨ 𝕔 ⟩
𝒻 ⋆∙ (j (βₐ o) ∧[ 𝒪 A ] k (βₐ o)) ∧ₓ ¬𝒻⋆ (βₐ o) ＝⟨ 𝕕 ⟩ₚ
(𝒻 ⋆∙ j (βₐ o) ∧ₓ 𝒻 ⋆∙ k (βₐ o)) ∧ₓ ¬𝒻⋆ (βₐ o) ＝⟨ 𝕖 ⟩ₚ
(𝒻 ⋆∙ j (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o)) ∧ₓ (𝒻 ⋆∙ k (βₐ o) ∧ₓ ¬𝒻⋆ (βₐ o)) ■
ξ : is-compact-open A (βₐ m ∨[ 𝒪 A ] βₐ n) holds
ξ = compact-opens-are-closed-under-∨ A (βₐ m) (βₐ n) (κₐ m) (κₐ n)
※ : ∃ o ꞉ Bₐ , βₐ o ＝ βₐ m ∨[ 𝒪 A ] βₐ n
※ = ∥∥-rec
∃-is-prop
(λ { (o , p′) → ∣ o , p′ ∣ })
(compact-opens-are-basic A A-directed-basisᴰ (βₐ m ∨[ 𝒪 A ] βₐ n) ξ)
Ⅳ = bicofinal-implies-same-join (𝒪 X) lhs₁ rhs₁ † ‡
Ⅴ = distributivity+
(𝒪 X)
⁅ (𝒻 ⋆∙ j (βₐ n)) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆
⁅ (𝒻 ⋆∙ k (βₐ n)) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆ ⁻¹
Ⅵ = ap₂
(λ x y → x ∧[ 𝒪 X ] y)
(f⁻⁺₂-equiv-f⁻⁺₁ 𝒿 ⁻¹)
(f⁻⁺₂-equiv-f⁻⁺₁ 𝓀 ⁻¹)
\end{code}
We now proceed to the join preservation proof which requires quite a few
auxiliary definitions and lemmas.
\begin{code}
X-is-spectral : is-spectral X holds
X-is-spectral = stone-locales-are-spectral X (𝕜 , 𝕫ᴰ)
open ClosedNucleus X X-is-spectral
using ()
renaming (‘_’ to ‘_’ₓ)
\end{code}
The following function `closed-image` takes an open `X` and gives a perfect
nucleus on `A`. It is the right adjoint to the function `f⁻⁺` that we have
defined. We define this function and prove the adjunction to show that `f⁻⁺`
preserves joins using the Adjoint Functor Theorem.
\begin{code}
closed-image : ⟨ 𝒪 X ⟩ → ⟨ 𝒪 A ⟩ → ⟨ 𝒪 A ⟩
closed-image U = (𝒻₊ ∘ ‘ U ’ₓ .pr₁) ∘ 𝒻 ⋆∙_
\end{code}
The definition of this function was suggested by Igor Arrieta who also gave a
summary of the proof. Even though our proof here differs from his, the idea is
due to him.
\begin{code}
closed-image-is-inflationary : (U : ⟨ 𝒪 X ⟩) (V : ⟨ 𝒪 A ⟩)
→ (V ≤[ poset-of (𝒪 A) ] closed-image U V) holds
closed-image-is-inflationary U V =
adjunction-inequality-forwardₓ 𝒻 (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V) V †
where
† : (𝒻 ⋆∙ V ≤[ poset-of (𝒪 X) ] (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V)) holds
† = ∨[ 𝒪 X ]-upper₂ U (𝒻 ⋆∙ V)
closed-image-is-idempotent : (U : ⟨ 𝒪 X ⟩)
→ is-idempotent (𝒪 A) (closed-image U) holds
closed-image-is-idempotent U V =
let
open PosetReasoning (poset-of (𝒪 A))
in
closed-image U (closed-image U V) ＝⟨ refl ⟩ₚ
𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ (𝒻₊ (U ∨[ 𝒪 X ] (𝒻 ⋆∙ V)))) ≤⟨ † ⟩
𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V) ＝⟨ refl ⟩ₚ
closed-image U V ■
where
‡ : (𝒻 ⋆∙ 𝒻₊ (U ∨[ 𝒪 X ] (𝒻 ⋆∙ 𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V)))
≤[ poset-of (𝒪 X) ]
(U ∨[ 𝒪 X ] 𝒻 ⋆∙ V)) holds
‡ = 𝒻 ⋆∙ 𝒻₊ (U ∨[ 𝒪 X ] (𝒻 ⋆∙ 𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V))) ≤⟨ Ⅰ ⟩
U ∨[ 𝒪 X ] (𝒻 ⋆∙ 𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V)) ≤⟨ Ⅱ ⟩
U ∨[ 𝒪 X ] (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V) ＝⟨ Ⅲ ⟩ₚ
(U ∨[ 𝒪 X ] U) ∨[ 𝒪 X ] 𝒻 ⋆∙ V ＝⟨ Ⅳ ⟩ₚ
U ∨[ 𝒪 X ] 𝒻 ⋆∙ V ■
where
open PosetReasoning (poset-of (𝒪 X))
Ⅰ = counitₐ
𝒻⁺ₘ
𝒻₊ₘ
(f₊-is-right-adjoint-of-f⁺ 𝒻)
(U ∨[ 𝒪 X ] (𝒻 ⋆∙ 𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V)))
Ⅱ = ∨[ 𝒪 X ]-right-monotone
(counitₐ 𝒻⁺ₘ 𝒻₊ₘ (f₊-is-right-adjoint-of-f⁺ 𝒻) (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V))
Ⅲ = ∨[ 𝒪 X ]-assoc U U (𝒻 ⋆∙ V) ⁻¹
Ⅳ = ap (λ - → - ∨[ 𝒪 X ] 𝒻 ⋆∙ V) (∨[ 𝒪 X ]-is-idempotent U ⁻¹)
† = adjunction-inequality-forwardₓ
𝒻
(U ∨[ 𝒪 X ] 𝒻 ⋆∙ V)
(𝒻₊ (U ∨[ 𝒪 X ] (𝒻 ⋆∙ 𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V))))
‡
\end{code}
\begin{code}
closed-image-preserves-meets : (U : ⟨ 𝒪 X ⟩)
→ preserves-binary-meets
(𝒪 A)
(𝒪 A)
(closed-image U)
holds
closed-image-preserves-meets U V₁ V₂ =
𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ (V₁ ∧[ 𝒪 A ] V₂)) ＝⟨ Ⅰ ⟩
𝒻₊ (U ∨[ 𝒪 X ] (𝒻 ⋆∙ V₁ ∧[ 𝒪 X ] 𝒻 ⋆∙ V₂)) ＝⟨ Ⅱ ⟩
𝒻₊ ((U ∨[ 𝒪 X ] 𝒻 ⋆∙ V₁) ∧[ 𝒪 X ] (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V₂)) ＝⟨ Ⅲ ⟩
𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V₁) ∧[ 𝒪 A ] 𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V₂) ＝⟨ refl ⟩
closed-image U V₁ ∧[ 𝒪 A ] closed-image U V₂ ∎
where
Ⅰ = ap
(λ - → 𝒻₊ (U ∨[ 𝒪 X ] -))
(frame-homomorphisms-preserve-meets (𝒪 A) (𝒪 X) 𝒻 V₁ V₂)
Ⅱ = ap 𝒻₊ (binary-distributivity-op (𝒪 X) U (𝒻 ⋆∙ V₁) (𝒻 ⋆∙ V₂))
Ⅲ = f₊-preserves-binary-meetsₓ 𝒻 (U ∨[ 𝒪 X ] 𝒻 ⋆∙ V₁) (U ∨[ 𝒪 X ] (𝒻 ⋆∙ V₂))
\end{code}
As mentioned previously, `closed-image U` is a perfect nucleus for any `U :
𝒪(X)`. We now prove this fact.
\begin{code}
closed-image-is-nucleus : (U : ⟨ 𝒪 X ⟩)
→ is-nucleus (𝒪 A) (closed-image U) holds
closed-image-is-nucleus U = closed-image-is-inflationary U
, closed-image-is-idempotent U
, closed-image-preserves-meets U
closed-image-is-sc : (U : ⟨ 𝒪 X ⟩)
→ is-scott-continuous (𝒪 A) (𝒪 A) (closed-image U) holds
closed-image-is-sc U =
∘-of-scott-cont-is-scott-cont (𝒪 A) (𝒪 X) (𝒪 A) (𝒻₊ ∘ ‘ U ’ₓ .pr₁) (𝒻 ⋆∙_) † ‡
where
† : is-scott-continuous (𝒪 X) (𝒪 A) (𝒻₊ ∘ ‘ U ’ₓ .pr₁) holds
† = ∘-of-scott-cont-is-scott-cont
(𝒪 X)
(𝒪 X)
(𝒪 A)
𝒻₊
(‘ U ’ₓ .pr₁)
(spectral-maps-are-perfect σ 𝒻 μ)
(∨-is-scott-continuous (𝒪 X) U)
where
open PerfectMaps X A A-has-basis
‡ : is-scott-continuous (𝒪 A) (𝒪 X) (𝒻 ⋆∙_) holds
‡ = join-preserving-implies-scott-continuous
(𝒪 A)
(𝒪 X)
(𝒻 ⋆∙_)
(frame-homomorphisms-preserve-all-joins′ (𝒪 A) (𝒪 X) 𝒻)
\end{code}
\begin{code}
f⁻₊ : ⟨ 𝒪 X ⟩ → ⟨ 𝒪 Patchₛ-A ⟩
f⁻₊ U = closed-image U , closed-image-is-nucleus U , closed-image-is-sc U
\end{code}
\begin{code}
f⁻₊-is-monotone : is-monotonic (poset-of (𝒪 X)) (poset-of (𝒪 Patchₛ-A)) f⁻₊
holds
f⁻₊-is-monotone (U , V) p n = pr₂ 𝒻₊ₘ _ (∨[ 𝒪 X ]-left-monotone p)
f⁻₊ₘ : poset-of (𝒪 X) ─m→ poset-of (𝒪 Patchₛ-A)
f⁻₊ₘ = f⁻₊ , f⁻₊-is-monotone
\end{code}
\begin{code}
f⁻₊-is-right-adjoint-of-f⁻⁺ : (f⁻⁺ₘ ⊣ f⁻₊ₘ) holds
f⁻₊-is-right-adjoint-of-f⁻⁺ 𝒿@(j , _) U = ϑ₁ , ϑ₂
where
open IgorsLemma X A A-has-basis
open PerfectMaps X A A-has-basis
open HeytingComplementationLemmas X X-has-basis
ϑ₁ : (f⁻⁺ 𝒿 ≤ₓ U ⇒ 𝒿 ≤[ poset-of (𝒪 Patchₛ-A) ] (f⁻₊ U)) holds
ϑ₁ φ n =
adjunction-inequality-forwardₓ
𝒻
(U ∨[ 𝒪 X ] 𝒻 ⋆∙ (βₐ n))
(j (βₐ n))
ψ
where
open PosetReasoning (poset-of (𝒪 X))
κ′ : is-clopen₀ (𝒪 X) (𝒻 ⋆∙ (βₐ n))
κ′ = compacts-are-clopen-in-zd-locales
X
∣ 𝕫ᴰ ∣
(𝒻 ⋆∙ βₐ n)
(μ (βₐ n) (κ n))
ϟ : ((𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] ((𝒻 ⋆∙ βₐ n) ==> 𝟎[ 𝒪 X ]))
≤[ poset-of (𝒪 X) ]
U) holds
ϟ =
𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] ((𝒻 ⋆∙ βₐ n) ==> 𝟎[ 𝒪 X ]) ≤⟨ Ⅰ ⟩
f⁻⁺₂ 𝒿 ＝⟨ Ⅱ ⟩ₚ
f⁻⁺ 𝒿 ≤⟨ φ ⟩
U ■
where
Ⅰ = ⋁[ 𝒪 X ]-upper
⁅ 𝒻 ⋆∙ j (βₐ n) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆
n
Ⅱ = f⁻⁺₂-equiv-f⁻⁺₁ 𝒿 ⁻¹
※ : (𝒻 ⋆∙ j (βₐ n) ≤[ poset-of (𝒪 X) ] (𝒻 ⋆∙ βₐ n ∨[ 𝒪 X ] U)) holds
※ = negation-∨-lemma₂ κ′ ϟ
ψ : (𝒻 ⋆∙ j (βₐ n) ≤[ poset-of (𝒪 X) ] (U ∨[ 𝒪 X ] 𝒻 ⋆∙ βₐ n)) holds
ψ = 𝒻 ⋆∙ j (βₐ n) ≤⟨ ※ ⟩
𝒻 ⋆∙ (βₐ n) ∨[ 𝒪 X ] U ＝⟨ ∨[ 𝒪 X ]-is-commutative (𝒻 ⋆∙ βₐ n) U ⟩ₚ
U ∨[ 𝒪 X ] 𝒻 ⋆∙ (βₐ n) ■
S =
⁅ (𝒻 ⋆∙ βₐ m) ∧ₓ ¬𝒻⋆ (βₐ n)
∣ (m , n , p) ∶ Σ m ꞉ Bₐ , Σ n ꞉ Bₐ , 𝔏 𝒿 m n holds ⁆
ϑ₂ : (𝒿 ≤[ poset-of (𝒪 Patchₛ-A) ] (f⁻₊ U)) holds
→ (f⁻⁺ 𝒿 ≤[ poset-of (𝒪 X) ] U) holds
ϑ₂ φ = ⋁[ 𝒪 X ]-least S (U , †)
where
open Joins (λ x y → x ≤[ poset-of (𝒪 X) ] y)
open PatchConstruction A σ using (⋁ₙ; _⋏_)
† : (U is-an-upper-bound-of S) holds
† (m , n , p) = goal
where
ψ : (U : ⟨ 𝒪 A ⟩)
→ (((‘ βₐ m ’ ⋏ ¬‘ βₖ n ’) .pr₁ U) ≤[ poset-of (𝒪 A) ] j U) holds
ψ = ≼ᵏ-implies-≼ (‘ βₐ m ’ ∧[ 𝒪 Patchₛ-A ] ¬‘ βₖ n ’) 𝒿 p
κ′ : is-clopen₀ (𝒪 X) (𝒻 ⋆∙ βₐ n)
κ′ =
compacts-are-clopen-in-zd-locales X ∣ 𝕫ᴰ ∣ (𝒻 ⋆∙ βₐ n) (μ (βₐ n) (κ n))
ϡ : (T : ⟨ 𝒪 A ⟩)
→ (((𝒻 ⋆∙ (βₐ m ∨[ 𝒪 A ] T)) ∧[ 𝒪 X ] 𝒻 ⋆∙ (βₐ n ==>ₐ T))
≤[ poset-of (𝒪 X) ]
(U ∨[ 𝒪 X ] 𝒻 ⋆∙ T)) holds
ϡ T =
let
open PosetReasoning (poset-of (𝒪 X))
in
𝒻 ⋆∙ (βₐ m ∨[ 𝒪 A ] T) ∧[ 𝒪 X ] 𝒻 ⋆∙ (βₐ n ==>ₐ T) ＝⟨ Ⅰ ⟩ₚ
𝒻 ⋆∙ ((βₐ m ∨[ 𝒪 A ] T) ∧[ 𝒪 A ] (βₐ n ==>ₐ T)) ≤⟨ Ⅱ ⟩
U ∨[ 𝒪 X ] (𝒻 ⋆∙ T) ■
where
♣ : (((βₐ m ∨[ 𝒪 A ] T) ∧[ 𝒪 A ] (βₐ n ==>ₐ T))
≤[ poset-of (𝒪 A) ]
𝒻₊ (U ∨[ 𝒪 X ] (𝒻 ⋆∙ T))) holds
♣ = (βₐ m ∨[ 𝒪 A ] T) ∧[ 𝒪 A ] (βₐ n ==>ₐ T) ≤⟨ Ⅰ ⟩
j T ≤⟨ Ⅱ ⟩
𝒻₊ (U ∨[ 𝒪 X ] 𝒻 ⋆∙ T) ■
where
open PosetReasoning (poset-of (𝒪 A))
Ⅰ = ≼ᵏ-implies-≼ (‘ βₐ m ’ ∧[ 𝒪 Patchₛ-A ] ¬‘ βₖ n ’) 𝒿 p T
Ⅱ = ≼ᵏ-implies-≼ 𝒿 (f⁻₊ U) φ T
Ⅰ = frame-homomorphisms-preserve-meets
(𝒪 A)
(𝒪 X)
𝒻
(βₐ m ∨[ 𝒪 A ] T)
(βₐ n ==>ₐ T) ⁻¹
Ⅱ = adjunction-inequality-backwardₓ
𝒻
(U ∨[ 𝒪 X ] 𝒻 ⋆∙ T)
((βₐ m ∨[ 𝒪 A ] T) ∧[ 𝒪 A ] (βₐ n ==>ₐ T))
♣
ϟ : (𝒻 ⋆∙ βₐ m ≤[ poset-of (𝒪 X) ] (U ∨[ 𝒪 X ] 𝒻 ⋆∙ βₐ n)) holds
ϟ = igors-lemma-⇐ 𝒻 (βₐ m) (βₐ n) U ϡ
ϑ : (𝒻 ⋆∙ βₐ m ≤[ poset-of (𝒪 X) ] (𝒻 ⋆∙ βₐ n ∨[ 𝒪 X ] U)) holds
ϑ = 𝒻 ⋆∙ βₐ m ≤⟨ ϟ ⟩
U ∨[ 𝒪 X ] 𝒻 ⋆∙ βₐ n ＝⟨ ∨[ 𝒪 X ]-is-commutative U (𝒻 ⋆∙ βₐ n) ⟩ₚ
𝒻 ⋆∙ βₐ n ∨[ 𝒪 X ] U ■
where
open PosetReasoning (poset-of (𝒪 X))
goal : (((𝒻 ⋆∙ βₐ m) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n)) ≤[ poset-of (𝒪 X) ] U) holds
goal = negation-∨-lemma₁ κ′ ϑ
\end{code}
Proof that `f⁻⁺` preserves joins.
\begin{code}
f⁻⁺-preserves-joins : is-join-preserving (𝒪 Patchₛ-A) (𝒪 X) f⁻⁺ holds
f⁻⁺-preserves-joins = aft-forward f⁻⁺ₘ (f⁻₊ₘ , f⁻₊-is-right-adjoint-of-f⁻⁺)
open Joins (λ x y → x ≤[ poset-of (𝒪 X) ] y)
using () renaming (_is-lub-of_ to _is-lub-ofₓ_)
𝒻⁻-γ : (S : Fam 𝓤 ⟨ 𝒪 Patchₛ-A ⟩)
→ (f⁻⁺ (⋁[ 𝒪 Patchₛ-A ] S) is-lub-ofₓ ⁅ f⁻⁺ 𝒿 ∣ 𝒿 ε S ⁆) holds
𝒻⁻-γ S =
transport
(λ - → (- is-lub-ofₓ ⁅ f⁻⁺ 𝒿 ∣ 𝒿 ε S ⁆) holds)
(f⁻⁺-preserves-joins S ⁻¹)
(⋁[ 𝒪 X ]-upper ⁅ f⁻⁺ 𝒿 ∣ 𝒿 ε S ⁆ , ⋁[ 𝒪 X ]-least ⁅ f⁻⁺ 𝒿 ∣ 𝒿 ε S ⁆)
\end{code}
Now, we start working towards proving that `f⁻⁺` makes the aforementioned
diagram commute.
\begin{code}
easy-lemma : (𝒻⁻₀@(f⁻₀ , _) : X ─c→ Patchₛ-A)
→ (n : Bₐ)
→ is-boolean-complement-of (𝒪 X) (f⁻₀ ¬‘ βₖ n ’) (f⁻₀ ‘ βₐ n ’) holds
easy-lemma 𝒻⁻₀ n =
frame-homomorphisms-preserve-complements (𝒪 Patchₛ-A) (𝒪 X) 𝒻⁻₀ †
where
open PatchComplementation A σᴰ
‡ : is-boolean-complement-of (𝒪 Patchₛ-A) ¬‘ βₖ n ’ ‘ βₐ n ’ holds
‡ = open-complements-closed (βₐ n) (pr₂ (βₖ n))
† : is-boolean-complement-of (𝒪 Patchₛ-A) ‘ βₐ n ’ ¬‘ βₖ n ’ holds
† = complementation-is-symmetric (𝒪 Patchₛ-A) ¬‘ βₖ n ’ ‘ βₐ n ’ ‡
\end{code}
A corollary of the "easy lemma" is that any continuous map `𝒻⁻₀` from `X` into
`Patch-A` that makes the diagram commute also satisfies
```
𝒻⁻₀⁺ ¬‘ C ’ = ¬𝒻⁺ C ≡ 𝒻⁺ C ==> 𝟎
```
We call this lemma `commutes-with-open-nucleus`.
\begin{code}
commutes-with-open-nucleus : (𝒻⁻₀@(f⁻₀ , _) : X ─c→ Patchₛ-A)
→ ((n : Bₐ) → 𝒻 ⋆∙ (βₐ n) ＝ f⁻₀ ‘ βₐ n ’)
→ (n : Bₐ) → ¬𝒻⋆ (βₐ n) ＝ f⁻₀ ¬‘ βₖ n ’
commutes-with-open-nucleus 𝒻⁻₀@(f⁻₀ , _) ϑ n =
complements-are-unique (𝒪 X) (𝒻 ⋆∙ (βₐ n)) (¬𝒻⋆ (βₐ n)) (f⁻₀ ¬‘ βₖ n ’) φ ψ
where
open HeytingComplementationLemmas X X-has-basis
ν : is-clopen (𝒪 X) (𝒻 ⋆∙ (βₐ n)) holds
ν = compacts-are-clopen-in-zd-locales
X
∣ 𝕫ᴰ ∣
(𝒻 ⋆∙ βₐ n)
(μ (βₐ n) (κ n))
C = pr₁ ν
C-complements-𝒻⋆βn : is-boolean-complement-of (𝒪 X) C (𝒻 ⋆∙ (βₐ n)) holds
C-complements-𝒻⋆βn = pr₂ ν
φ : is-boolean-complement-of (𝒪 X) (¬𝒻⋆ (βₐ n)) (𝒻 ⋆∙ (βₐ n)) holds
φ = transport
(λ - → is-boolean-complement-of (𝒪 X) - (𝒻 ⋆∙ (βₐ n)) holds)
(complement-is-heyting-complement (𝒻 ⋆∙ (βₐ n)) C C-complements-𝒻⋆βn)
C-complements-𝒻⋆βn
ψ : is-boolean-complement-of (𝒪 X) (f⁻₀ ¬‘ βₖ n ’) (𝒻 ⋆∙ (βₐ n)) holds
ψ = transport
(λ - → is-boolean-complement-of (𝒪 X) (f⁻₀ ¬‘ βₖ n ’) - holds)
(ϑ n ⁻¹)
(easy-lemma 𝒻⁻₀ n)
\end{code}
Using `commutes-with-open-nucleus` and the `easy-lemma`, it is not hard to
prove that `𝒻⁻` makes the diagram commute.
\begin{code}
𝒻⁻-makes-the-diagram-commute : (U : ⟨ 𝒪 A ⟩) → 𝒻 ⋆∙ U ＝ f⁻⁺ ‘ U ’
𝒻⁻-makes-the-diagram-commute U = ≤-is-antisymmetric (poset-of (𝒪 X)) † ‡
where
𝟎-is-basic : is-basic A 𝟎[ 𝒪 A ] A-directed-basisᴰ holds
𝟎-is-basic = compact-opens-are-basic A A-directed-basisᴰ 𝟎[ 𝒪 A ] (𝟎-is-compact A)
ℒ : Fam 𝓤 Bₐ
ℒ = covering-index-family (𝒪 A) (Bₐ , βₐ) β-is-basis-for-A U
ℒ-covers-U : U ＝ ⋁[ 𝒪 A ] ⁅ βₐ l ∣ l ε ℒ ⁆
ℒ-covers-U = covers (𝒪 A) (Bₐ , βₐ) β-is-basis-for-A U
Ⅲ : ((⋁[ 𝒪 X ] ⁅ 𝒻 ⋆∙ (βₐ l) ∣ l ε ℒ ⁆) ≤[ poset-of (𝒪 X) ] f⁻⁺ ‘ U ’) holds
Ⅲ = ⋁[ 𝒪 X ]-least ⁅ 𝒻 ⋆∙ (βₐ l) ∣ l ε ℒ ⁆ (f⁻⁺ ‘ U ’ , ※)
where
open Joins (λ x y → x ≤[ poset-of (𝒪 A) ] y)
using () renaming (_is-lub-of_ to _is-lub-ofₐ_;
_is-an-upper-bound-of_ to _is-an-upper-bound-ofₐ_)
※ : (l : index ℒ) → (𝒻 ⋆∙ (βₐ (ℒ [ l ])) ≤[ poset-of (𝒪 X) ] f⁻⁺ ‘ U ’) holds
※ l = ∥∥-rec
(holds-is-prop (𝒻 ⋆∙ (βₐ (ℒ [ l ])) ≤[ poset-of (𝒪 X) ] f⁻⁺ ‘ U ’))
♣
𝟎-is-basic
where
♣ : Σ t ꞉ Bₐ , βₐ t ＝ 𝟎[ 𝒪 A ]
→ (𝒻 ⋆∙ βₐ (ℒ [ l ]) ≤[ poset-of (𝒪 X) ] f⁻⁺ ‘ U ’) holds
♣ (t , q) =
let
open PosetReasoning (poset-of (𝒪 X))
in
𝒻 ⋆∙ (βₐ (ℒ [ l ])) ＝⟨ 𝟏 ⟩ₚ
𝒻 ⋆∙ (βₐ (ℒ [ l ])) ∧[ 𝒪 X ] 𝟏[ 𝒪 X ] ＝⟨ 𝟐 ⟩ₚ
𝒻 ⋆∙ (βₐ (ℒ [ l ])) ∧[ 𝒪 X ] ¬𝒻⋆ 𝟎[ 𝒪 A ] ＝⟨ 𝟑 ⟩ₚ
𝒻 ⋆∙ (βₐ (ℒ [ l ])) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ t) ≤⟨ 𝟒 ⟩
f⁻⁺ ‘ U ’ ■
where
♠ = λ n →
let
open PosetReasoning (poset-of (𝒪 A))
※ = βₐ (ℒ [ l ]) ≤⟨ ⋁[ 𝒪 A ]-upper ⁅ βₐ l ∣ l ε ℒ ⁆ l ⟩
⋁[ 𝒪 A ] ⁅ βₐ l ∣ l ε ℒ ⁆ ＝⟨ ℒ-covers-U ⁻¹ ⟩ₚ
U ≤⟨ ∨[ 𝒪 A ]-upper₁ U (βₐ n) ⟩
U ∨[ 𝒪 A ] βₐ n ■
𝕒 = ap (λ - → (βₐ (ℒ [ l ]) ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 A ] (- ==>ₐ βₐ n)) q
𝕓 = ap
(λ - → (βₐ (ℒ [ l ]) ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 A ] -)
(only-𝟏-is-above-𝟏
(𝒪 A)
(𝟎[ 𝒪 A ] ==>ₐ βₐ n)
(ex-falso-quodlibetₐ (βₐ n)))
𝕔 = 𝟏-right-unit-of-∧ (𝒪 A) (βₐ (ℒ [ l ]) ∨[ 𝒪 A ] βₐ n)
𝕕 = ∨[ 𝒪 A ]-least ※ (∨[ 𝒪 A ]-upper₂ U (βₐ n))
in
(βₐ (ℒ [ l ]) ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 A ] (βₐ t ==>ₐ βₐ n) ＝⟨ 𝕒 ⟩ₚ
(βₐ (ℒ [ l ]) ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 A ] (𝟎[ 𝒪 A ] ==>ₐ βₐ n) ＝⟨ 𝕓 ⟩ₚ
(βₐ (ℒ [ l ]) ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 A ] 𝟏[ 𝒪 A ] ＝⟨ 𝕔 ⟩ₚ
βₐ (ℒ [ l ]) ∨[ 𝒪 A ] βₐ n ≤⟨ 𝕕 ⟩
U ∨[ 𝒪 A ] βₐ n ■
𝟏 = 𝟏-right-unit-of-∧ (𝒪 X) (𝒻 ⋆∙ (βₐ (ℒ [ l ]))) ⁻¹
𝟐 = ap (λ - → 𝒻 ⋆∙ βₐ (ℒ [ l ]) ∧[ 𝒪 X ] -) (¬𝒻⋆𝟎-is-𝟏 ⁻¹)
𝟑 = ap (λ - → 𝒻 ⋆∙ βₐ (ℒ [ l ]) ∧[ 𝒪 X ] ¬𝒻⋆ -) (q ⁻¹)
𝟒 = ⋁[ 𝒪 X ]-upper
⁅ 𝒻 ⋆∙ βₐ m ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ (m , n , p) ∶ below ‘ U ’ ⁆
(ℒ [ l ] , t , ♠)
† : (𝒻 ⋆∙ U ≤[ poset-of (𝒪 X) ] f⁻⁺ ‘ U ’) holds
† =
let
open PosetReasoning (poset-of (𝒪 X))
in
𝒻 ⋆∙ U ＝⟨ Ⅰ ⟩ₚ
𝒻 ⋆∙ (⋁[ 𝒪 A ] ⁅ βₐ l ∣ l ε ℒ ⁆) ＝⟨ Ⅱ ⟩ₚ
⋁[ 𝒪 X ] ⁅ 𝒻 ⋆∙ (βₐ l) ∣ l ε ℒ ⁆ ≤⟨ Ⅲ ⟩
f⁻⁺ ‘ U ’ ■
where
Ⅰ = ap (𝒻 ⋆∙_) ℒ-covers-U
Ⅱ = frame-homomorphisms-preserve-all-joins′ (𝒪 A) (𝒪 X) 𝒻 ⁅ βₐ l ∣ l ε ℒ ⁆
‡ : (f⁻⁺ ‘ U ’ ≤[ poset-of (𝒪 X) ] 𝒻 ⋆∙ U) holds
‡ = f⁻⁺ ‘ U ’ ＝⟨ f⁻⁺₂-equiv-f⁻⁺₁ ‘ U ’ ⟩ₚ
f⁻⁺₂ ‘ U ’ ≤⟨ ※ ⟩
𝒻 ⋆∙ U ■
where
open PosetReasoning (poset-of (𝒪 X))
ϟ : (n : Bₐ)
→ ((𝒻 ⋆∙ (U ∨[ 𝒪 A ] βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)) ≤ₓ 𝒻 ⋆∙ U) holds
ϟ n =
𝒻 ⋆∙ (U ∨[ 𝒪 A ] βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n) ＝⟨ 𝟏 ⟩ₚ
(𝒻 ⋆∙ U ∨[ 𝒪 X ] 𝒻 ⋆∙ βₐ n) ∧ₓ ((𝒻 ⋆∙ (βₐ n)) ==> 𝟎[ 𝒪 X ]) ＝⟨ 𝟐 ⟩ₚ
(𝒻 ⋆∙ U ∧ₓ ¬𝒻⋆ (βₐ n)) ∨[ 𝒪 X ] (𝒻 ⋆∙ (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)) ≤⟨ 𝟑 ⟩
𝒻 ⋆∙ U ∨[ 𝒪 X ] (𝒻 ⋆∙ (βₐ n) ∧ₓ ¬𝒻⋆ (βₐ n)) ≤⟨ 𝟒 ⟩
(𝒻 ⋆∙ U) ∨[ 𝒪 X ] 𝟎[ 𝒪 X ] ＝⟨ 𝟓 ⟩ₚ
𝒻 ⋆∙ U ■
where
𝟏 = ap
(λ - → - ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n))
(frame-homomorphisms-preserve-binary-joins (𝒪 A) (𝒪 X) 𝒻 U (βₐ n))
𝟐 = binary-distributivity-right (𝒪 X)
𝟑 = ∨[ 𝒪 X ]-left-monotone
(∧[ 𝒪 X ]-lower₁
(𝒻 ⋆∙ U)
((𝒻 ⋆∙ βₐ n) ==> 𝟎[ 𝒪 X ]))
𝟒 = ∨[ 𝒪 X ]-right-monotone (mp-left (𝒻 ⋆∙ βₐ n) 𝟎[ 𝒪 X ])
𝟓 = 𝟎-left-unit-of-∨ (𝒪 X) (𝒻 ⋆∙ U)
※ = ⋁[ 𝒪 X ]-least
⁅ 𝒻 ⋆∙ (U ∨[ 𝒪 A ] βₐ n) ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ n) ∣ n ∶ Bₐ ⁆
(𝒻 ⋆∙ U , ϟ)
\end{code}
We now package up the function `f⁻` with the proof that it's a continuous map.
\begin{code}
𝒻⁻⁺ : X ─c→ Patchₛ-A
𝒻⁻⁺ = f⁻⁺ , 𝒻⁻-α , 𝒻⁻-β , 𝒻⁻-γ
\end{code}
\section{Uniqueness}
First, the extensional equality which is the main content of the uniqueness
proof.
\begin{code}
𝒻⁻-is-unique-ext : (𝒻⁻₀@(f⁻₀ , _) : X ─c→ Patchₛ-A)
→ (((U : ⟨ 𝒪 A ⟩) → 𝒻 ⋆∙ U ＝ f⁻₀ ‘ U ’) )
→ (𝒿 : ⟨ 𝒪 Patchₛ-A ⟩) → f⁻⁺ 𝒿 ＝ f⁻₀ 𝒿
𝒻⁻-is-unique-ext 𝒻⁻₀@(f⁻₀ , _) ϑ 𝒿 =
f⁻⁺ 𝒿 ＝⟨ Ⅰ ⟩
f⁻⁺ (⋁ₙ ⁅ (𝔠 k) ⋏ (𝔬 l) ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆) ＝⟨ Ⅱ ⟩
⋁[ 𝒪 X ] ⁅ f⁻⁺ (𝔠 k ⋏ 𝔬 l) ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆ ＝⟨ Ⅲ ⟩
⋁[ 𝒪 X ] ⁅ f⁻⁺ (𝔠 k) ∧ₓ f⁻⁺ (𝔬 l) ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆ ＝⟨ Ⅳ ⟩
⋁[ 𝒪 X ] ⁅ f⁻⁺ (𝔠 k) ∧ₓ ¬𝒻⋆ (βₐ l) ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆ ＝⟨ Ⅴ ⟩
⋁[ 𝒪 X ] ⁅ 𝒻 ⋆∙ (βₐ k) ∧ₓ ¬𝒻⋆ (βₐ l) ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆ ＝⟨ Ⅵ ⟩
⋁[ 𝒪 X ] ⁅ 𝒻 ⋆∙ (βₐ k) ∧ₓ f⁻₀ (𝔬 l) ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆ ＝⟨ Ⅶ ⟩
⋁[ 𝒪 X ] ⁅ f⁻₀ (𝔠 k) ∧ₓ f⁻₀ (𝔬 l) ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆ ＝⟨ Ⅷ ⟩
⋁[ 𝒪 X ] ⁅ f⁻₀ (𝔠 k ⋏ 𝔬 l) ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆ ＝⟨ Ⅸ ⟩
f⁻₀ (⋁ₙ ⁅ 𝔠 k ⋏ 𝔬 l ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆) ＝⟨ Ⅹ ⟩
f⁻₀ 𝒿 ∎
where
open BasisOfPatch A σᴰ hiding (σ)
open PatchConstruction A σ using (⋁ₙ; _⋏_)
ν : 𝒿 ＝ ⋁[ 𝒪 Patchₛ-A ] ⁅ 𝔠 k ⋏ 𝔬 l ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆
ν = main-covering-lemma 𝒿
Ⅰ = ap f⁻⁺ ν
Ⅱ = ⋁[ 𝒪 X ]-unique
⁅ f⁻⁺ (𝔠 k ∧[ 𝒪 Patchₛ-A ] 𝔬 l) ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆
(f⁻⁺ (⋁[ 𝒪 Patchₛ-A ] ⁅ 𝔠 k ⋏ 𝔬 l ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆))
(𝒻⁻-γ ⁅ 𝔠 k ∧[ 𝒪 Patchₛ-A ] 𝔬 l ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆)
Ⅲ = ap
(λ - → ⋁[ 𝒪 X ] (basic-below 𝒿 , -))
(dfunext fe (λ { ((k , l) , p) → 𝒻⁻-β (𝔠 k) (𝔬 l) }))
ctx = λ - → ⋁[ 𝒪 X ] (basic-below 𝒿 , -)
Ⅳ = ap
ctx
(dfunext fe (λ { ((k , l) , p) →
ap
(λ - → (f⁻⁺ (𝔠 k)) ∧[ 𝒪 X ] -)
(commutes-with-open-nucleus 𝒻⁻⁺ ※ l ⁻¹) }))
where
※ = 𝒻⁻-makes-the-diagram-commute ∘ βₐ
Ⅴ = ap
ctx
((dfunext fe (λ { ((k , l) , p) →
ap
(λ - → - ∧[ 𝒪 X ] ¬𝒻⋆ (βₐ l))
(𝒻⁻-makes-the-diagram-commute (βₐ k) ⁻¹) })))
Ⅵ = ap
ctx
(dfunext fe λ { ((k , l) , p) →
ap
(λ - → 𝒻 ⋆∙ (βₐ k) ∧[ 𝒪 X ] -)
(commutes-with-open-nucleus 𝒻⁻₀ (ϑ ∘ βₐ) l) })
Ⅶ = ap
ctx
(dfunext fe λ { ((k , l) , p) →
ap
(λ - → - ∧[ 𝒪 X ] f⁻₀ (𝔬 l))
(ϑ (βₐ k)) })
Ⅷ = ap
ctx
(dfunext fe λ { ((k , l) , p) →
frame-homomorphisms-preserve-meets
(𝒪 Patchₛ-A)
(𝒪 X)
𝒻⁻₀
(𝔠 k)
(𝔬 l) ⁻¹ } )
Ⅸ = frame-homomorphisms-preserve-all-joins′
(𝒪 Patchₛ-A)
(𝒪 X)
𝒻⁻₀
⁅ 𝔠 k ∧[ 𝒪 Patchₛ-A ] 𝔬 l ∣ ((k , l) , _) ∶ basic-below 𝒿 ⁆ ⁻¹
Ⅹ = ap f⁻₀ ν ⁻¹
𝒻⁻-is-unique : is-central
(Σ 𝒻⁻₀ ꞉ (X ─c→ Patchₛ-A) ,
((U : ⟨ 𝒪 A ⟩) → 𝒻 .pr₁ U ＝ 𝒻⁻₀ .pr₁ ‘ U ’))
((f⁻⁺ , 𝒻⁻-α , 𝒻⁻-β , 𝒻⁻-γ) , 𝒻⁻-makes-the-diagram-commute)
𝒻⁻-is-unique (𝒻⁻₀@(f⁻₀ , _ , _ , 𝒻⁻₀-γ) , ϑ) =
to-subtype-＝ ※ (to-subtype-＝ γ (dfunext fe †))
where
※ : (𝒻⁻₀ : X ─c→ Patchₛ-A)
→ is-prop ((U : ⟨ 𝒪 A ⟩) → 𝒻 .pr₁ U ＝ 𝒻⁻₀ .pr₁ ‘ U ’)
※ 𝒻⁻₀ = Π-is-prop fe λ _ → carrier-of-[ poset-of (𝒪 X) ]-is-set
γ : (ℊ⁻ : ⟨ 𝒪 Patchₛ-A ⟩ → ⟨ 𝒪 X ⟩)
→ is-prop (is-a-frame-homomorphism (𝒪 Patchₛ-A) (𝒪 X) ℊ⁻ holds)
γ ℊ⁻ = holds-is-prop (is-a-frame-homomorphism (𝒪 Patchₛ-A) (𝒪 X) ℊ⁻)
open HeytingComplementationLemmas X X-has-basis
open BasisOfPatch A σᴰ
† : (𝒿 : ⟨ 𝒪 Patchₛ-A ⟩) → f⁻⁺ 𝒿 ＝ f⁻₀ 𝒿
† = 𝒻⁻-is-unique-ext 𝒻⁻₀ ϑ
proof-of-ump : ∃! 𝒻⁻ ꞉ (X ─c→ Patchₛ-A) , ((U : ⟨ 𝒪 A ⟩) → 𝒻 ⋆∙ U ＝ 𝒻⁻ .pr₁ ‘ U ’)
proof-of-ump =
((f⁻⁺ , 𝒻⁻-α , 𝒻⁻-β , 𝒻⁻-γ) , 𝒻⁻-makes-the-diagram-commute) , 𝒻⁻-is-unique
ump-of-patch : {𝓤 : Universe}
→ (A : Locale (𝓤 ⁺) 𝓤 𝓤)
→ (σ : is-spectral A holds)
→ (sk : has-small-𝒦 A)
→ (X : Locale (𝓤 ⁺) 𝓤 𝓤)
→ is-stone X holds
→ (𝒻@(f , _) : X ─c→ A)
→ is-spectral-map A X 𝒻 holds
→ let
σ′ : spectralᴰ A
σ′ = spectral-and-small-𝒦-implies-spectralᴰ A σ sk
open PatchConstruction A σ renaming (Patch to Patch-A)
open ClosedNucleus A σ
open OpenNucleus A σ′
in
∃! 𝒻⁻ ꞉ X ─c→ Patch-A , ((U : ⟨ 𝒪 A ⟩) → f U ＝ 𝒻⁻ .pr₁ ‘ U ’)
ump-of-patch {𝓤} A σ sk X 𝕤 𝒻 μ = ∥∥-rec₂ (being-singleton-is-prop fe) γ ∣ σ′ ∣ (pr₂ 𝕤)
where
σ′ : spectralᴰ A
σ′ = spectral-and-small-𝒦-implies-spectralᴰ A σ sk
open PatchConstruction A σ renaming (Patch to Patch-A)
open ClosedNucleus A σ
open OpenNucleus A σ′
γ : spectralᴰ A
→ zero-dimensionalᴰ (𝒪 X)
→ ∃! 𝒻⁻ ꞉ (X ─c→ Patch-A) , ((U : ⟨ 𝒪 A ⟩) → 𝒻 .pr₁ U ＝ 𝒻⁻ .pr₁ ‘ U ’)
γ σᴰ 𝕫ᴰ = (𝒻⁻₀ , 𝒻⁻-makes-the-diagram-commute) , 𝔠
where
open UniversalProperty A X σᴰ 𝕫ᴰ (pr₁ 𝕤) 𝒻 μ
open SmallPatchConstruction A σᴰ renaming (SmallPatch to Patchₛ-A)
𝒻⁻₀ : X ─c→ Patch-A
𝒻⁻₀ = f⁻⁺ , 𝒻⁻-α , 𝒻⁻-β , 𝒻⁻-γ
𝔠 : is-central
((Σ 𝒻⁻₀ ꞉ (X ─c→ Patch-A) , ((U : ⟨ 𝒪 A ⟩) → 𝒻 .pr₁ U ＝ 𝒻⁻₀ .pr₁ ‘ U ’)))
(𝒻⁻₀ , 𝒻⁻-makes-the-diagram-commute)
𝔠 (𝒻⁻₁@(f⁻₁ , α₁ , β₁ , γ₁) , p) =
to-subtype-＝ ♣ (to-subtype-＝ ♠ (dfunext fe (𝒻⁻-is-unique-ext 𝒻⁻₁′ p)))
where
open Joins (λ x y → x ≤[ poset-of (𝒪 X) ] y)
open PosetReasoning (poset-of (𝒪 X))
𝒻⁻₁′ : X ─c→ Patchₛ-A
𝒻⁻₁′ = f⁻₁ , α₁ , β₁ , γ₁′
where
γ₁′ : (S : Fam 𝓤 ⟨ 𝒪 Patchₛ-A ⟩)
→ (f⁻₁ (⋁[ 𝒪 Patchₛ-A ] S) is-lub-of ⁅ f⁻₁ U ∣ U ε S ⁆) holds
γ₁′ S = † , ‡
where
† = λ i →
meet-preserving-implies-monotone
(𝒪 Patchₛ-A)
(𝒪 X)
f⁻₁
β₁
(_ , _)
(⋁[ 𝒪 Patchₛ-A ]-upper S i)
open Joins _≼ᵏ_
using ()
renaming (_is-an-upper-bound-of_ to _is-an-upper-bound-ofₙ_)
open Joins _≼_
using ()
renaming (_is-an-upper-bound-of_ to _is-an-upper-bound-ofₖ_)
φ : ⋁[ 𝒪 Patchₛ-A ] S ＝ ⋁[ 𝒪 Patch-A ] S
φ = ≤-is-antisymmetric (poset-of (𝒪 Patchₛ-A)) φ₁ φ₂
where
ψ₁ : ((⋁[ 𝒪 Patchₛ-A ] S) is-an-upper-bound-ofₙ S) holds
ψ₁ i = ≼-implies-≼ᵏ
(S [ i ])
(⋁[ 𝒪 Patch-A ] S)
(⋁[ 𝒪 Patch-A ]-upper S i)
φ₁ : ((⋁[ 𝒪 Patchₛ-A ] S) ≼ᵏ (⋁[ 𝒪 Patch-A ] S)) holds
φ₁ = ⋁[ 𝒪 Patchₛ-A ]-least S ((⋁[ 𝒪 Patch-A ] S) , ψ₁)
ψ₂ : ((⋁[ 𝒪 Patch-A ] S) is-an-upper-bound-ofₖ S) holds
ψ₂ i = ≼ᵏ-implies-≼
(S [ i ])
(⋁[ 𝒪 Patchₛ-A ] S)
(⋁[ 𝒪 Patchₛ-A ]-upper S i)
φ₂ : ((⋁[ 𝒪 Patch-A ] S) ≼ᵏ (⋁[ 𝒪 Patchₛ-A ] S)) holds
φ₂ = ⋁[ 𝒪 Patch-A ]-least S ((⋁[ 𝒪 Patchₛ-A ] S) , ψ₂) ∘ βₐ
‡ : ((U , _) : upper-bound ⁅ f⁻₁ U ∣ U ε S ⁆)
→ (f⁻₁ (⋁[ 𝒪 Patchₛ-A ] S) ≤ₓ U) holds
‡ (U , p) = f⁻₁ (⋁[ 𝒪 Patchₛ-A ] S) ＝⟨ ap (𝒻⁻₁ .pr₁) φ ⟩ₚ
f⁻₁ (⋁[ 𝒪 Patch-A ] S) ≤⟨ pr₂ (γ₁ S) (U , p) ⟩
U ■
♣ : (𝒻⁻₂ : X ─c→ Patch-A)
→ is-prop ((U : ⟨ 𝒪 A ⟩) → 𝒻 .pr₁ U ＝ 𝒻⁻₂ .pr₁ ‘ U ’)
♣ 𝒻⁻₂ = Π-is-prop fe (λ _ → carrier-of-[ poset-of (𝒪 X) ]-is-set)
♠ : (𝒻⁻₂ : ⟨ 𝒪 Patch-A ⟩ → ⟨ 𝒪 X ⟩)
→ is-prop (is-a-frame-homomorphism (𝒪 Patch-A) (𝒪 X) 𝒻⁻₂ holds)
♠ = holds-is-prop ∘ is-a-frame-homomorphism (𝒪 Patch-A) (𝒪 X)
ϟ : (𝒿 : ⟨ 𝒪 Patch-A ⟩) → f⁻⁺ 𝒿 ＝ f⁻₁ 𝒿
ϟ = 𝒻⁻-is-unique-ext 𝒻⁻₁′ p
\end{code}