FrameIsomorphism-Definition
-------------------------------------------------------------------------------- title: Frame isomorphisms author: Ayberk Tosun date-started: 2024-04-11 date-completed: 2024-04-18 -------------------------------------------------------------------------------- Various formulations of the notion of frame isomorphism, and proofs of their equivalences.{-# OPTIONS --safe --without-K #-} open import MLTT.Spartan hiding (𝟚; ₀; ₁) open import UF.FunExt open import UF.PropTrunc module Locales.ContinuousMap.FrameIsomorphism-Definition (pt : propositional-truncations-exist) (fe : Fun-Ext) where open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe open import Locales.ContinuousMap.FrameHomomorphism-Properties pt fe open import Locales.Frame pt fe open import UF.Equiv open import UF.Equiv-FunExt open import UF.Logic open import UF.Retracts open import UF.Subsingletons open import UF.Subsingletons-FunExt open import UF.SubtypeClassifier open AllCombinators pt fe open FrameHomomorphismProperties open FrameHomomorphismsWe work in a module parameterized by two frames `F` and `G`.module FrameIsomorphisms (F : Frame 𝓤 𝓥 𝓦) (G : Frame 𝓤' 𝓥' 𝓦) whereWe start with the record-based definition of the notion of frame isomorphism.record Isomorphismᵣ : 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓥' ⊔ 𝓦 ⁺ ̇ where field 𝓈 : F ─f→ G 𝓇 : G ─f→ F s : ⟨ F ⟩ → ⟨ G ⟩ s = fun F G 𝓈 r : ⟨ G ⟩ → ⟨ F ⟩ r = fun G F 𝓇 s-is-homomorphism : is-a-frame-homomorphism F G s holds s-is-homomorphism = fun-is-a-frame-homomorphism F G 𝓈 r-is-homomorphism : is-a-frame-homomorphism G F r holds r-is-homomorphism = fun-is-a-frame-homomorphism G F 𝓇 field 𝓇-cancels-𝓈 : r ∘ s ∼ id 𝓈-cancels-𝓇 : s ∘ r ∼ idWe now show the equivalence of this to a Σ-based definition. Given a frame homomorphism `F ─f→ G`, its type of homomorphic inverses is a proposition.homomorphic-inverse : (F ─f→ G) → 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓦 ⁺ ̇ homomorphic-inverse s = Σ r ꞉ (G ─f→ F) , fun F G s ∘ fun G F r ∼ id × fun G F r ∘ fun F G s ∼ id homomorphic-inverse-is-prop : (h : F ─f→ G) → is-prop (homomorphic-inverse h) homomorphic-inverse-is-prop h (r , φ , ψ) (r′ , φ′ , ψ′) = to-subtype-＝ † (to-frame-homomorphism-＝ G F r r′ ‡) where † : (h′ : G ─f→ F) → is-prop (fun F G h ∘ fun G F h′ ∼ id × fun G F h′ ∘ fun F G h ∼ id) † h′ = ×-is-prop (Π-is-prop fe (λ _ → carrier-of-[ poset-of G ]-is-set)) (Π-is-prop fe (λ _ → carrier-of-[ poset-of F ]-is-set)) ϑ : fun F G h ∘ fun G F r ∼ fun F G h ∘ fun G F r′ ϑ y = fun F G h (fun G F r y) ＝⟨ Ⅰ ⟩ y ＝⟨ Ⅱ ⟩ fun F G h (fun G F r′ y) ∎ where Ⅰ = φ y Ⅱ = φ′ y ⁻¹ ξ : left-cancellable (fun F G h) ξ = sections-are-lc (fun F G h) (fun G F r , ψ) ‡ : (y : ⟨ G ⟩) → fun G F r y ＝ fun G F r′ y ‡ y = ξ (ϑ y)To say that a frame homomorphism is an isomorphism is to say that its type of homomorphic inverses is inhabited.is-isomorphism : (F ─f→ G) → Ω (𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓦 ⁺) is-isomorphism h = homomorphic-inverse h , homomorphic-inverse-is-prop hWe define the type of isomorphisms between frames `F` and `G` accordingly.Isomorphism : 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓥' ⊔ 𝓦 ⁺ ̇ Isomorphism = Σ h ꞉ F ─f→ G , is-isomorphism h holdsIt is immediate that `Isomorphism` and `Isomorphismᵣ` are equivalent types.isomorphism-to-isomorphismᵣ : Isomorphism → Isomorphismᵣ isomorphism-to-isomorphismᵣ (𝓈 , 𝓇 , φ , ψ) = record { 𝓈 = 𝓈 ; 𝓇 = 𝓇 ; 𝓇-cancels-𝓈 = ψ ; 𝓈-cancels-𝓇 = φ } isomorphismᵣ-to-isomorphism : Isomorphismᵣ → Isomorphism isomorphismᵣ-to-isomorphism iso = let open Isomorphismᵣ iso in 𝓈 , 𝓇 , 𝓈-cancels-𝓇 , 𝓇-cancels-𝓈 isomorphism-equiv-to-isomorphismᵣ : Isomorphism ≃ Isomorphismᵣ isomorphism-equiv-to-isomorphismᵣ = isomorphism-to-isomorphismᵣ , (isomorphismᵣ-to-isomorphism , λ _ → refl) , (isomorphismᵣ-to-isomorphism , λ _ → refl)We now give an alternative definition of the same notion, which is more convenient to use for the SIP. The predicate `is-homomorphic` below expresses what it means for an equivalence between the carrier sets of `F` and `G` to be homomorphic.is-homomorphic : (⟨ F ⟩ ≃ ⟨ G ⟩) → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓤' ⊔ 𝓥' ⊔ 𝓦 ⁺) is-homomorphic e = is-a-frame-homomorphism F G ⌜ e ⌝ ∧ is-a-frame-homomorphism G F (e⁻¹ (⌜⌝-is-equiv e)) where e⁻¹ = inverse ⌜ e ⌝The type of isomorphisms between `F` and `G` could alternatively be defined as the type of homomorphic equivalences.Isomorphism₀ : 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓥' ⊔ 𝓦 ⁺ ̇ Isomorphism₀ = Σ e ꞉ ⟨ F ⟩ ≃ ⟨ G ⟩ , is-homomorphic e holdsThese two notions of frame isomorphism are equivalent.isomorphismᵣ-to-isomorphism₀ : Isomorphismᵣ → Isomorphism₀ isomorphismᵣ-to-isomorphism₀ iso = (s , † , ‡) , φ , ψ where open Isomorphismᵣ iso † : has-section s † = r , 𝓈-cancels-𝓇 ‡ : is-section s ‡ = r , 𝓇-cancels-𝓈 φ : is-a-frame-homomorphism F G s holds φ = fun-is-a-frame-homomorphism F G 𝓈 ψ : is-a-frame-homomorphism G F r holds ψ = fun-is-a-frame-homomorphism G F 𝓇 isomorphism₀-to-isomorphismᵣ : Isomorphism₀ → Isomorphismᵣ isomorphism₀-to-isomorphismᵣ (e , φ , ψ) = record { 𝓈 = ⌜ e ⌝ , φ ; 𝓇 = inverse ⌜ e ⌝ (⌜⌝-is-equiv e) , ψ ; 𝓇-cancels-𝓈 = inverses-are-retractions ⌜ e ⌝ (⌜⌝-is-equiv e) ; 𝓈-cancels-𝓇 = inverses-are-sections ⌜ e ⌝ (⌜⌝-is-equiv e) } isomorphism-to-isomorphism₀ : Isomorphism → Isomorphism₀ isomorphism-to-isomorphism₀ = isomorphismᵣ-to-isomorphism₀ ∘ isomorphism-to-isomorphismᵣ isomorphism₀-to-isomorphism : Isomorphism₀ → Isomorphism isomorphism₀-to-isomorphism = isomorphismᵣ-to-isomorphism ∘ isomorphism₀-to-isomorphismᵣ isomorphism-equivalent-to-isomorphism₀ : Isomorphism ≃ Isomorphism₀ isomorphism-equivalent-to-isomorphism₀ = isomorphism-to-isomorphism₀ , (isomorphism₀-to-isomorphism , †) , (isomorphism₀-to-isomorphism , ‡) where † : isomorphism-to-isomorphism₀ ∘ isomorphism₀-to-isomorphism ∼ id † (h , _) = to-subtype-＝ (holds-is-prop ∘ is-homomorphic) (to-subtype-＝ (being-equiv-is-prop (λ 𝓤 𝓥 → fe {𝓤} {𝓥})) refl) ‡ : isomorphism₀-to-isomorphism ∘ isomorphism-to-isomorphism₀ ∼ id ‡ iso = to-subtype-＝ (holds-is-prop ∘ is-isomorphism) refl isomorphismᵣ-equivalent-to-isomorphism₀ : Isomorphismᵣ ≃ Isomorphism₀ isomorphismᵣ-equivalent-to-isomorphism₀ = Isomorphismᵣ ≃⟨ Ⅰ ⟩ Isomorphism ≃⟨ Ⅱ ⟩ Isomorphism₀ ■ where Ⅰ = ≃-sym isomorphism-equiv-to-isomorphismᵣ Ⅱ = isomorphism-equivalent-to-isomorphism₀Some nice syntax for frame isomorphisms.Isomorphismᵣ-Syntax : Frame 𝓤 𝓥 𝓦 → Frame 𝓤' 𝓥' 𝓦 → 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓥' ⊔ 𝓦 ⁺ ̇ Isomorphismᵣ-Syntax = FrameIsomorphisms.Isomorphismᵣ infix 0 Isomorphismᵣ-Syntax syntax Isomorphismᵣ-Syntax F G = F ≅f≅ GAdded on 2024-04-14. We denote by `𝔦𝔡` the identity equivalence on the carrier set of a frame.𝔦𝔡 : (L : Frame 𝓤 𝓥 𝓦) → ⟨ L ⟩ ≃ ⟨ L ⟩ 𝔦𝔡 L = ≃-refl ⟨ L ⟩The proof that `𝔦𝔡` preserves the top element and meets is definitional.𝔦𝔡-preserves-top : (L : Frame 𝓤 𝓥 𝓦) → preserves-top L L ⌜ 𝔦𝔡 L ⌝ holds 𝔦𝔡-preserves-top L = refl 𝔦𝔡-preserves-binary-meets : (L : Frame 𝓤 𝓥 𝓦) → preserves-binary-meets L L ⌜ 𝔦𝔡 L ⌝ holds 𝔦𝔡-preserves-binary-meets _ _ _ = reflThe fact that it preserves joins is also direct.𝔦𝔡-preserves-joins : (L : Frame 𝓤 𝓥 𝓦) → preserves-joins L L ⌜ 𝔦𝔡 L ⌝ holds 𝔦𝔡-preserves-joins L S = † , ‡ where open Joins (λ x y → x ≤[ poset-of L ] y) † : ((⋁[ L ] S) is-an-upper-bound-of S) holds † = ⋁[ L ]-upper S ‡ : ((u , _) : upper-bound S) → ((⋁[ L ] S) ≤[ poset-of L ] u) holds ‡ = ⋁[ L ]-least SWe package these up together into the proof `𝔦𝔡-is-frame-homomorphism`, and denote this frame homomorphism by `𝔦𝔡ₕ`.𝔦𝔡-is-frame-homomorphism : (L : Frame 𝓤 𝓥 𝓦) → is-a-frame-homomorphism L L ⌜ 𝔦𝔡 L ⌝ holds 𝔦𝔡-is-frame-homomorphism L = 𝔦𝔡-preserves-top L , 𝔦𝔡-preserves-binary-meets L , 𝔦𝔡-preserves-joins L 𝔦𝔡ₕ : (L : Frame 𝓤 𝓥 𝓦) → L ─f·→ L 𝔦𝔡ₕ L = frame-homomorphism-to-frame-homomorphismᵣ L L (⌜ 𝔦𝔡 L ⌝ , 𝔦𝔡-is-frame-homomorphism L)Finally, we record the fact that the identity equivalence is a homomorphic equivalence.𝔦𝔡-is-homomorphic : (L : Frame 𝓤 𝓥 𝓦) → FrameIsomorphisms.is-homomorphic L L (𝔦𝔡 L) holds 𝔦𝔡-is-homomorphic L = 𝔦𝔡-is-frame-homomorphism L , 𝔦𝔡-is-frame-homomorphism L