Agda UALib β

### Isomorphisms

This section describes the Homomorphisms.Isomorphisms module of the Agda Universal Algebra Library. Here we formalize the informal notion of isomorphism between algebraic structures.

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

open import Algebras.Signatures using (Signature; π; π₯)

module Homomorphisms.Isomorphisms {π : Signature π π₯} where

open import Homomorphisms.Noether{π = π} public
open import MGS-Embeddings using (Nat; NatΞ ; NatΞ -is-embedding) public

```

#### Definition of isomorphism

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.

```
_β_ : {π€ π¦ : Universe}(π¨ : Algebra π€ π)(π© : Algebra π¦ π) β π β π₯ β π€ β π¦ Μ
π¨ β π© =  Ξ£ f κ (hom π¨ π©) , Ξ£ g κ (hom π© π¨) , (β£ f β£ β β£ g β£ βΌ β£ πΎπΉ π© β£)
Γ (β£ g β£ β β£ f β£ βΌ β£ πΎπΉ π¨ β£)

```

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

#### Isomorphism is an equivalence relation

```
β-refl : {π€ : Universe} {π¨ : Algebra π€ π} β π¨ β π¨
β-refl {π€}{π¨} = πΎπΉ π¨ , πΎπΉ π¨ , (Ξ» a β refl) , (Ξ» a β refl)

β-sym : {π€ π¦ : Universe}{π¨ : Algebra π€ π}{π© : Algebra π¦ π}
β-sym h = fst β₯ h β₯ , fst h , β₯ snd β₯ h β₯ β₯ , β£ snd β₯ h β₯ β£

module _ {π§ π¨ π© : Universe} where

β-trans : {π¨ : Algebra π§ π}{π© : Algebra π¨ π}{πͺ : Algebra π© π}
β        π¨ β π© β π© β πͺ β π¨ β πͺ

β-trans {π¨} {π©}{πͺ} ab bc = f , g , Ξ± , Ξ²
where
f1 = β£ ab β£
f2 = β£ bc β£
f : hom π¨ πͺ
f = β-hom π¨ πͺ f1 f2

g1 = fst β₯ bc β₯
g2 = fst β₯ ab β₯
g : hom πͺ π¨
g = β-hom πͺ π¨ g1 g2

Ξ± : β£ f β£ β β£ g β£ βΌ β£ πΎπΉ πͺ β£
Ξ± x = (ap β£ f2 β£(β£ snd β₯ ab β₯ β£ (β£ g1 β£ x)))β(β£ snd β₯ bc β₯ β£) x

Ξ² : β£ g β£ β β£ f β£ βΌ β£ πΎπΉ π¨ β£
Ξ² x = (ap β£ g2 β£(β₯ snd β₯ bc β₯ β₯ (β£ f1 β£ x)))β(β₯ snd β₯ ab β₯ β₯) x

```

#### Lift is an algebraic invariant

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 Lift

module _ {π€ π¦ : Universe} where

Lift-β : {π¨ : Algebra π€ π} β π¨ β (Lift-alg π¨ π¦)
Lift-β {π¨} = ππΎπ»π , (πβ΄πβ―π{π€}{π¦}{π¨}) , happly liftβΌlower , happly (lowerβΌlift{π¦})

Lift-hom : (π§ : Universe)(π¨ : Universe){π¨ : Algebra π€ π}(π© : Algebra π¦ π)
β             hom π¨ π©  β  hom (Lift-alg π¨ π§) (Lift-alg π© π¨)

Lift-hom π§ π¨ {π¨} π© (f , fhom) = lift β f β lower , Ξ³
where
lABh : is-homomorphism (Lift-alg π¨ π§) π© (f β lower)
lABh = β-is-hom (Lift-alg π¨ π§) π© {lower}{f} (Ξ» _ _ β refl) fhom

Ξ³ : is-homomorphism(Lift-alg π¨ π§)(Lift-alg π© π¨) (lift β (f β lower))
Ξ³ = β-is-hom (Lift-alg π¨ π§) (Lift-alg π© π¨){f β lower}{lift} lABh Ξ» _ _ β refl

module _ {π€ π¦ : Universe} where

Lift-alg-iso : {π¨ : Algebra π€ π}{π§ : Universe}
{π© : Algebra π¦ π}{π¨ : Universe}
-----------------------------------------
β             π¨ β π© β (Lift-alg π¨ π§) β (Lift-alg π© π¨)

Lift-alg-iso AβB = β-trans (β-trans (β-sym Lift-β) AβB) Lift-β

```

#### Lift associativity

The lift is also associative, up to isomorphism at least.

```
module _ {π π€ π¦ : Universe} where

Lift-alg-assoc : {π¨ : Algebra π€ π} β Lift-alg π¨ (π¦ β π) β (Lift-alg (Lift-alg π¨ π¦) π)
Lift-alg-assoc {π¨} = β-trans (β-trans Ξ³ Lift-β) Lift-β
where
Ξ³ : Lift-alg π¨ (π¦ β π) β π¨
Ξ³ = β-sym Lift-β

Lift-alg-associative : (π¨ : Algebra π€ π) β Lift-alg π¨ (π¦ β π) β (Lift-alg (Lift-alg π¨ π¦) π)
Lift-alg-associative π¨ = Lift-alg-assoc {π¨}

```

#### Products preserve isomorphisms

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 _ {π π€ π¦ : Universe}{I : π Μ}{feππ€ : dfunext π π€}{feππ¦ : dfunext π π¦} where

β¨β : {π : I β Algebra π€ π}{β¬ : I β Algebra π¦ π} β Ξ  i κ I , π i β β¬ i β β¨ π β β¨ β¬

