Agda UALib β

### Homomorphic Images

This section describes the Homomorphisms.HomomorphicImages module of the Agda Universal Algebra Library.

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

open import Algebras.Signatures using (Signature; π; π₯)

module Homomorphisms.HomomorphicImages {π : Signature π π₯} where

open import Homomorphisms.Isomorphisms{π = π} public

```

#### Images of a single algebra

We begin with what seems, for our purposes, the most useful way to represent the class of homomorphic images of an algebra in dependent type theory.

```
module _ {π€ π¦ : Universe} where

HomImage : {π¨ : Algebra π€ π}(π© : Algebra π¦ π)(Ο : hom π¨ π©) β β£ π© β£ β π€ β π¦ Μ
HomImage π© Ο = Ξ» b β Image β£ Ο β£ β b

HomImagesOf : Algebra π€ π β π β π₯ β π€ β π¦ βΊ Μ
HomImagesOf π¨ = Ξ£ π© κ (Algebra π¦ π) , Ξ£ Ο κ (β£ π¨ β£ β β£ π© β£) , is-homomorphism π¨ π© Ο Γ Epic Ο

```

These types should be self-explanatory, but just to be sure, letβs describe the Sigma type appearing in the second definition. Given an `π`-algebra `π¨ : Algebra π€ π`, the type `HomImagesOf π¨` denotes the class of algebras `π© : Algebra π¦ π` with a map `Ο : β£ π¨ β£ β β£ π© β£` such that `Ο` is a surjective homomorphism.

Since we take the class of homomorphic images of an algebra to be closed under isomorphism, we consider `π©` to be a homomorphic image of `π¨` if there exists an algebra `πͺ` which is a homomorphic image of `π¨` and isomorphic to `π©`. The following type expresses this.

```
_is-hom-image-of_ : (π© : Algebra π¦ π)(π¨ : Algebra π€ π) β ov π¦ β π€ Μ
π© is-hom-image-of π¨ = Ξ£ πͺΟ κ (HomImagesOf π¨) , β£ πͺΟ β£ β π©

```

#### Images of a class of algebras

Given a class `π¦` of `π`-algebras, we need a type that expresses the assertion that a given algebra is a homomorphic image of some algebra in the class, as well as a type that represents all such homomorphic images.

```
module _ {π€ : Universe} where

_is-hom-image-of-class_ : Algebra π€ π β Pred (Algebra π€ π)(π€ βΊ) β ov π€ Μ
π© is-hom-image-of-class π = Ξ£ π¨ κ (Algebra π€ π) , (π¨ β π) Γ (π© is-hom-image-of π¨)

HomImagesOfClass : Pred (Algebra π€ π) (π€ βΊ) β ov π€ Μ
HomImagesOfClass π = Ξ£ π© κ (Algebra π€ π) , (π© is-hom-image-of-class π)

```

#### Lifting tools

Here are some tools that have been useful (e.g., in the road to the proof of Birkhoffβs HSP theorem).

The first states and proves the simple fact that the lift of an epimorphism is an epimorphism.

```
open Lift

module _ {π§ π¨ : Universe} where

lift-of-alg-epic-is-epic : (π© : Universe){π¦ : Universe}
{π¨ : Algebra π§ π}(π© : Algebra π¨ π)(h : hom π¨ π©)
-----------------------------------------------
β                         Epic β£ h β£  β  Epic β£ Lift-hom π© π¦ π© h β£

lift-of-alg-epic-is-epic π© {π¦} {π¨} π© h hepi y = eq y (lift a) Ξ·
where

ΞΆ : Image β£ h β£ β (lower y)
ΞΆ = hepi (lower y)

a : β£ π¨ β£
a = Inv β£ h β£ ΞΆ

Ξ² : lift (β£ h β£ a) β‘ (lift β β£ h β£ β lower{π¦}) (lift a)
Ξ² = ap (Ξ» - β lift (β£ h β£ ( - a))) (lowerβΌlift {π¦} )

Ξ· : y β‘ β£ lh β£ (lift a)
Ξ· = y               β‘β¨ (happly liftβΌlower) y β©
lift (lower y)  β‘β¨ ap lift (InvIsInv β£ h β£ ΞΆ)β»ΒΉ β©
lift (β£ h β£ a)  β‘β¨ Ξ² β©
β£ lh β£ (lift a) β

Lift-alg-hom-image : {π© π¦ : Universe}
{π¨ : Algebra π§ π}{π© : Algebra π¨ π}
-----------------------------------------------

Lift-alg-hom-image {π©}{π¦}{π¨}{π©} ((πͺ , Ο , Οhom , Οepic) , CβB) =
(Lift-alg πͺ π¦ , β£ lΟ β£ , β₯ lΟ β₯ , lΟepic) , Lift-alg-iso CβB
where
lΟ : hom (Lift-alg π¨ π©) (Lift-alg πͺ π¦)
lΟ = (Lift-hom π© π¦ πͺ) (Ο , Οhom)

lΟepic : Epic β£ lΟ β£
lΟepic = lift-of-alg-epic-is-epic π© πͺ (Ο , Οhom) Οepic

```