---
layout: default
title : "Setoid.Homomorphisms.Properties module (Agda Universal Algebra Library)"
date : "2021-09-13"
author: "agda-algebras development team"
---

#### Properties of Homomorphisms of Algebras

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

This module collects some of the facts that follow from the definition of a
homomorphism alone, before any theory.  These include the following:

+  homomorphisms and epimorphisms compose;
+  if a relation `R` is contained in the kernel of a homomorphism, then the
   congruence generated by `R` is also contained in the kernel;
+  the universe liftings and lowerings of an algebra are homomorphisms, and
   surjective in the lifting direction.

The lifting results are the ones we use most.  Agda's universes are not
cumulative, so an algebra defined at one universe level cannot be used directly at
a higher universe level.  `Lift-Alg`{.AgdaFunction} of [Setoid.Algebras.Basic][]
lifts an algebra to a higher level, and the homomorphisms defined here
(`ToLift`{.AgdaFunction}, `FromLift`{.AgdaFunction}, `Lift-hom`{.AgdaFunction} and
their one-sided variants) are what prove this lift harmless.
[Setoid.Homomorphisms.Isomorphisms][] assembles these facts into
`Lift-≅`{.AgdaFunction}, and the closure operators of [Setoid.Varieties.Closure][]
rely on them at every change of level.

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Homomorphisms.Properties  where

-- Imports from Agda and the Agda Standard Library ------------------------------------------
open import Data.Product                           using ( _,_ ; proj₁ ; proj₂ )
open import Function     renaming ( Func to _⟶_ )  using ( id ; _$_ ; _∘_ )
open import Level                                  using ( Level ; _⊔_ )
open import Relation.Binary                        using ( Setoid )
                                                   renaming ( Rel to BinaryRel ; _⇒_ to _⊆_)
open import Relation.Binary.PropositionalEquality  using ( refl)

-- Imports from the Agda Universal Algebra Library ------------------------------------------
open import Overture                       using  ( 𝓞 ; 𝓥 ; Signature )
open import Setoid.Algebras                using  ( Algebra ; _^_; Lift-Algˡ ; Lift-Algʳ
                                                  ; Lift-Alg; 𝕌[_] ; 𝔻[_] )
open import Setoid.Congruences.Generation  using  ( Gen ; Cg-least )
open import Setoid.Functions               using  ( _⊙_ ; eq ; ⊙-IsSurjective )
open import Setoid.Homomorphisms.Basic     using  ( hom ; IsHom ; epi ; IsEpi )
open import Setoid.Homomorphisms.Kernels   using  ( kercon )

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

private variable
  α β γ ρᵃ ρᵇ ρᶜ ℓ : Level
  𝑆 : Signature 𝓞 𝓥
```
-->

##### Composition of homs

The composite of two homomorphisms is a homomorphism, and the composite of two
epimorphisms is an epimorphism.

+  `⊙-is-hom`{.AgdaFunction} is the predicate form: from `IsHom 𝑨 𝑩 g` and `IsHom
   𝑩 𝑪 h` it proves `IsHom 𝑨 𝑪 (h ⊙ g)`, by transitivity through two steps, first
   pushing `g`'s compatibility across `h` with `cong h`, then applying `h`'s own
   compatibility.
+  `⊙-is-epi`{.AgdaFunction} adds surjectivity of the composite, which is
   `⊙-IsSurjective`{.AgdaFunction} of [Setoid.Functions.Surjective][].
+  `⊙-hom`{.AgdaFunction} and `⊙-epi`{.AgdaFunction} are the bundled forms.

All four take their arguments in *diagrammatic* order, the map out of `𝑨` first
and the map out of `𝑩` second, although the underlying composition
`_⊙_`{.AgdaFunction} of [Setoid.Functions.Basic][] is written right to left; so
`⊙-hom f g` is read as "apply `f`, then `g`".

```agda
module _
  {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}
  {𝑩 : Algebra β ρᵇ}
  {𝑪 : Algebra γ ρᶜ}
  where
  open Setoid 𝔻[ 𝑨 ] renaming ( _≈_ to _≈₁_ ) using ()
  open Setoid 𝔻[ 𝑪 ] renaming ( _≈_ to _≈₃_ ) using ( trans )
  open IsHom
  open IsEpi

  -- The composition of homomorphisms is again a homomorphism
  ⊙-is-hom : {g : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]} {h : 𝔻[ 𝑩 ] ⟶ 𝔻[ 𝑪 ]}
    → IsHom 𝑨 𝑩 g → IsHom 𝑩 𝑪 h → IsHom 𝑨 𝑪 (h ⊙ g)
  ⊙-is-hom {g} {h} ghom hhom .compatible {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
  ⊙-is-epi : {g : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]} {h : 𝔻[ 𝑩 ] ⟶ 𝔻[ 𝑪 ]}
    → IsEpi 𝑨 𝑩 g → IsEpi 𝑩 𝑪 h → IsEpi 𝑨 𝑪 (h ⊙ g)
  ⊙-is-epi gE hE .isHom = ⊙-is-hom (isHom gE) (isHom hE)
  ⊙-is-epi gE hE .isSurjective = ⊙-IsSurjective (isSurjective gE) (isSurjective hE)

  ⊙-epi : epi 𝑨 𝑩 → epi 𝑩 𝑪  → epi 𝑨 𝑪
  ⊙-epi (h , hepi) (g , gepi) = g ⊙ h , ⊙-is-epi hepi gepi
