Agda UALib β

### Homomorphism Theorems

This chapter presents the Homomorphisms.Noether module of the Agda Universal Algebra Library.

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

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

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

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

```

#### The First Homomorphism Theorem

Here we formalize a version of the first homomorphism theorem, sometimes called Noetherβs first homomorphism theorem, after Emmy Noether who was among the first proponents of the abstract approach to the subject that we now call βmodern algebraβ).

Informally, the theorem states that every homomorphism from `π¨` to `π©` (`π`-algebras) factors through the quotient algebra `π¨ β± ker h` (`π¨` modulo the kernel of the given homomorphism). In other terms, given `h : hom π¨ π©` there exists `Ο : hom (π¨ β± ker h) π©` which, when composed with the canonical projection `Οker : π¨ β  π¨ β± ker h`, is equal to `h`; that is, `h = Ο β Οker`. Moreover, `Ο` is a monomorphism (injective homomorphism) and is unique.

Our formal proof of this theorem will require function extensionality as well as a couple of truncation assumptions. The function extensionality postulate (`fe`) will be clear enough. As for truncation, proving that `Ο` is monic will require the following postulates:1

• Uniqueness of (codomain) Identity Proofs (`UIPcod`): the codomain `β£ π© β£` is a set, that is, has unique identity proofs.
• Uniqueness of (block) Membership Proofs (`UMPblk`): given any pair of blocks of the kernel there is at most one proof that the given blocks are equal;

And proving that `Ο` is an embedding requires

• Uniqueness of (kernel) Membership Proofs (`UMPker`): the kernel of `h` inhabits the type `Predβ` of binary propositions so there is at most one proof that a given pair belongs to the kernel relation;

Note that the classical, informal statement of the theorem does not demand that `Ο` be an embedding (in our sense of having subsingleton fibers), and if we left this out of the consequent of the formal theorem statement below, then we could omit from the antecedent the assumption that β£ π© β£ is a set.

Without further ado, we present our formalization of the first homomorphism theorem.2

```

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

FirstHomTheorem|Set : (π¨ : Algebra π€ π)(π© : Algebra π¦ π)(h : hom π¨ π©)
-- extensionality assumptions:
β                       pred-ext π€ π¦
β                       (fe : dfunext π₯ π¦)

-- truncation assumptions:
β                       blk-uip β£ π¨ β£ β£ kercon π© {fe} h β£

β Ξ£ Ο κ (hom (π¨ [ π© ]/ker h βΎ fe) π©) , (β£ h β£ β‘ β£ Ο β£ β β£ Οker π© {fe} h β£) Γ Monic β£ Ο β£ Γ is-embedding β£ Ο β£

FirstHomTheorem|Set π¨ π© h pe fe Bset buip = (Ο , Οhom) , Οcom , Οmon , Οemb
where
ΞΈ : Con{π¦} π¨
ΞΈ = kercon π© {fe} h
ΞΎ : IsEquivalence β£ ΞΈ β£
ΞΎ = IsCongruence.is-equivalence β₯ ΞΈ β₯

Ο : β£ (π¨ [ π© ]/ker h βΎ fe) β£ β β£ π© β£
Ο a = β£ h β£ β a β

Οhom : is-homomorphism (π¨ [ π© ]/ker h βΎ fe) π© Ο
Οhom π π =  β£ h β£ ( (π Μ π¨) (Ξ» x β β π x β) ) β‘β¨ β₯ h β₯ π (Ξ» x β β π x β)  β©
(π Μ π©) (β£ h β£ β (Ξ» x β β π x β)) β‘β¨ ap (π Μ π©) (fe Ξ» x β refl) β©
(π Μ π©) (Ξ» x β Ο (π x))             β

Οmon : Monic Ο
Οmon (_ , (u , refl)) (_ , (v , refl)) Οuv = block-ext|uip pe buip ΞΎ Οuv

Οcom : β£ h β£ β‘ Ο β β£ Οker π©{fe} h β£
Οcom = refl

Οemb : is-embedding Ο
Οemb = monic-is-embedding|Set Ο Bset Οmon

```

Below we will prove that the homomorphism `Ο`, whose existence we just proved, is unique (see `NoetherHomUnique`), but first we show that if we add to the hypotheses of the first homomorphism theorem the assumption that `h` is surjective, then we obtain the so-called first isomorphism theorem. Naturally, we let `FirstHomTheorem|Set` do most of the work. (Note that the proof also requires an additional local function extensionality postulate.)

```
FirstIsoTheorem|Set : (π¨ : Algebra π€ π)(π© : Algebra π¦ π)(h : hom π¨ π©)
-- extensionality assumptions:
β                       pred-ext π€ π¦
β                       (fe : dfunext π₯ π¦)
β                       dfunext π¦ π¦

