 Isomorphisms of general structures

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

module Structures.Sigma.Isos where

-- Imports from the Agda Standard Library ------------------------------------------------------
open import Axiom.Extensionality.Propositional
using () renaming (Extensionality to funext)
open import Agda.Primitive using ( _⊔_ ; lsuc ) renaming ( Set to Type )
open import Data.Product   using ( _,_ ; Σ-syntax ; _×_ ) renaming ( proj₁ to fst ; proj₂ to snd )
open import Function.Base  using ( _∘_ )
open import Level          using ( Level ; Lift ; lift ; lower )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; cong ; cong-app )

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture.Preliminaries    using ( ∣_∣ ; _≈_ ; ∥_∥ ; _∙_ ; lower∼lift ; lift∼lower )
open import Structures.Sigma.Basic    using ( Signature ; Structure ; Lift-Struc )
open import Structures.Sigma.Homs     using ( hom ; 𝒾𝒹 ; ∘-hom ; 𝓁𝒾𝒻𝓉 ; 𝓁ℴ𝓌ℯ𝓇 ; is-hom)
open import Structures.Sigma.Products using    (   ; ℓp ;  ; 𝔖 ; class-prod )
private variable 𝑅 𝐹 : Signature

Recall, f ≈ g means f and g are extensionally (or pointwise) equal; i.e., ∀ x, f x ≡ g x. We use this notion of equality of functions in the following definition of isomorphism.

module _ {α ρᵃ β ρᵇ : Level} where

record _≅_ (𝑨 : Structure  𝑅 𝐹 {α}{ρᵃ})(𝑩 : Structure 𝑅 𝐹 {β}{ρᵇ}) : Type (α  ρᵃ  β  ρᵇ) where
field
to : hom 𝑨 𝑩
from : hom 𝑩 𝑨
to∼from :  to    from    𝒾𝒹 𝑩
from∼to :  from    to    𝒾𝒹 𝑨

open _≅_ public

That is, two structures are isomorphic provided there are homomorphisms going back and forth between them which compose to the identity map.

Properties of isomorphism of structures of sigma type

module _ {α ρᵃ : Level} where

≅-refl : {𝑨 : Structure 𝑅 𝐹 {α}{ρᵃ}}  𝑨  𝑨
≅-refl {𝑨 = 𝑨} =
record { to = 𝒾𝒹 𝑨 ; from = 𝒾𝒹 𝑨 ; to∼from = λ _  refl ; from∼to = λ _  refl }

module _ {α ρᵃ β ρᵇ : Level} where

≅-sym : {𝑨 : Structure 𝑅 𝐹 {α}{ρᵃ}}{𝑩 : Structure 𝑅 𝐹 {β}{ρᵇ}}
𝑨  𝑩  𝑩  𝑨
≅-sym A≅B = record { to = from A≅B ; from = to A≅B ; to∼from = from∼to A≅B ; from∼to = to∼from A≅B }

module _ {α ρᵃ β ρᵇ γ ρᶜ : Level}
(𝑨 : Structure 𝑅 𝐹 {α}{ρᵃ}){𝑩 : Structure 𝑅 𝐹 {β}{ρᵇ}}
(𝑪 : Structure 𝑅 𝐹 {γ}{ρᶜ}) where

≅-trans : 𝑨  𝑩  𝑩  𝑪  𝑨  𝑪

≅-trans ab bc = record { to = f ; from = g ; to∼from = τ ; from∼to = ν }
where
f1 : hom 𝑨 𝑩
f1 = to ab
f2 : hom 𝑩 𝑪
f2 = to bc
f : hom 𝑨 𝑪
f = ∘-hom 𝑨 𝑪 f1 f2

g1 : hom 𝑪 𝑩
g1 = from bc
g2 : hom 𝑩 𝑨
g2 = from ab
g : hom 𝑪 𝑨
g = ∘-hom 𝑪 𝑨 g1 g2

τ :  f    g    𝒾𝒹 𝑪
τ x = (cong  f2 (to∼from ab ( g1  x)))(to∼from bc) x

ν :  g    f    𝒾𝒹 𝑨
ν x = (cong  g2 (from∼to bc ( f1  x)))(from∼to ab) x

Fortunately, the lift operation preserves isomorphism (i.e., it’s an algebraic invariant). As our focus is universal algebra, this is important and is what makes the lift operation a workable solution to the technical problems that arise from the noncumulativity of the universe hierarchy discussed in [Overture.Lifts][].

open Level

module _ {α ρᵃ : Level} where

Lift-≅ : ( ρ : Level)  {𝑨 : Structure 𝑅 𝐹 {α}{ρᵃ}}  𝑨  (Lift-Struc  ρ 𝑨)
Lift-≅  ρ {𝑨} = record { to = 𝓁𝒾𝒻𝓉  ρ 𝑨
; from = 𝓁ℴ𝓌ℯ𝓇  ρ 𝑨
; to∼from = cong-app lift∼lower
; from∼to = cong-app (lower∼lift{α}{ρ})
}

module _ {α ρᵃ β ρᵇ : Level}
{𝑨 : Structure 𝑅 𝐹 {α}{ρᵃ}}{𝑩 : Structure 𝑅 𝐹 {β}{ρᵇ}} where

Lift-Struc-iso : ( ρ ℓ' ρ' : Level)  𝑨  𝑩  Lift-Struc  ρ 𝑨  Lift-Struc ℓ' ρ' 𝑩

Lift-Struc-iso  ρ ℓ' ρ' A≅B = ≅-trans (Lift-Struc  ρ 𝑨) (Lift-Struc ℓ' ρ' 𝑩)
( ≅-trans (Lift-Struc  ρ 𝑨) 𝑩 (≅-sym (Lift-≅  ρ)) A≅B )
(Lift-≅ ℓ' ρ')

Products of isomorphic families of algebras are themselves isomorphic. The proof looks a bit technical, but it is as straightforward as it ought to be.

module _ {ι : Level}{I : Type ι}
{α ρᵃ β ρᵇ : Level} {fe : funext ρᵇ ρᵇ}
{fiu : funext ι α}{fiw : funext ι β} where

⨅≅ : {𝒜 : I  Structure 𝑅 𝐹 {α}{ρᵃ}}{ : I  Structure 𝑅 𝐹 {β}{ρᵇ}}  (∀ (i : I)  𝒜 i   i)   𝒜

⨅≅ {𝒜 = 𝒜}{} AB = record { to = ϕ , ϕhom ; from = ψ , ψhom ; to∼from = ϕ~ψ ; from∼to = ψ~ϕ }
where
ϕ :   𝒜
ϕ a i =  to (AB i)  (a i)

ϕhom : is-hom ( 𝒜) ( ) ϕ
ϕhom =  r a x 𝔦  fst  to (AB 𝔦)  r  z  a z 𝔦) (x 𝔦)) ,
λ f a  fiw  i  snd  to (AB i)  f  z  a z i))

ψ :        𝒜
ψ b i =  from (AB i)  (b i)

ψhom : is-hom ( ) ( 𝒜) ψ
ψhom =  r a x 𝔦  fst  from (AB 𝔦)  r  z  a z 𝔦) (x 𝔦)) ,
f a  fiu  i  snd  from (AB i)  f  z  a z i)))

ϕ~ψ : ϕ  ψ   𝒾𝒹 ( )
ϕ~ψ 𝒃 = fiw λ i  (to∼from (AB i)) (𝒃 i)

ψ~ϕ : ψ  ϕ   𝒾𝒹 ( 𝒜)
ψ~ϕ a = fiu λ i  (from∼to (AB i)) (a i)