Skip to content

Legacy.Base.Structures.Sigma.Isos

Isomorphisms of general structures


{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Legacy.Base.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        using ( ∣_∣ ; _β‰ˆ_ ; βˆ₯_βˆ₯ ; _βˆ™_ ; lower∼lift ; lift∼lower )
open import Legacy.Base.Structures.Sigma.Basic     using ( Signature ; Structure ; Lift-Struc )
open import Legacy.Base.Structures.Sigma.Homs      using ( hom ; 𝒾𝒹 ; ∘-hom ; 𝓁𝒾𝒻𝓉 ; π“β„΄π“Œβ„―π“‡ ; is-hom)
open import Legacy.Base.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 Agda's universe hierarchy.


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)