-- truncation assumptions:
β                       blk-uip β£ π¨ β£ β£ kercon π©{fe}h β£

β Epic β£ h β£
β Ξ£ f κ epi (π¨ [ π© ]/ker h βΎ fe) π© , (β£ h β£ β‘ β£ f β£ β β£ Οker π©{fe}h β£) Γ Monic β£ f β£ Γ is-embedding β£ f β£

FirstIsoTheorem|Set π¨ π© h pe fe feww Bset buip hE = (fmap , fhom , fepic) , refl , (snd β₯ FHT β₯)
where
FHT = FirstHomTheorem|Set π¨ π© h pe fe Bset buip  -- (Ο , Οhom) , Οcom , Οmon , Οemb

fmap : β£ π¨ [ π© ]/ker h βΎ fe β£ β β£ π© β£
fmap = fst β£ FHT β£

fhom : is-homomorphism (π¨ [ π© ]/ker h βΎ fe) π© fmap
fhom = snd β£ FHT β£

fepic : Epic fmap
fepic b = Ξ³ where
a : β£ π¨ β£
a = EpicInv β£ h β£ hE b

bfa : b β‘ fmap βͺ a β«
bfa = (cong-app (EpicInvIsRightInv {fe = feww} β£ h β£ hE) b)β»ΒΉ

Ξ³ : Image fmap β b
Ξ³ = Image_β_.eq b βͺ a β« bfa

```

Now we prove that the homomorphism `Ο`, whose existence is guaranteed by `FirstHomomorphismTheorem`, is unique.

```
module _ {π€ π¦ : Universe}{fe : dfunext π₯ π¦}(π¨ : Algebra π€ π)(π© : Algebra π¦ π)(h : hom π¨ π©) where

NoetherHomUnique : (f g : hom (π¨ [ π© ]/ker h βΎ fe) π©)
β                 β£ h β£ β‘ β£ f β£ β β£ Οker π© {fe} h β£ β β£ h β£ β‘ β£ g β£ β β£ Οker π©{fe} h β£
β                 β a  β  β£ f β£ a β‘ β£ g β£ a

NoetherHomUnique f g hfk hgk (_ , (a , refl)) = β£ f β£ (_ , (a , refl)) β‘β¨ cong-app(hfk β»ΒΉ)a β©
β£ h β£ a                β‘β¨ cong-app(hgk)a β©
β£ g β£ (_ , (a , refl)) β

```

If, in addition, we postulate extensionality of functions defined on the domain `π¨ [ π© ]/ker h`, then we obtain the following variation of the last result.1

```
fe-NoetherHomUnique : {fuww : funext (π€ β π¦ βΊ) π¦}(f g : hom (π¨ [ π© ]/ker h βΎ fe) π©)
β  β£ h β£ β‘ β£ f β£ β β£ Οker π©{fe} h β£  β  β£ h β£ β‘ β£ g β£ β β£ Οker π©{fe} h β£  β  β£ f β£ β‘ β£ g β£

fe-NoetherHomUnique {fuww} f g hfk hgk = fuww (NoetherHomUnique f g hfk hgk)

```

The proof of `NoetherHomUnique` goes through for the special case of epimorphisms, as we now verify.

```
NoetherIsoUnique : (f g : epi (π¨ [ π© ]/ker h βΎ fe) π©)
β                 β£ h β£ β‘ β£ f β£ β β£ Οker π©{fe} h β£ β β£ h β£ β‘ β£ g β£ β β£ Οker π© {fe} h β£
β                 β a β β£ f β£ a β‘ β£ g β£ a

NoetherIsoUnique f g hfk hgk = NoetherHomUnique (epi-to-hom π© f) (epi-to-hom π© g) hfk hgk

```

#### Homomorphism composition

The composition of homomorphisms is again a homomorphism. We formalize this in a number of alternative ways.

```
module _ {π§ π¨ π© : Universe} (π¨ : Algebra π§ π){π© : Algebra π¨ π}(πͺ : Algebra π© π) where

β-hom : hom π¨ π©  β  hom π© πͺ  β  hom π¨ πͺ
β-hom (g , ghom) (h , hhom) = h β g , Ξ³ where

Ξ³ : β π a β (h β g)((π Μ π¨) a) β‘ (π Μ πͺ)(h β g β a)

Ξ³ π a = (h β g) ((π Μ π¨) a) β‘β¨ ap h ( ghom π a ) β©
h ((π Μ π©) (g β a)) β‘β¨ hhom π ( g β a ) β©
(π Μ πͺ) (h β g β a) β

β-is-hom : {f : β£ π¨ β£ β β£ π© β£} {g : β£ π© β£ β β£ πͺ β£}
β         is-homomorphism π¨ πͺ (g β f)