```

#### A kernel that collapses `R` contains the congruence generated by `R`

If a relation `R` is contained in the kernel of a homomorphism `h` (i.e., `h`
collapses every `R`-pair), then the congruence `Cg R` generated by `R` is also
contained in that kernel.  This is exactly `Cg-least`{.AgdaFunction} applied to
the kernel congruence `kercon h`{.AgdaFunction}: the kernel is a congruence above
`R`, hence above the least such, `Cg R`.

```agda
Cg⊆ker : {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ}
  (h : hom 𝑨 𝑩) {R : BinaryRel 𝕌[ 𝑨 ] ℓ}
  → R ⊆ proj₁ (kercon h) → Gen R ⊆ proj₁ (kercon h)

Cg⊆ker h R⊆k = Cg-least (kercon h) R⊆k
```


##### Lifting and lowering of homs

This section establishes that the operations of lifting and lowering of a setoid
algebra are homomorphisms.

```agda
module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{ℓ : Level} where
  open Level                       using ( lift ; lower )
  open IsHom                       using (compatible)
  open Setoid 𝔻[ 𝑨 ]              using () renaming ( _≈_ to _≈₁_ ; refl to refl₁ )
  open Setoid 𝔻[ Lift-Algˡ 𝑨 ℓ ]  using () renaming ( _≈_ to _≈ˡ_ )
  open Setoid 𝔻[ Lift-Algʳ 𝑨 ℓ ]  using () renaming ( _≈_ to _≈ʳ_ )

  ToLiftˡ : hom 𝑨 (Lift-Algˡ 𝑨 ℓ)
  ToLiftˡ .proj₁ ⟨$⟩ x = lift x
  ToLiftˡ .proj₁ .cong = id
  ToLiftˡ .proj₂ .compatible = refl₁

  FromLiftˡ : hom (Lift-Algˡ 𝑨 ℓ) 𝑨
  FromLiftˡ .proj₁ ⟨$⟩ x = lower x
  FromLiftˡ .proj₁ .cong = id
  FromLiftˡ .proj₂ .compatible = refl₁

  ToFromLiftˡ : ∀ b →  ToLiftˡ .proj₁ ⟨$⟩ (FromLiftˡ .proj₁ ⟨$⟩ b) ≈ˡ b
  ToFromLiftˡ _ = refl₁

  FromToLiftˡ : ∀ a → FromLiftˡ .proj₁ ⟨$⟩ (ToLiftˡ .proj₁ ⟨$⟩ a) ≈₁ a
  FromToLiftˡ _ = refl₁

  ToLiftʳ : hom 𝑨 (Lift-Algʳ 𝑨 ℓ)
  ToLiftʳ .proj₁ ⟨$⟩ x = x
  ToLiftʳ .proj₁ .cong = lift
  ToLiftʳ .proj₂ .compatible = lift refl₁

  FromLiftʳ : hom (Lift-Algʳ 𝑨 ℓ) 𝑨
  FromLiftʳ .proj₁ ⟨$⟩ x = x
  FromLiftʳ .proj₁ .cong = lower
  FromLiftʳ .proj₂ .compatible = refl₁

  ToFromLiftʳ : ∀ b → ToLiftʳ .proj₁ ⟨$⟩ (FromLiftʳ .proj₁ ⟨$⟩ b) ≈ʳ b
  ToFromLiftʳ _ = lift refl₁

  FromToLiftʳ : ∀ a → FromLiftʳ .proj₁ ⟨$⟩ (ToLiftʳ .proj₁ ⟨$⟩ a) ≈₁ a
  FromToLiftʳ _ = refl₁