β¨β {π}{β¬} AB = Ξ³
where
Ο : β£ β¨ π β£ β β£ β¨ β¬ β£
Ο a i = β£ fst (AB i) β£ (a i)

Οhom : is-homomorphism (β¨ π) (β¨ β¬) Ο
Οhom π a = feππ¦ (Ξ» i β β₯ fst (AB i) β₯ π (Ξ» x β a x i))

Ο : β£ β¨ β¬ β£ β β£ β¨ π β£
Ο b i = β£ fst β₯ AB i β₯ β£ (b i)

Οhom : is-homomorphism (β¨ β¬) (β¨ π) Ο
Οhom π π = feππ€ (Ξ» i β snd β£ snd (AB i) β£ π (Ξ» x β π x i))

Ο~Ο : Ο β Ο βΌ β£ πΎπΉ (β¨ β¬) β£
Ο~Ο π = feππ¦ Ξ» i β fst β₯ snd (AB i) β₯ (π i)

Ο~Ο : Ο β Ο βΌ β£ πΎπΉ (β¨ π) β£
Ο~Ο a = feππ€ Ξ» i β snd β₯ snd (AB i) β₯ (a i)

Ξ³ : β¨ π β β¨ β¬
Ξ³ = (Ο , Οhom) , ((Ο , Οhom) , Ο~Ο , Ο~Ο)

```

A nearly identical proof goes through for isomorphisms of lifted products (though, just for fun, we use the universal quantifier syntax here to express the dependent function type in the statement of the lemma, instead of the Pi notation we used in the statement of the previous lemma; that is, `β i β π i β β¬ (lift i)` instead of `Ξ  i κ I , π i β β¬ (lift i)`.)

```
module _ {π π© : Universe}{I : π Μ}{fizw : dfunext (π β π©) π¦}{fiu : dfunext π π€} where

Lift-alg-β¨β : {π : I β Algebra π€ π}{β¬ : (Lift{π©} I) β Algebra π¦ π}
β            (β i β π i β β¬ (lift i)) β Lift-alg (β¨ π) π© β β¨ β¬

Lift-alg-β¨β {π}{β¬} AB = Ξ³
where
Ο : β£ β¨ π β£ β β£ β¨ β¬ β£
Ο a i = β£ fst (AB  (lower i)) β£ (a (lower i))

Οhom : is-homomorphism (β¨ π) (β¨ β¬) Ο
Οhom π a = fizw (Ξ» i β (β₯ fst (AB (lower i)) β₯) π (Ξ» x β a x (lower i)))

Ο : β£ β¨ β¬ β£ β β£ β¨ π β£
Ο b i = β£ fst β₯ AB i β₯ β£ (b (lift i))

Οhom : is-homomorphism (β¨ β¬) (β¨ π) Ο
Οhom π π = fiu (Ξ» i β (snd β£ snd (AB i) β£) π (Ξ» x β π x (lift i)))

Ο~Ο : Ο β Ο βΌ β£ πΎπΉ (β¨ β¬) β£
Ο~Ο π = fizw Ξ» i β fst β₯ snd (AB (lower i)) β₯ (π i)

Ο~Ο : Ο β Ο βΌ β£ πΎπΉ (β¨ π) β£
Ο~Ο a = fiu Ξ» i β snd β₯ snd (AB i) β₯ (a i)

AβB : β¨ π β β¨ β¬
AβB = (Ο , Οhom) , ((Ο , Οhom) , Ο~Ο , Ο~Ο)

Ξ³ : Lift-alg (β¨ π) π© β β¨ β¬
Ξ³ = β-trans (β-sym Lift-β) AβB

```

#### Embedding tools

Finally, we prove some useful facts about embeddings that occasionally come in handy.

```
module _ {π π€ π¦ : Universe} where

embedding-lift-nat : hfunext π π€ β hfunext π π¦
β                   {I : π Μ}{A : I β π€ Μ}{B : I β π¦ Μ}
(h : Nat A B) β (β i β is-embedding (h i))
------------------------------------------
β                   is-embedding(NatΞ  h)

embedding-lift-nat hfiu hfiw h hem = NatΞ -is-embedding hfiu hfiw h hem

embedding-lift-nat' : hfunext π π€ β hfunext π π¦
β                    {I : π Μ}{π : I β Algebra π€ π}{β¬ : I β Algebra π¦ π}
(h : Nat(fst β π)(fst β β¬)) β (β i β is-embedding (h i))
--------------------------------------------------------
β                    is-embedding(NatΞ  h)

embedding-lift-nat' hfiu hfiw h hem = NatΞ -is-embedding hfiu hfiw h hem

embedding-lift : hfunext π π€ β hfunext π π¦
β               {I : π Μ} β {π : I β Algebra π€ π}{β¬ : I β Algebra π¦ π}
β               (h : β i β β£ π i β£ β β£ β¬ i β£) β (β i β is-embedding (h i))
----------------------------------------------------------
β               is-embedding(Ξ» (x : β£ β¨ π β£) (i : I) β (h i)(x i))

embedding-lift hfiu hfiw {I}{π}{β¬} h hem = embedding-lift-nat' hfiu hfiw {I}{π}{β¬} h hem

isoβembedding : {π€ π¦ : Universe}{π¨ : Algebra π€ π}{π© : Algebra π¦ π}
β              (Ο : π¨ β π©) β is-embedding (fst β£ Ο β£)

isoβembedding Ο = equivs-are-embeddings (fst β£ Ο β£)
(invertibles-are-equivs (fst β£ Ο β£) finv)
where
finv : invertible (fst β£ Ο β£)
finv = β£ fst β₯ Ο β₯ β£ , (snd β₯ snd Ο β₯ , fst β₯ snd Ο β₯)

```