β-is-hom {f} {g} fhom ghom = β₯ β-hom (f , fhom) (g , ghom) β₯

```

#### Homomorphism decomposition

If `g : hom π¨ π©`, `h : hom π¨ πͺ`, `h` is surjective, and `ker h β ker g`, then there exists `Ο : hom πͺ π©` such that `g = Ο β h`, that is, such that the following diagram commutes;

``````π¨---- h -->>πͺ
\         .
\       .
g     βΟ
\   .
\ .
V
``````

This, or some variation of it, is sometimes referred to as the Second Isomorphism Theorem. We formalize its statement and proof as follows. (Notice that the proof is constructive.)

```module _ {π€ : Universe}{π¨ π© πͺ : Algebra π€ π} where
homFactor : funext π€ π€ β (g : hom π¨ π©)(h : hom π¨ πͺ)
β          kernel β£ h β£ β kernel β£ g β£ β Epic β£ h β£
-------------------------------------------
β          Ξ£ Ο κ (hom πͺ π©) , β£ g β£ β‘ β£ Ο β£ β β£ h β£

homFactor fe(g , ghom)(h , hhom) KhβKg hEpi = (Ο , ΟIsHomCB) , gΟh
where
hInv : β£ πͺ β£ β β£ π¨ β£
hInv = Ξ» c β (EpicInv h hEpi) c

Ο : β£ πͺ β£ β β£ π© β£
Ο = Ξ» c β g ( hInv c )

ΞΎ : β x β kernel h (x , hInv (h x))
ΞΎ x = (cong-app (EpicInvIsRightInv {fe = fe} h hEpi) (h x))β»ΒΉ

gΟh : g β‘ Ο β h
gΟh = fe  Ξ» x β KhβKg (ΞΎ x)

ΞΆ : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£)(x : β₯ π β₯ π) β  π x β‘ (h β hInv)(π x)
ΞΆ  π π x = (cong-app (EpicInvIsRightInv {fe = fe} h hEpi) (π x))β»ΒΉ

ΞΉ : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£) β  π β‘ h β (hInv β π)
ΞΉ π π = ap (Ξ» - β - β π)(EpicInvIsRightInv {fe = fe} h hEpi)β»ΒΉ

useker : β π π β g(hInv (h((π Μ π¨)(hInv β π)))) β‘ g((π Μ π¨)(hInv β π))
useker π c = KhβKg (cong-app (EpicInvIsRightInv{fe = fe} h hEpi)
(h ((π Μ π¨)(hInv β c))) )

ΟIsHomCB : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£) β Ο((π Μ πͺ) π) β‘ (π Μ π©)(Ο β π)

ΟIsHomCB π π =  g (hInv ((π Μ πͺ) π))              β‘β¨ i   β©
g (hInv ((π Μ πͺ)(h β (hInv β π)))) β‘β¨ ii  β©
g (hInv (h ((π Μ π¨)(hInv β π))))   β‘β¨ iii β©
g ((π Μ π¨)(hInv β π))              β‘β¨ iv  β©
(π Μ π©)(Ξ» x β g (hInv (π x)))      β
where
i   = ap (g β hInv) (ap (π Μ πͺ) (ΞΉ π π))
ii  = ap (g β hInv) (hhom π (hInv β π))β»ΒΉ
iii = useker π π
iv  = ghom π (hInv β π)

```

Hereβs a more general version.

``````π¨ --- Ξ³ ->> πͺ
\         .
\       .
Ξ²     βΟ
\   .
\ .
V
``````
```
module _ {π§ π¨ π© : Universe}{π¨ : Algebra π§ π}{πͺ : Algebra π© π} where

HomFactor : funext π§ π¨ β funext π© π© β (π© : Algebra π¨ π)(Ξ± : hom π¨ π©)(Ξ² : hom π¨ πͺ)
β          kernel β£ Ξ² β£ β kernel β£ Ξ± β£ β Epic β£ Ξ² β£
-------------------------------------------
β          Ξ£ Ο κ (hom πͺ π©) , β£ Ξ± β£ β‘ β£ Ο β£ β β£ Ξ² β£

HomFactor fxy fzz π© Ξ± Ξ² KΞ²Ξ± Ξ²E = (Ο , ΟIsHomCB) , Ξ±ΟΞ²
where
Ξ²Inv : β£ πͺ β£ β β£ π¨ β£
Ξ²Inv = Ξ» y β (EpicInv β£ Ξ² β£ Ξ²E) y

Ο : β£ πͺ β£ β β£ π© β£
Ο = Ξ» y β β£ Ξ± β£ ( Ξ²Inv y )

ΞΎ : (x : β£ π¨ β£) β kernel β£ Ξ² β£ (x , Ξ²Inv (β£ Ξ² β£ x))
ΞΎ x =  ( cong-app (EpicInvIsRightInv {fe = fzz} β£ Ξ² β£ Ξ²E) ( β£ Ξ² β£ x ) )β»ΒΉ

