↑ Top


Properties of Homomorphisms

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

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

open import Algebras.Basic

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

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Data.Product   using ( _,_ )
open import Function.Base  using ( _∘_ )
open import Level          using ( Level )
open import Relation.Binary.PropositionalEquality
                           using ( _≑_ ; module ≑-Reasoning ; cong ; refl )

-- -- Imports from the Agda Universal Algebras Library --------------------------------
open import Overture.Preliminaries       using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import 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.


← Homomorphisms.Basic Homomorphisms.Kernels β†’