Agda UALib ↑

Basic Definitions

This section describes the Homomorphisms.Basic module of the Agda Universal Algebra Library.


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

open import Algebras.Signatures using (Signature; π“ž; π“₯)

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

open import Algebras.Congruences{𝑆 = 𝑆} public
open import MGS-MLTT using (_β‰‘βŸ¨_⟩_; _∎; id) public

Homomorphisms

If 𝑨 and 𝑩 are 𝑆-algebras, then a homomorphism from 𝑨 to 𝑩 is a function β„Ž : ∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣ 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 π‘Ž : βˆ₯ 𝑆 βˆ₯ 𝑓 β†’ ∣ 𝑨 ∣ of 𝑨, the following holds:1

h ((𝑓 Μ‚ 𝑨) π‘Ž) ≑ (𝑓 Μ‚ 𝑩) (h ∘ π‘Ž).

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.


module _ {𝓀 𝓦 : Universe}(𝑨 : Algebra 𝓀 𝑆)(𝑩 : Algebra 𝓦 𝑆) where

 compatible-op-map : ∣ 𝑆 ∣ β†’ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
 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.


 is-homomorphism : (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) β†’ π“ž βŠ” π“₯ βŠ” 𝓀 βŠ” 𝓦 Μ‡
 is-homomorphism g = βˆ€ 𝑓  β†’  compatible-op-map 𝑓 g

 hom : π“ž βŠ” π“₯ βŠ” 𝓀 βŠ” 𝓦 Μ‡
 hom = Ξ£ g κž‰ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣ ) , is-homomorphism g

Examples of homomorphisms

Let’s look at a few examples of homomorphisms. These examples are actually quite special in that the function in question commutes with the basic operations of all algebras and so, no matter the algebras involved, is always a homomorphism (trivially). We begin with the identity map, which is proved to be (the underlying map of) a homomorphism as follows.


module _ {𝓀 : Universe} where

 𝒾𝒹 : (A : Algebra 𝓀 𝑆) β†’ hom A A
 𝒾𝒹 _ = id , Ξ» 𝑓 π‘Ž β†’ refl

Next, lift and lower, defined in the Overture.Lifts module, are (the maps of) homomorphisms. Again, the proofs are trivial.


 open Lift

 𝓁𝒾𝒻𝓉 : {𝓦 : Universe}{𝑨 : Algebra 𝓀 𝑆} β†’ hom 𝑨 (Lift-alg 𝑨 𝓦)
 𝓁𝒾𝒻𝓉 = lift , Ξ» 𝑓 π‘Ž β†’ refl

 π“β„΄π“Œβ„―π“‡ : {𝓦 : Universe}{𝑨 : Algebra 𝓀 𝑆} β†’ hom (Lift-alg 𝑨 𝓦) 𝑨
 π“β„΄π“Œβ„―π“‡ = lower , Ξ» 𝑓 π‘Ž β†’ refl

Monomorphisms and epimorphisms

A monomorphism is an injective homomorphism and an epimorphism is a surjective homomorphism. These are represented in the UALib by the following types.


module _ {𝓀 𝓦 : Universe} where

 is-monomorphism : (𝑨 : Algebra 𝓀 𝑆)(𝑩 : Algebra 𝓦 𝑆) β†’ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) β†’ π“ž βŠ” π“₯ βŠ” 𝓀 βŠ” 𝓦 Μ‡
 is-monomorphism 𝑨 𝑩 g = is-homomorphism 𝑨 𝑩 g Γ— Monic g

 mon : Algebra 𝓀 𝑆 β†’ Algebra 𝓦 𝑆  β†’ π“ž βŠ” π“₯ βŠ” 𝓀 βŠ” 𝓦 Μ‡
 mon 𝑨 𝑩 = Ξ£ g κž‰ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) , is-monomorphism 𝑨 𝑩 g

 is-epimorphism : (𝑨 : Algebra 𝓀 𝑆)(𝑩 : Algebra 𝓦 𝑆) β†’ (∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣) β†’ π“ž βŠ” π“₯ βŠ” 𝓀 βŠ” 𝓦 Μ‡
 is-epimorphism 𝑨 𝑩 g = is-homomorphism 𝑨 𝑩 g Γ— Epic g

 epi : Algebra 𝓀 𝑆 β†’ Algebra 𝓦 𝑆  β†’ π“ž βŠ” π“₯ βŠ” 𝓀 βŠ” 𝓦 Μ‡
 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).


 mon-to-hom : (𝑨 : Algebra 𝓀 𝑆){𝑩 : Algebra 𝓦 𝑆} β†’ mon 𝑨 𝑩 β†’ hom 𝑨 𝑩
 mon-to-hom 𝑨 Ο• = ∣ Ο• ∣ , fst βˆ₯ Ο• βˆ₯

 epi-to-hom : {𝑨 : Algebra 𝓀 𝑆}(𝑩 : Algebra 𝓦 𝑆) β†’ epi 𝑨 𝑩 β†’ hom 𝑨 𝑩
 epi-to-hom _ Ο• = ∣ Ο• ∣ , fst βˆ₯ Ο• βˆ₯

