↑ Top

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 𝑨 𝑩 f β†’ is-homomorphism 𝑩 π‘ͺ 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.

← Base.Homomorphisms.Basic Base.Homomorphisms.Kernels β†’