module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{ℓ r : Level} where
  open Setoid 𝔻[ 𝑨 ]               using () renaming (refl to ≈refl)
  open Setoid 𝔻[ 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 .proj₁ ⟨$⟩ (FromLift .proj₁ ⟨$⟩ b) ≈ b
  ToFromLift = Level.lift ≈refl

  ToLift-epi : epi 𝑨 (Lift-Alg 𝑨 ℓ r)
  ToLift-epi =  ToLift .proj₁ ,
                record  { isHom = ToLift .proj₂
                        ; isSurjective = λ {y} → eq (FromLift .proj₁ ⟨$⟩ y) ToFromLift
                        }
```

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

```agda
module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ} {𝑩 : Algebra β ρᵇ} where
  open Level using ( lift ; lower )

  Lift-homˡ : hom 𝑨 𝑩  → (ℓᵃ ℓᵇ : Level) →  hom (Lift-Algˡ 𝑨 ℓᵃ) (Lift-Algˡ 𝑩 ℓᵇ)
  Lift-homˡ (f , fhom) ℓᵃ ℓᵇ = ϕ , ⊙-is-hom lABh (ToLiftˡ .proj₂)
    where
    lA : Algebra (α ⊔ ℓᵃ) ρᵃ
    lA = Lift-Algˡ 𝑨 ℓᵃ

    lB : Algebra (β ⊔ ℓᵇ) ρᵇ
    lB = Lift-Algˡ 𝑩 ℓᵇ

    ψ : 𝔻[ lA ] ⟶ 𝔻[ 𝑩 ]
    ψ ⟨$⟩ x = f ⟨$⟩ (Level.lower x)
    ψ .cong = f .cong

    lABh : IsHom lA 𝑩 ψ
    lABh = ⊙-is-hom (FromLiftˡ .proj₂) fhom

    ϕ : 𝔻[ lA ] ⟶ 𝔻[ lB ]
    ϕ ⟨$⟩ x = lift (f ⟨$⟩ (lower x))
    ϕ .cong = f .cong

  Lift-homʳ : hom 𝑨 𝑩  → (rᵃ rᵇ : Level) →  hom (Lift-Algʳ 𝑨 rᵃ) (Lift-Algʳ 𝑩 rᵇ)
  Lift-homʳ (f , fhom) rᵃ rᵇ = ϕ , Goal
    where
    lA : Algebra α (ρᵃ ⊔ rᵃ)
    lA = Lift-Algʳ 𝑨 rᵃ
    lB : Algebra β (ρᵇ ⊔ rᵇ)
    lB = Lift-Algʳ 𝑩 rᵇ
    ψ : 𝔻[ lA ] ⟶ 𝔻[ 𝑩 ]
    ψ ⟨$⟩ x = f ⟨$⟩ x
    ψ .cong = f .cong ∘ lower

    lABh : IsHom lA 𝑩 ψ
    lABh = ⊙-is-hom (proj₂ FromLiftʳ) fhom

    ϕ : 𝔻[ lA ] ⟶ 𝔻[ lB ]
    ϕ ⟨$⟩ x = f ⟨$⟩ x
    ϕ .cong xy .lower = f .cong $ xy .lower

    Goal : IsHom lA lB ϕ
    Goal = ⊙-is-hom lABh (ToLiftʳ .proj₂)

  module _ (h : hom 𝑨 𝑩) (a : 𝕌[ 𝑨 ]) (ℓᵃ ℓᵇ : Level) where
    open Setoid 𝔻[ Lift-Algˡ 𝑩 ℓᵇ ] using ( _≈_ )
    lift-hom-lemma : lift (h .proj₁ ⟨$⟩ a) ≈ (Lift-homˡ h ℓᵃ ℓᵇ) .proj₁ ⟨$⟩ lift a
    lift-hom-lemma = Setoid.refl 𝔻[ 𝑩 ]

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
```