↑ Top


Properties of Homomorphisms of Algebras

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

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

open import Overture using (𝓞 ; 𝓥 ; Signature)

module Setoid.Homomorphisms.Properties {𝑆 : Signature 𝓞 𝓥} where

-- Imports from Agda and the Agda Standard Library ------------------------------------------
open import Data.Product     using ( _,_ ) renaming ( proj₁ to fst ; proj₂ to snd )
open import Function         using ( id ) renaming ( Func to _⟶_ )
open import Level            using ( Level )
open import Relation.Binary  using ( Setoid )

open import Relation.Binary.PropositionalEquality as  using ( _≡_ )

-- Imports from the Agda Universal Algebra Library ------------------------------------------
open import Overture          using ( ∣_∣ ; ∥_∥ )
open import Setoid.Functions  using ( _∘_ ; 𝑖𝑑 ; Image_∋_ ; eq ; ∘-IsSurjective )

open  import Setoid.Algebras {𝑆 = 𝑆}
      using ( Algebra ; _̂_; Lift-Algˡ; Lift-Algʳ; Lift-Alg; 𝕌[_])
open  import Setoid.Homomorphisms.Basic {𝑆 = 𝑆}
      using ( hom ; IsHom ; epi ; IsEpi ; compatible-map )

open _⟶_ using ( cong ) renaming (f to _⟨$⟩_ )

private variable α β γ ρᵃ ρᵇ ρᶜ  : Level
Composition of homs
module _  {𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} where
  open Algebra 𝑨  renaming (Domain to A )   using ()
  open Algebra 𝑩  renaming (Domain to B )   using ()
  open Algebra 𝑪  renaming (Domain to C )   using ()
  open Setoid A   renaming ( _≈_ to _≈₁_ )  using ()
  open Setoid B   renaming ( _≈_ to _≈₂_ )  using ()
  open Setoid C   renaming ( _≈_ to _≈₃_ )  using ( trans )

  open IsHom

  -- The composition of homomorphisms is again a homomorphism
  ∘-is-hom :  {g : A  B}{h : B  C}
             IsHom 𝑨 𝑩 g  IsHom 𝑩 𝑪 h
             IsHom 𝑨 𝑪 (h  g)

  ∘-is-hom {g} {h} ghom hhom = record { compatible = c }
   where
   c : compatible-map 𝑨 𝑪 (h  g)
   c {f}{a} = trans lemg lemh
    where
    lemg : (h ⟨$⟩ (g ⟨$⟩ ((f ̂ 𝑨) a))) ≈₃ (h ⟨$⟩ ((f ̂ 𝑩)  x  g ⟨$⟩ (a x))))
    lemg = cong h (compatible ghom)

    lemh : (h ⟨$⟩ ((f ̂ 𝑩)  x  g ⟨$⟩ (a x)))) ≈₃ ((f ̂ 𝑪)  x  h ⟨$⟩ (g ⟨$⟩ (a x))))
    lemh = compatible hhom

  ∘-hom : hom 𝑨 𝑩  hom 𝑩 𝑪   hom 𝑨 𝑪
  ∘-hom (h , hhom) (g , ghom) = (g  h) , ∘-is-hom hhom ghom

  -- The composition of epimorphisms is again an epimorphism
  open IsEpi

  ∘-is-epi :  {g : A  B}{h : B  C}
             IsEpi 𝑨 𝑩 g  IsEpi 𝑩 𝑪 h  IsEpi 𝑨 𝑪 (h  g)

  ∘-is-epi gE hE = record  { isHom = ∘-is-hom (isHom gE) (isHom hE)
                           ; isSurjective = ∘-IsSurjective (isSurjective gE) (isSurjective hE)
                           }

  ∘-epi : epi 𝑨 𝑩  epi 𝑩 𝑪   epi 𝑨 𝑪
  ∘-epi (h , hepi) (g , gepi) = (g  h) , ∘-is-epi hepi gepi
Lifting and lowering of homs