Kernels of homomorphisms

The kernel of a homomorphism is a congruence relation and conversely for every congruence relation ΞΈ, there exists a homomorphism with kernel ΞΈ (namely, that canonical projection onto the quotient modulo ΞΈ).


module _ {𝓀 𝓦 : Universe}{𝑨 : Algebra 𝓀 𝑆} where

 homker-compatible : dfunext π“₯ 𝓦 β†’ (𝑩 : Algebra 𝓦 𝑆)(h : hom 𝑨 𝑩) β†’ compatible 𝑨 (ker ∣ h ∣)
 homker-compatible fe 𝑩 h f {u}{v} Kerhab = ∣ h ∣ ((f Μ‚ 𝑨) u)   β‰‘βŸ¨ βˆ₯ h βˆ₯ f u ⟩
                                            (f Μ‚ 𝑩)(∣ h ∣ ∘ u)  β‰‘βŸ¨ ap (f Μ‚ 𝑩)(fe Ξ» x β†’ Kerhab x) ⟩
                                            (f Μ‚ 𝑩)(∣ h ∣ ∘ v)  β‰‘βŸ¨ (βˆ₯ h βˆ₯ f v)⁻¹ ⟩
                                            ∣ h ∣ ((f Μ‚ 𝑨) v)   ∎

It is convenient to define a function that takes a homomorphism and constructs a congruence from its kernel. We call this function kercon.


 kercon : (𝑩 : Algebra 𝓦 𝑆){fe : dfunext π“₯ 𝓦} β†’ hom 𝑨 𝑩 β†’ Con{𝓦} 𝑨
 kercon 𝑩 {fe} h = ker ∣ h ∣ , mkcon (ker-IsEquivalence ∣ h ∣)(homker-compatible fe 𝑩 h)

With this congruence we construct the corresponding quotient, along with some syntactic sugar to denote it.


 kerquo : dfunext π“₯ 𝓦 β†’ {𝑩 : Algebra 𝓦 𝑆} β†’ hom 𝑨 𝑩 β†’ Algebra (𝓀 βŠ” 𝓦 ⁺) 𝑆
 kerquo fe {𝑩} h = 𝑨 β•± (kercon 𝑩 {fe} h)


_[_]/ker_β†Ύ_ : (𝑨 : Algebra 𝓀 𝑆)(𝑩 : Algebra 𝓦 𝑆) β†’ hom 𝑨 𝑩 β†’ dfunext π“₯ 𝓦 β†’ Algebra (𝓀 βŠ” 𝓦 ⁺) 𝑆
𝑨 [ 𝑩 ]/ker h β†Ύ fe = kerquo fe {𝑩} h

infix 60 _[_]/ker_β†Ύ_

Thus, given h : hom 𝑨 𝑩, we can construct the quotient of 𝑨 modulo the kernel of h, and the syntax for this quotient in the UALib is 𝑨 [ 𝑩 ]/ker h β†Ύ fe.

The canonical projection

Given an algebra 𝑨 and a congruence ΞΈ, the canonical projection is a map from 𝑨 onto 𝑨 β•± ΞΈ that is constructed, and proved epimorphic, as follows.


module _ {𝓀 𝓦 : Universe}{𝑨 : Algebra 𝓀 𝑆} where
 Ο€epi : (ΞΈ : Con{𝓦} 𝑨) β†’ epi 𝑨 (𝑨 β•± ΞΈ)
 Ο€epi ΞΈ = (Ξ» a β†’ βŸͺ a ⟫) , (Ξ» _ _ β†’ refl) , cΟ€-is-epic  where
  cΟ€-is-epic : Epic (Ξ» a β†’ βŸͺ a ⟫)
  cΟ€-is-epic (C , (a , refl)) =  Image_βˆ‹_.im a

In may happen that we don’t care about the surjectivity of Ο€epi, in which case would might prefer to work with the homomorphic reduct of Ο€epi. This is obtained by applying epi-to-hom, like so.


 Ο€hom : (ΞΈ : Con{𝓦} 𝑨) β†’ hom 𝑨 (𝑨 β•± ΞΈ)
 Ο€hom ΞΈ = epi-to-hom (𝑨 β•± ΞΈ) (Ο€epi ΞΈ)