Ξ±ΟΞ² : β£ Ξ± β£ β‘ Ο β β£ Ξ² β£
Ξ±ΟΞ² = fxy Ξ» x β KΞ²Ξ± (ΞΎ x)

ΞΉ : (π : β£ π β£)(π : β₯ π β₯ π β β£ πͺ β£) β π β‘  β£ Ξ² β£ β (Ξ²Inv β π)
ΞΉ π π = ap (Ξ» - β - β π) (EpicInvIsRightInv{fe = fzz} β£ Ξ² β£ Ξ²E)β»ΒΉ

useker : β π π β β£ Ξ± β£ (Ξ²Inv (β£ Ξ² β£((π Μ π¨)(Ξ²Inv β π)))) β‘ β£ Ξ± β£((π Μ π¨)(Ξ²Inv β π))
useker π π = KΞ²Ξ± (cong-app (EpicInvIsRightInv {fe = fzz} β£ Ξ² β£ Ξ²E)
(β£ Ξ² β£ ((π Μ π¨)(Ξ²Inv β π))))

ΟIsHomCB : β π π β Ο ((π Μ πͺ) π) β‘ ((π Μ π©)(Ο β π))

ΟIsHomCB π π = β£ Ξ± β£ (Ξ²Inv ((π Μ πͺ) π))                   β‘β¨ i   β©
β£ Ξ± β£ (Ξ²Inv ((π Μ πͺ)(β£ Ξ² β£ β (Ξ²Inv β π)))) β‘β¨ ii  β©
β£ Ξ± β£ (Ξ²Inv (β£ Ξ² β£ ((π Μ π¨)(Ξ²Inv β π))))   β‘β¨ iii β©
β£ Ξ± β£ ((π Μ π¨)(Ξ²Inv β π))                  β‘β¨ iv  β©
((π Μ π©)(Ξ» x β β£ Ξ± β£ (Ξ²Inv (π x))))        β
where
i   = ap (β£ Ξ± β£ β Ξ²Inv) (ap (π Μ πͺ) (ΞΉ π π))
ii  = ap (β£ Ξ± β£ β Ξ²Inv) (β₯ Ξ² β₯ π (Ξ²Inv β π))β»ΒΉ
iii = useker π π
iv  = β₯ Ξ± β₯ π (Ξ²Inv β π)

```

If, in addition to the hypotheses of the last theorem, we assume Ξ± is epic, then so is Ο. (Note that the proof also requires an additional local function extensionality postulate, `funext π¨ π¨`.)

```
HomFactorEpi : funext π§ π¨ β funext π© π© β funext π¨ π¨
β             (π© : Algebra π¨ π)(Ξ± : hom π¨ π©)(Ξ² : hom π¨ πͺ)
β             kernel β£ Ξ² β£ β kernel β£ Ξ± β£ β Epic β£ Ξ² β£ β Epic β£ Ξ± β£
----------------------------------------------------------
β             Ξ£ Ο κ (epi πͺ π©) , β£ Ξ± β£ β‘ β£ Ο β£ β β£ Ξ² β£

HomFactorEpi fxy fzz fyy π© Ξ± Ξ² kerincl Ξ²e Ξ±e = (fst β£ ΟF β£ , (snd β£ ΟF β£ , ΟE)) , β₯ ΟF β₯
where
ΟF : Ξ£ Ο κ (hom πͺ π©) , β£ Ξ± β£ β‘ β£ Ο β£ β β£ Ξ² β£
ΟF = HomFactor fxy fzz π© Ξ± Ξ² kerincl Ξ²e

Ξ²inv : β£ πͺ β£ β β£ π¨ β£
Ξ²inv = Ξ» c β (EpicInv β£ Ξ² β£ Ξ²e) c

Ξ±inv : β£ π© β£ β β£ π¨ β£
Ξ±inv = Ξ» b β (EpicInv β£ Ξ± β£ Ξ±e) b

Ο : β£ πͺ β£ β β£ π© β£
Ο = Ξ» c β β£ Ξ± β£ ( Ξ²inv c )

ΟE : Epic Ο
ΟE = epic-factor {fe = fyy} β£ Ξ± β£ β£ Ξ² β£ Ο β₯ ΟF β₯ Ξ±e

```

1 See Relations.Truncation for a discussion of truncation, sets, and uniqueness of proofs.

2 In this module we are already assuming global function extensionality (`gfe`), and we could just appeal to `gfe` (e.g., in the proof of `FirstHomomorphismTheorem`) instead of adding local function extensionality (\ab{fe}) to the list of assumptions. However, we sometimes add an extra extensionality postulate in order to highlight where and how the principle is applied.}