---
title: Isomorphisms of distributive lattices
author: Ayberk Tosun
date-started: 2024-04-24
dates-updated: [2024-06-17, 2024-05-30, 2024-06-01]
---
This module contains the definition of the notion of distributive lattice
isomorphism.
\begin{code}
{-# OPTIONS --safe --without-K #-}
open import UF.FunExt
open import UF.PropTrunc
module Locales.DistributiveLattice.Isomorphism
(fe : Fun-Ext)
(pt : propositional-truncations-exist)
where
open import Locales.AdjointFunctorTheoremForFrames pt fe
open import Locales.Adjunctions.Properties pt fe
open import Locales.Adjunctions.Properties-DistributiveLattice pt fe
open import Locales.DistributiveLattice.Definition fe pt
open import Locales.DistributiveLattice.Homomorphism fe pt
open import Locales.Frame pt fe
open import Locales.GaloisConnection pt fe
open import MLTT.Spartan
open import UF.Base
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.Logic
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open AllCombinators pt fe renaming (_∧_ to _∧ₚ_)
\end{code}
We work in a module parameterized by a 𝓤-distributive-lattice `L₁` and a
𝓥-distributive-lattice `L₂`.
\begin{code}
module DistributiveLatticeIsomorphisms (L₁ : DistributiveLattice 𝓤)
(L₂ : DistributiveLattice 𝓥) where
\end{code}
The type `Isomorphismᵈᵣ L₁ L₂`, defined below, is the type of isomorphisms
between distributive lattices `L₁` and `L₂`.
\begin{code}
record Isomorphismᵈᵣ : (𝓤 ⊔ 𝓥) ⁺ ̇ where
field
𝓈 : L₁ ─d→ L₂
𝓇 : L₂ ─d→ L₁
s : ∣ L₁ ∣ᵈ → ∣ L₂ ∣ᵈ
s = Homomorphismᵈᵣ.h 𝓈
r : ∣ L₂ ∣ᵈ → ∣ L₁ ∣ᵈ
r = Homomorphismᵈᵣ.h 𝓇
s-is-homomorphism : is-homomorphismᵈ L₁ L₂ s holds
s-is-homomorphism = Homomorphismᵈᵣ.h-is-homomorphism 𝓈
r-is-homomorphism : is-homomorphismᵈ L₂ L₁ r holds
r-is-homomorphism = Homomorphismᵈᵣ.h-is-homomorphism 𝓇
field
r-cancels-s : r ∘ s ∼ id
s-cancels-r : s ∘ r ∼ id
\end{code}
Added on 2024-05-30.
Lemma for showing the equality two distributive lattice isomorphisms.
\begin{code}
open Isomorphismᵈᵣ
to-isomorphismᵈᵣ-＝ : (𝒾 𝒿 : Isomorphismᵈᵣ) → s 𝒾 ∼ s 𝒿 → r 𝒾 ∼ r 𝒿 → 𝒾 ＝ 𝒿
to-isomorphismᵈᵣ-＝ 𝒾 𝒿 φ ψ = † p q
where
open DistributiveLattice
p : 𝓈 𝒾 ＝ 𝓈 𝒿
p = to-homomorphismᵈ-＝ L₁ L₂ (𝓈 𝒾) (𝓈 𝒿) φ
q : 𝓇 𝒾 ＝ 𝓇 𝒿
q = to-homomorphismᵈ-＝ L₂ L₁ (𝓇 𝒾) (𝓇 𝒿) ψ
g : (r 𝒾 ∘ s 𝒾) ∼ id → (s 𝒾 ∘ r 𝒾) ∼ id → Isomorphismᵈᵣ
g e₁ e₂ = record { 𝓈 = 𝓈 𝒾 ; 𝓇 = 𝓇 𝒾 ; r-cancels-s = e₁ ; s-cancels-r = e₂}
f : 𝓈 𝒾 ＝ 𝓈 𝒿 → 𝓇 𝒾 ＝ 𝓇 𝒿 → Isomorphismᵈᵣ
f refl refl =
record
{ 𝓈 = 𝓈 𝒾
; 𝓇 = 𝓇 𝒾
; r-cancels-s = r-cancels-s 𝒾
; s-cancels-r = s-cancels-r 𝒾
}
† : 𝓈 𝒾 ＝ 𝓈 𝒿 → 𝓇 𝒾 ＝ 𝓇 𝒿 → 𝒾 ＝ 𝒿
† refl refl = ap₂ g β γ
where
β : r-cancels-s 𝒾 ＝ r-cancels-s 𝒿
β = Π-is-prop fe (λ _ → X-is-set L₁) (r-cancels-s 𝒾) (r-cancels-s 𝒿)
γ : s-cancels-r 𝒾 ＝ s-cancels-r 𝒿
γ = Π-is-prop fe (λ _ → X-is-set L₂) (s-cancels-r 𝒾) (s-cancels-r 𝒿)
\end{code}
End of addition.
Pretty syntax for `Isomorphismᵈᵣ`.
\begin{code}
Isomorphismᵈᵣ-Syntax : DistributiveLattice 𝓤
→ DistributiveLattice 𝓥
→ (𝓤 ⊔ 𝓥) ⁺ ̇
Isomorphismᵈᵣ-Syntax K L = DistributiveLatticeIsomorphisms.Isomorphismᵈᵣ K L
infix 0 Isomorphismᵈᵣ-Syntax
syntax Isomorphismᵈᵣ-Syntax K L = K ≅d≅ L
\end{code}
Added on 2024-05-17.
We now give an alternative definition of the notion of distributive lattice
homomorphism: an equivalence whose both sides are monotone.
\begin{code}
module HomomorphicEquivalences (K : DistributiveLattice 𝓤)
(L : DistributiveLattice 𝓤) where
is-homomorphic : (∣ K ∣ᵈ ≃ ∣ L ∣ᵈ) → Ω 𝓤
is-homomorphic e = is-monotonic (poset-ofᵈ K) (poset-ofᵈ L) ⌜ e ⌝
∧ₚ is-monotonic (poset-ofᵈ L) (poset-ofᵈ K) ⌜ e⁻¹ ⌝
where
e⁻¹ : ∣ L ∣ᵈ ≃ ∣ K ∣ᵈ
e⁻¹ = ≃-sym e
\end{code}
We denote by `Isomorphism₀` the type of isomorphisms given via this alternative
definition.
\begin{code}
Isomorphism₀ : 𝓤 ̇
Isomorphism₀ = Σ e ꞉ ∣ K ∣ᵈ ≃ ∣ L ∣ᵈ , is-homomorphic e holds
\end{code}
We now prove that this is equivalent to the categorical definition.
The part of the equivalence going from `Isomorphismᵈᵣ K L` to
`Isomorphism₀` is easy.
\begin{code}
open DistributiveLatticeIsomorphisms
open Some-Properties-Of-Posetal-Adjunctions
open Properties-Of-Posetal-Adjunctions-on-Distributive-Lattices
to-isomorphism₀ : Isomorphismᵈᵣ K L → Isomorphism₀
to-isomorphism₀ 𝒾 = e , 𝒽
where
open Isomorphismᵈᵣ 𝒾
using (s; 𝓈; 𝓇; r; s-cancels-r; r-cancels-s; s-is-homomorphism)
open Homomorphismᵈᵣ 𝓈
using ()
renaming (h-preserves-∧ to 𝓈-preserves-∧; h-is-monotone to 𝓈-is-monotone)
open Homomorphismᵈᵣ 𝓇
using ()
renaming (h-is-monotone to 𝓇-is-monotone)
open DistributiveLattice K
using ()
renaming (_∧_ to _∧₁_)
open DistributiveLattice L
using ()
renaming (_∧_ to _∧₂_)
e : ∣ K ∣ᵈ ≃ ∣ L ∣ᵈ
e = s , qinvs-are-equivs s (r , r-cancels-s , s-cancels-r)
𝒽 : is-homomorphic e holds
𝒽 = 𝓈-is-monotone , 𝓇-is-monotone
\end{code}
We now address the other direction.
Both parts of an equivalence are both a left adjoint and a right adjoint.
Therefore, they preserve finite meets and finite joins.
\begin{code}
open AdjointFunctorTheorem
open GaloisConnectionBetween (poset-ofᵈ L) (poset-ofᵈ K) renaming (_⊣_ to _⊣₁_)
open GaloisConnectionBetween (poset-ofᵈ K) (poset-ofᵈ L) renaming (_⊣_ to _⊣₂_)
to-isomorphismᵈᵣ : Isomorphism₀ → Isomorphismᵈᵣ K L
to-isomorphismᵈᵣ (e , (μ₁ , μ₂)) =
record
{ 𝓈 = 𝓈
; 𝓇 = 𝓇
; r-cancels-s = inverses-are-retractions' e
; s-cancels-r = inverses-are-sections' e
}
where
open DistributiveLattice L using () renaming (𝟏 to 𝟏L; 𝟎 to 𝟎L)
open DistributiveLattice K using () renaming (𝟏 to 𝟏K; 𝟎 to 𝟎K)
\end{code}
We have the monotone equivalence `e`, the forward and backward components of
which we denote by `s` and `r`:
\begin{code}
s = ⌜ e ⌝
r = ⌜ ≃-sym e ⌝
\end{code}
We denote by `sₘ` and `rₘ`, the versions of these packaged up with the proofs
that they are monotone.
\begin{code}
sₘ : poset-ofᵈ K ─m→ poset-ofᵈ L
sₘ = s , μ₁
rₘ : poset-ofᵈ L ─m→ poset-ofᵈ K
rₘ = r , μ₂
\end{code}
The map `s` is the left adjoint of `r` and vice versa.
\begin{code}
𝒶𝒹𝒿 : (rₘ ⊣₁ sₘ) holds
𝒶𝒹𝒿 = monotone-equivalences-are-adjoint
(poset-ofᵈ L)
(poset-ofᵈ K)
rₘ
sₘ
(inverses-are-retractions' e)
(inverses-are-sections' e)
𝒶𝒹𝒿' : (sₘ ⊣₂ rₘ) holds
𝒶𝒹𝒿' = monotone-equivalences-are-adjoint
(poset-ofᵈ K)
(poset-ofᵈ L)
sₘ
rₘ
(inverses-are-sections' e)
(inverses-are-retractions' e)
\end{code}
Because `r` is a right adjoint, it preserves `𝟏`.
\begin{code}
α₁ : preserves-𝟏 K L s holds
α₁ = right-adjoint-preserves-𝟏 L K rₘ sₘ 𝒶𝒹𝒿
\end{code}
Because `s` is a right adjoint, it preserves binary meets.
\begin{code}
β₁ : preserves-∧ K L s holds
β₁ = right-adjoint-preserves-∧ L K rₘ sₘ 𝒶𝒹𝒿
\end{code}
Because `s` is a left adjoint, it preserves the bottom element `𝟎`.
\begin{code}
γ₁ : preserves-𝟎 K L s holds
γ₁ = left-adjoint-preserves-𝟎 K L sₘ rₘ 𝒶𝒹𝒿'
\end{code}
Because `s` is a left adjoint, it preserves binary joins.
\begin{code}
δ₁ : preserves-∨ K L s holds
δ₁ = left-adjoint-preserves-∨ K L sₘ rₘ 𝒶𝒹𝒿'
\end{code}
Because `r` is a right adjoint, it preserves the top element `𝟏`.
\begin{code}
α₂ : preserves-𝟏 L K r holds
α₂ = right-adjoint-preserves-𝟏 K L sₘ rₘ 𝒶𝒹𝒿'
\end{code}
Because `r` is a right adjoint, it preserves binary meets.
\begin{code}
β₂ : preserves-∧ L K r holds
β₂ = right-adjoint-preserves-∧ K L sₘ rₘ 𝒶𝒹𝒿'
\end{code}
Because `r` is a left adjoint, it preserves the bottom element `𝟎`.
\begin{code}
γ₂ : preserves-𝟎 L K r holds
γ₂ = left-adjoint-preserves-𝟎 L K rₘ sₘ 𝒶𝒹𝒿
\end{code}
Because `r` is a left adjoint, it preserves binary joins.
\begin{code}
δ₂ : preserves-∨ L K r holds
δ₂ = left-adjoint-preserves-∨ L K rₘ sₘ 𝒶𝒹𝒿
\end{code}
Finally, we package everything up into the distributive lattice homomorphism
type.
\begin{code}
𝓈 : Homomorphismᵈᵣ K L
𝓈 = record
{ h = s
; h-is-homomorphism = α₁ , β₁ , γ₁ , δ₁}
𝓇 : Homomorphismᵈᵣ L K
𝓇 = record
{ h = r
; h-is-homomorphism = α₂ , β₂ , γ₂ , δ₂
}
\end{code}
The actual proof that these form an equivalence is trivial.
\begin{code}
isomorphismᵈᵣ-is-equivalent-to-isomorphism₀ : Isomorphism₀ ≃ Isomorphismᵈᵣ K L
isomorphismᵈᵣ-is-equivalent-to-isomorphism₀ =
to-isomorphismᵈᵣ , qinvs-are-equivs to-isomorphismᵈᵣ (to-isomorphism₀ , † , ‡)
where
† : to-isomorphism₀ ∘ to-isomorphismᵈᵣ ∼ id
† 𝒾@(e , μ₁ , μ₂) =
to-subtype-＝
(holds-is-prop ∘ is-homomorphic)
(to-subtype-＝ (being-equiv-is-prop (λ 𝓤 𝓥 → fe {𝓤} {𝓥})) refl)
‡ : to-isomorphismᵈᵣ ∘ to-isomorphism₀ ∼ id
‡ 𝒾 = to-isomorphismᵈᵣ-＝
K
L
(to-isomorphismᵈᵣ (to-isomorphism₀ 𝒾))
𝒾
(λ _ → refl)
(λ _ → refl)
\end{code}
Added on 2024-06-01.
We define the identity homomorphism on a distributive lattice.
The identity function preserves the bottom element.
\begin{code}
id-preserves-bottom : (L : DistributiveLattice 𝓤) → preserves-𝟎 L L id holds
id-preserves-bottom _ = refl
\end{code}
The identity function preserves the top element definitionally.
\begin{code}
id-preserves-top : (L : DistributiveLattice 𝓤) → preserves-𝟏 L L id holds
id-preserves-top _ = refl
\end{code}
The identity function preserves the meets definitionally.
\begin{code}
id-preserves-meets : (L : DistributiveLattice 𝓤) → preserves-∧ L L id holds
id-preserves-meets _ _ _ = refl
\end{code}
The identity function preserves the joins definitionally.
\begin{code}
id-preserves-joins : (L : DistributiveLattice 𝓤) → preserves-∨ L L id holds
id-preserves-joins _ _ _ = refl
\end{code}
We package up these into the proof that `id` is a homomorphism.
\begin{code}
id-is-homomorphism : (L : DistributiveLattice 𝓤) → is-homomorphismᵈ L L id holds
id-is-homomorphism L = id-preserves-top L
, id-preserves-meets L
, id-preserves-bottom L
, id-preserves-joins L
\end{code}
We package up the identity function together with the proof that it is a
homomorphism and denote it `𝔦𝔡`.
\begin{code}
𝔦𝔡 : (L : DistributiveLattice 𝓤) → L ─d→ L
𝔦𝔡 L = record { h = id ; h-is-homomorphism = id-is-homomorphism L}
\end{code}