---
layout: default
title : "Legacy.Base.Homomorphisms.Basic module (The Agda Universal Algebra Library)"
date : "2021-01-13"
author: "agda-algebras development team"
---

### <a id="basic-definitions">Basic Definitions</a>

This is the [Legacy.Base.Homomorphisms.Basic] module of the [Agda Universal Algebra Library][].


```agda


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

open import Overture using ( Signature; π“ž ; π“₯ )

module Legacy.Base.Homomorphisms.Basic {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Agda.Primitive  renaming ( Set to Type )   using ()
open import Data.Product    renaming ( proj₁ to fst )
                            using ( _,_ ; Ξ£ ;  _Γ—_ ; Ξ£-syntax)
open import Function        using ( _∘_ ; id )
open import Level           using ( Level ; _βŠ”_ )

open import Relation.Binary.PropositionalEquality using ( _≑_ ; refl )

-- Imports from the Agda Universal Algebras Library --------------------------------
open import Overture               using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Legacy.Base.Functions         using ( IsInjective ; IsSurjective )
open import Legacy.Base.Algebras {𝑆 = 𝑆}  using ( Algebra ; _Μ‚_ ; Lift-Alg )

private variable Ξ± Ξ² : Level
```


#### <a id="homomorphisms">Homomorphisms</a>

If `𝑨` and `𝑩` are `𝑆`-algebras, then a *homomorphism* from `𝑨` to `𝑩` is a
function `h : ∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣` from the domain of `𝑨` to the domain of `𝑩` that is
*compatible* (or *commutes*) with all of the basic operations of the signature;
that is, for all operation symbols `𝑓 : ∣ 𝑆 ∣` and tuples `a : βˆ₯ 𝑆 βˆ₯ 𝑓 β†’ ∣ 𝑨 ∣` of
`𝑨`, the following holds:

`h ((𝑓 Μ‚ 𝑨) a) ≑ (𝑓 Μ‚ 𝑩) (h ∘ a)`.

**Remarks**. Recall, `h ∘ 𝒂` is the tuple whose i-th component is `h (𝒂 i)`.
Instead of "homomorphism," we sometimes use the nickname "hom" to refer to such
a map.

To formalize this concept, we first define a type representing the assertion that
a function `h : ∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣` commutes with a single basic operation `𝑓`.  With
Agda's extremely flexible syntax the defining equation above can be expressed
unadulterated.


```agda


module _ (𝑨 : Algebra Ξ±)(𝑩 : Algebra Ξ²) where

 compatible-op-map : ∣ 𝑆 ∣ β†’ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) β†’ Type(Ξ± βŠ” π“₯ βŠ” Ξ²)
 compatible-op-map 𝑓 h = βˆ€ π‘Ž β†’ h ((𝑓 Μ‚ 𝑨) π‘Ž) ≑ (𝑓 Μ‚ 𝑩) (h ∘ π‘Ž)
```


Agda infers from the shorthand `βˆ€ π‘Ž` that `π‘Ž` has type `βˆ₯ 𝑆 βˆ₯ 𝑓 β†’ ∣ 𝑨 ∣` since it
must be a tuple on `∣ 𝑨 ∣` of "length" `βˆ₯ 𝑆 βˆ₯ 𝑓` (the arity of `𝑓`).

We now define the type `hom 𝑨 𝑩` of homomorphisms from `𝑨` to `𝑩` by first
defining the type `is-homomorphism` which represents the property of being a
homomorphism.


```agda


 is-homomorphism : (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) β†’ Type(π“ž βŠ” π“₯ βŠ” Ξ± βŠ” Ξ²)
 is-homomorphism g = βˆ€ 𝑓  β†’  compatible-op-map 𝑓 g

 hom : Type(π“ž βŠ” π“₯ βŠ” Ξ± βŠ” Ξ²)
 hom = Ξ£ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) is-homomorphism
```



#### <a id="important-exmples-of-homomorphisms">Important examples of homomorphisms</a>

Let's look at a few important examples of homomorphisms. These examples are
actually quite special in that every algebra has such a homomorphism.

We begin with the identity map, which is proved to be (the underlying map of) a
homomorphism as follows.


```agda


𝒾𝒹 : (𝑨 : Algebra Ξ±) β†’ hom 𝑨 𝑨
𝒾𝒹 _ = id , Ξ» 𝑓 π‘Ž β†’ refl
```


Next, the lifting of an algebra to a higher universe level is, in fact, a
homomorphism. Dually, the lowering of a lifted algebra to its original universe
level is a homomorphism.


```agda


open Level

𝓁𝒾𝒻𝓉 : {Ξ² : Level}(𝑨 : Algebra Ξ±) β†’ hom 𝑨 (Lift-Alg 𝑨 Ξ²)
𝓁𝒾𝒻𝓉 _ = lift , Ξ» 𝑓 π‘Ž β†’ refl

π“β„΄π“Œβ„―π“‡ : {Ξ² : Level}(𝑨 : Algebra Ξ±) β†’ hom (Lift-Alg 𝑨 Ξ²) 𝑨
π“β„΄π“Œβ„―π“‡ _ = lower , Ξ» 𝑓 π‘Ž β†’ refl
```



#### <a id="monomorphisms-and-epimorphisms">Monomorphisms and epimorphisms</a>

A *monomorphism* is an injective homomorphism and an *epimorphism* is a surjective
homomorphism. These are represented in the [agda-algebras][] library by the following
types.


```agda


is-monomorphism : (𝑨 : Algebra Ξ±)(𝑩 : Algebra Ξ²) β†’ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) β†’ Type _
is-monomorphism 𝑨 𝑩 g = is-homomorphism 𝑨 𝑩 g Γ— IsInjective g

mon : Algebra Ξ± β†’ Algebra Ξ² β†’ Type(π“ž βŠ” π“₯ βŠ” Ξ± βŠ” Ξ²)
mon 𝑨 𝑩 = Ξ£[ g ∈ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) ] is-monomorphism 𝑨 𝑩 g

is-epimorphism : (𝑨 : Algebra Ξ±)(𝑩 : Algebra Ξ²) β†’ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) β†’ Type _
is-epimorphism 𝑨 𝑩 g = is-homomorphism 𝑨 𝑩 g Γ— IsSurjective g

epi : Algebra Ξ± β†’ Algebra Ξ² β†’ Type(π“ž βŠ” π“₯ βŠ” Ξ± βŠ” Ξ²)
epi 𝑨 𝑩 = Ξ£[ g ∈ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) ] is-epimorphism 𝑨 𝑩 g
```


It will be convenient to have a function that takes an inhabitant of `mon` (or
`epi`) and extracts the homomorphism part, or *hom reduct* (that is, the pair
consisting of the map and a proof that the map is a homomorphism).


```agda


monβ†’hom : (𝑨 : Algebra Ξ±){𝑩 : Algebra Ξ²} β†’ mon 𝑨 𝑩 β†’ hom 𝑨 𝑩
monβ†’hom 𝑨 Ο• = ∣ Ο• ∣ , fst βˆ₯ Ο• βˆ₯

epiβ†’hom : {𝑨 : Algebra Ξ±}(𝑩 : Algebra Ξ²) β†’ epi 𝑨 𝑩 β†’ hom 𝑨 𝑩
epiβ†’hom _ Ο• = ∣ Ο• ∣ , fst βˆ₯ Ο• βˆ₯
```