First we define the identity homomorphism for setoid algebras and then we prove that the operations of lifting and lowering of a setoid algebra are homomorphisms.

module _ {𝑨 : Algebra α ρᵃ} where
 open Algebra 𝑨  renaming (Domain to A )                   using ()
 open Setoid A   renaming ( _≈_ to _≈₁_ ; refl to refl₁ )  using ( reflexive )

 𝒾𝒹 :  hom 𝑨 𝑨
 𝒾𝒹 = 𝑖𝑑 , record { compatible = reflexive ≡.refl }

module _ {𝑨 : Algebra α ρᵃ}{ : Level} where
 open Algebra 𝑨  using ()             renaming (Domain to A )
 open Setoid A   using ( reflexive )  renaming ( _≈_ to _≈₁_ ; refl to refl₁ )

 open Algebra  using ( Domain )
 open Setoid (Domain (Lift-Algˡ 𝑨 ))  using () renaming ( _≈_ to _≈ˡ_ ; refl to reflˡ)
 open Setoid (Domain (Lift-Algʳ 𝑨 ))  using () renaming ( _≈_ to _≈ʳ_ ; refl to reflʳ)

 open Level
 ToLiftˡ : hom 𝑨 (Lift-Algˡ 𝑨 )
 ToLiftˡ =  record { f = lift ; cong = id } ,
            record { compatible = reflexive ≡.refl }

 FromLiftˡ : hom (Lift-Algˡ 𝑨 ) 𝑨
 FromLiftˡ = record { f = lower ; cong = id } , record { compatible = reflˡ }

 ToFromLiftˡ :  b   ( ToLiftˡ  ⟨$⟩ ( FromLiftˡ  ⟨$⟩ b)) ≈ˡ b
 ToFromLiftˡ b = refl₁

 FromToLiftˡ :  a  ( FromLiftˡ  ⟨$⟩ ( ToLiftˡ  ⟨$⟩ a)) ≈₁ a
 FromToLiftˡ a = refl₁

 ToLiftʳ : hom 𝑨 (Lift-Algʳ 𝑨 )
 ToLiftʳ =  record { f = id ; cong = lift } ,
            record { compatible = lift (reflexive ≡.refl) }

 FromLiftʳ : hom (Lift-Algʳ 𝑨 ) 𝑨
 FromLiftʳ =  record { f = id ; cong = lower } , record { compatible = reflˡ }

 ToFromLiftʳ :  b  ( ToLiftʳ  ⟨$⟩ ( FromLiftʳ  ⟨$⟩ b)) ≈ʳ b
 ToFromLiftʳ b = lift refl₁

 FromToLiftʳ :  a  ( FromLiftʳ  ⟨$⟩ ( ToLiftʳ  ⟨$⟩ a)) ≈₁ a
 FromToLiftʳ a = refl₁

module _ {𝑨 : Algebra α ρᵃ}{ r : Level} where
 open Level
 open Algebra                            using ( Domain )
 open Setoid  (Domain 𝑨)                 using (refl)
 open Setoid  (Domain (Lift-Alg 𝑨  r))  using ( _≈_ )

 ToLift : hom 𝑨 (Lift-Alg 𝑨  r)
 ToLift = ∘-hom ToLiftˡ ToLiftʳ

 FromLift : hom (Lift-Alg 𝑨  r) 𝑨
 FromLift = ∘-hom FromLiftʳ FromLiftˡ

 ToFromLift :  b  ( ToLift  ⟨$⟩ ( FromLift  ⟨$⟩ b))  b
 ToFromLift b = lift refl


 ToLift-epi : epi 𝑨 (Lift-Alg 𝑨  r)
 ToLift-epi =  ToLift  ,
              record  { isHom =  ToLift 
                      ; isSurjective = λ {y}  eq ( FromLift  ⟨$⟩ y) (ToFromLift y)
                      }

Next we formalize the fact that a homomorphism from 𝑨 to 𝑩 can be lifted to a homomorphism from Lift-Alg 𝑨 ℓᵃ to Lift-Alg 𝑩 ℓᵇ.