We combine the foregoing to define a function that takes 𝑆-algebras 𝑨 and 𝑩, and a homomorphism h : hom 𝑨 𝑩 and returns the canonical epimorphism from 𝑨 onto 𝑨 [ 𝑩 ]/ker h. (Recall, the latter is the special notation we defined above for the quotient of 𝑨 modulo the kernel of h.)


 Ο€ker : (𝑩 : Algebra 𝓦 𝑆){fe : dfunext π“₯ 𝓦}(h : hom 𝑨 𝑩) β†’ epi 𝑨 (𝑨 [ 𝑩 ]/ker h β†Ύ fe)
 Ο€ker 𝑩 {fe} h = Ο€epi (kercon 𝑩 {fe} h)

The kernel of the canonical projection of 𝑨 onto 𝑨 / ΞΈ is equal to ΞΈ, but since equality of inhabitants of certain types (like Congruence or Rel) can be a tricky business, we settle for proving the containment 𝑨 / ΞΈ βŠ† ΞΈ. Of the two containments, this is the easier one to prove; luckily it is also the one we need later.


 open IsCongruence

 ker-in-con : {fe : dfunext π“₯ (𝓀 βŠ” 𝓦 ⁺)}(ΞΈ : Con{𝓦} 𝑨)
  β†’           βˆ€ {x}{y} β†’ ∣ kercon (𝑨 β•± ΞΈ){fe} (Ο€hom ΞΈ) ∣ x y β†’  ∣ ΞΈ ∣ x y

 ker-in-con ΞΈ hyp = /-≑ ΞΈ hyp

Product homomorphisms

Suppose we have an algebra 𝑨, a type I : π“˜ Μ‡, and a family ℬ : I β†’ Algebra 𝓦 𝑆 of algebras. We sometimes refer to the inhabitants of I as indices, and call ℬ an indexed family of algebras.

If in addition we have a family 𝒽 : (i : I) β†’ hom 𝑨 (ℬ i) of homomorphisms, then we can construct a homomorphism from 𝑨 to the product β¨… ℬ in the natural way.


module _ {π“˜ 𝓦 : Universe}{I : π“˜ Μ‡}(ℬ : I β†’ Algebra 𝓦 𝑆) where

 β¨…-hom-co : dfunext π“˜ 𝓦 β†’ {𝓀 : Universe}(𝑨 : Algebra 𝓀 𝑆) β†’ Ξ  i κž‰ I , hom 𝑨 (ℬ i) β†’ hom 𝑨 (β¨… ℬ)
 β¨…-hom-co fe 𝑨 𝒽 = (Ξ» a i β†’ ∣ 𝒽 i ∣ a) , (Ξ» 𝑓 𝒢 β†’ fe Ξ» i β†’ βˆ₯ 𝒽 i βˆ₯ 𝑓 𝒢)

The family 𝒽 of homomorphisms inhabits the dependent type Ξ  i κž‰ I , hom 𝑨 (ℬ i). The syntax we use to represent this type is available to us because of the way -Ξ  is defined in the Type Topology library. We like this syntax because it is very close to the notation one finds in the standard type theory literature. However, we could equally well have used one of the following alternatives, which may be closer to β€œstandard Agda” syntax:

Ξ  Ξ» i β†’ hom 𝑨 (ℬ i) Β  or Β  (i : I) β†’ hom 𝑨 (ℬ i) Β  or Β  βˆ€ i β†’ hom 𝑨 (ℬ i).

The foregoing generalizes easily to the case in which the domain is also a product of a family of algebras. That is, if we are given π’œ : I β†’ Algebra 𝓀 𝑆 and ℬ : I β†’ Algebra 𝓦 𝑆 (two families of 𝑆-algebras), and 𝒽 : Ξ  i κž‰ I , hom (π’œ i)(ℬ i) (a family of homomorphisms), then we can construct a homomorphism from β¨… π’œ to β¨… ℬ in the following natural way.


 β¨…-hom : dfunext π“˜ 𝓦 β†’ {𝓀 : Universe}(π’œ : I β†’ Algebra 𝓀 𝑆) β†’ Ξ  i κž‰ I , hom (π’œ i)(ℬ i) β†’ hom (β¨… π’œ)(β¨… ℬ)
 β¨…-hom fe π’œ 𝒽 = (Ξ» x i β†’ ∣ 𝒽 i ∣ (x i)) , (Ξ» 𝑓 𝒢 β†’ fe Ξ» i β†’ βˆ₯ 𝒽 i βˆ₯ 𝑓 (Ξ» x β†’ 𝒢 x i))

Projection out of products

Later we will need a proof of the fact that projecting out of a product algebra onto one of its factors is a homomorphism.


 β¨…-projection-hom : Ξ  i κž‰ I , hom (β¨… ℬ) (ℬ i)
 β¨…-projection-hom = Ξ» x β†’ (Ξ» z β†’ z x) , Ξ» _ _ β†’ refl

We could prove a more general result involving projections onto multiple factors, but so far the single-factor result has sufficed.

1 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.


↑ Homomorphisms Homomorphisms.Noether β†’