Properties of Homomorphisms

This is the Base.Homomorphisms.Properties module of the Agda Universal Algebra Library.

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

open import Overture using (Signature ; π ; π₯ )

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

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Data.Product  using ( _,_ )
open import Function      using ( _β_ )
open import Level         using ( Level )

open  import Relation.Binary.PropositionalEquality as β‘
using ( _β‘_ ; module β‘-Reasoning )

-- Imports from the Agda Universal Algebras Library --------------------------------
open import Overture                           using ( β£_β£ ; β₯_β₯ )
open import Base.Algebras             {π = π}  using ( Algebra ; _Μ_ ; Lift-Alg )
open import Base.Homomorphisms.Basic  {π = π}  using ( hom ; is-homomorphism )

private variable Ξ± Ξ² Ξ³ Ο : Level
```

Homomorphism composition

The composition of homomorphisms is again a homomorphism. We formalize this in a number of alternative ways.

```open β‘-Reasoning

module _ (π¨ : Algebra Ξ± π){π© : Algebra Ξ² π}(πͺ : Algebra Ξ³ π) where

β-hom : hom π¨ π©  β  hom π© πͺ  β  hom π¨ πͺ
β-hom (g , ghom) (h , hhom) = h β g , Goal where

Goal : β π a β (h β g)((π Μ π¨) a) β‘ (π Μ πͺ)(h β g β a)
Goal π a =  (h β g)((π Μ π¨) a)  β‘β¨ β‘.cong h ( ghom π a )  β©
h ((π Μ π©)(g β a))  β‘β¨ hhom π ( g β a )       β©
(π Μ πͺ)(h β g β a)  β

β-is-hom :  {f : β£ π¨ β£ β β£ π© β£}{g : β£ π© β£ β β£ πͺ β£}
β          is-homomorphism π¨ πͺ (g β f)

β-is-hom {f} {g} fhom ghom = β₯ β-hom (f , fhom) (g , ghom) β₯

```

A homomorphism from `π¨` to `π©` can be lifted to a homomorphism from `Lift-Alg π¨ βα΅` to `Lift-Alg π© βα΅`.

```open Level

Lift-hom :  {π¨ : Algebra Ξ± π}(βα΅ : Level){π© : Algebra Ξ² π} (βα΅ : Level)
β          hom π¨ π©  β  hom (Lift-Alg π¨ βα΅) (Lift-Alg π© βα΅)

Lift-hom {π¨ = π¨} βα΅ {π©} βα΅ (f , fhom) = lift β f β lower , Goal
where
lABh : is-homomorphism (Lift-Alg π¨ βα΅) π© (f β lower)
lABh = β-is-hom (Lift-Alg π¨ βα΅) π© {lower}{f} (Ξ» _ _ β β‘.refl) fhom

Goal : is-homomorphism(Lift-Alg π¨ βα΅)(Lift-Alg π© βα΅) (lift β (f β lower))
Goal = β-is-hom  (Lift-Alg π¨ βα΅) (Lift-Alg π© βα΅)
{f β lower}{lift} lABh Ξ» _ _ β β‘.refl

```

We should probably point out that while the lifting and lowering homomorphisms are important for our formal treatment of algebras in type theory, they never ariseβin fact, they are not even definableβin classical universal algebra based on set theory.