module _ {𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} where
 open Algebra            using ( Domain )
 open Setoid (Domain 𝑨)  using ( reflexive )  renaming ( _≈_ to _≈₁_ )
 open Setoid (Domain 𝑩)  using ()             renaming ( _≈_ to _≈₂_ )
 open Level

 Lift-homˡ : hom 𝑨 𝑩   (ℓᵃ ℓᵇ : Level)   hom (Lift-Algˡ 𝑨 ℓᵃ) (Lift-Algˡ 𝑩 ℓᵇ)
 Lift-homˡ (f , fhom) ℓᵃ ℓᵇ = ϕ , ∘-is-hom lABh (snd ToLiftˡ)
  where
  lA lB : Algebra _ _
  lA = Lift-Algˡ 𝑨 ℓᵃ
  lB = Lift-Algˡ 𝑩 ℓᵇ

  ψ : Domain lA  Domain 𝑩
  ψ ⟨$⟩ x = f ⟨$⟩ (lower x)
  cong ψ = cong f

  lABh : IsHom lA 𝑩 ψ
  lABh = ∘-is-hom (snd FromLiftˡ) fhom

  ϕ : Domain lA  Domain lB
  ϕ ⟨$⟩ x = lift (f ⟨$⟩ (lower x))
  cong ϕ = cong f

 Lift-homʳ : hom 𝑨 𝑩   (rᵃ rᵇ : Level)   hom (Lift-Algʳ 𝑨 rᵃ) (Lift-Algʳ 𝑩 rᵇ)
 Lift-homʳ (f , fhom) rᵃ rᵇ = ϕ , Goal
  where
  lA lB : Algebra _ _
  lA = Lift-Algʳ 𝑨 rᵃ
  lB = Lift-Algʳ 𝑩 rᵇ
  ψ : Domain lA  Domain 𝑩
  ψ ⟨$⟩ x = f ⟨$⟩ x
  cong ψ xy = cong f (lower xy)

  lABh : IsHom lA 𝑩 ψ
  lABh = ∘-is-hom (snd FromLiftʳ) fhom

  ϕ : Domain lA  Domain lB
  ϕ ⟨$⟩ x = f ⟨$⟩ x
  lower (cong ϕ xy) = cong f (lower xy)

  Goal : IsHom lA lB ϕ
  Goal = ∘-is-hom lABh (snd ToLiftʳ)

 open Setoid using ( _≈_ )

 lift-hom-lemma :  (h : hom 𝑨 𝑩)(a : 𝕌[ 𝑨 ])(ℓᵃ ℓᵇ : Level)
                  (_≈_ (Domain (Lift-Algˡ 𝑩 ℓᵇ))) (lift ( h  ⟨$⟩ a))
                   ( Lift-homˡ h ℓᵃ ℓᵇ  ⟨$⟩ lift a)

 lift-hom-lemma h a ℓᵃ ℓᵇ = Setoid.refl (Domain 𝑩)

module _ {𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} where

 Lift-hom :  hom 𝑨 𝑩   (ℓᵃ rᵃ ℓᵇ rᵇ : Level)
            hom (Lift-Alg 𝑨 ℓᵃ rᵃ) (Lift-Alg 𝑩 ℓᵇ rᵇ)

 Lift-hom φ ℓᵃ rᵃ ℓᵇ rᵇ = Lift-homʳ (Lift-homˡ φ ℓᵃ ℓᵇ) rᵃ rᵇ

 Lift-hom-fst : hom 𝑨 𝑩   ( r : Level)   hom (Lift-Alg 𝑨  r) 𝑩
 Lift-hom-fst φ _ _ = ∘-hom FromLift φ

 Lift-hom-snd : hom 𝑨 𝑩   ( r : Level)   hom 𝑨 (Lift-Alg 𝑩  r)
 Lift-hom-snd φ _ _ = ∘-hom φ ToLift 

← Setoid.Homomorphisms.Basic Setoid.Homomorphisms.Kernels →