↑ Top

Basic Definitions

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


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

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

module 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 Base.Functions         using ( IsInjective ; IsSurjective )
open import Base.Algebras {𝑆 = 𝑆}  using ( Algebra ; _Μ‚_ ; Lift-Alg )

private variable Ξ± Ξ² : Level

Homomorphisms

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.


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.


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

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

Important examples of homomorphisms

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.


𝒾𝒹 : (𝑨 : 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.


open Level

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

π“β„΄π“Œβ„―π“‡ : {Ξ² : Level}(𝑨 : 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 agda-algebras library by the following types.


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


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

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

↑ Base.Homomorphisms Base.Homomorphisms.Properties β†’