---
layout: default
title : "Legacy.Base.Homomorphisms.Noether module (The Agda Universal Algebra Library)"
date : "2021-01-13"
author: "agda-algebras development team"
---

### <a id="homomorphism-theorems">Homomorphism Theorems</a>

This is the [Legacy.Base.Homomorphisms.Noether][] module of the [Agda Universal Algebra Library][].


```agda


{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Overture using ( π“ž ; π“₯ ; Signature )

module Legacy.Base.Homomorphisms.Noether {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library ---------------------------------------
open  import Data.Product     using ( Ξ£-syntax ; _,_ ; _Γ—_ )
                              renaming ( proj₁ to fst ; projβ‚‚ to snd )
open  import Function         using ( _∘_ ; id )
open  import Level            using (Level )
open  import Relation.Binary  using ( IsEquivalence )

open  import Relation.Binary.PropositionalEquality as ≑
      using ( module ≑-Reasoning ; _≑_ )

-- Imports from agda-algebras --------------------------------------------------------------
open import Legacy.Base.Relations         using ( ⌞_⌟ ; mkblk ; βŸͺ_⟫ )
open import Overture               using ( ∣_∣ ; βˆ₯_βˆ₯ ; _⁻¹ )
open import Legacy.Base.Functions         using ( Image_βˆ‹_ ; IsInjective ; SurjInv )
                                   using ( IsSurjective ; SurjInvIsInverseΚ³ )

open import Legacy.Base.Algebras {𝑆 = 𝑆}  using ( Algebra ; _Μ‚_ ; Con ; IsCongruence )

open  import Legacy.Base.Homomorphisms.Kernels {𝑆 = 𝑆}
      using ( kercon ; ker[_β‡’_]_β†Ύ_ ; Ο€ker )

open  import Legacy.Base.Equality
      using ( swelldef ; is-set ; blk-uip ; is-embedding ; monic-is-embedding|Set )
      using ( pred-ext ; block-ext|uip )

open  import Legacy.Base.Homomorphisms.Basic {𝑆 = 𝑆}
      using ( hom ; is-homomorphism ; epi ; epi→hom )

private variable Ξ± Ξ² Ξ³ : Level
```



#### <a id="the-first-homomorphism-theorem">The First Homomorphism Theorem</a>

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, proposition
extensionality, and a couple of truncation assumptions.  The extensionality
assumptions are postulated using `swelldef` and `pred-ext` which were defined
in [Legacy.Base.Equality.Welldefined][] and [Legacy.Base.Equality.Extensionality][]. As for
truncation, to prove that `Ο†` is injective we require

+   `buip`: *uniqueness of (block) identity proofs*; given two blocks of the kernel
    there is at most one proof that the blocks are equal;

To prove that `Ο†` is an embedding we require

+  `Bset`: *uniqueness of identity proofs* in the codomain; that is, the codomain
   `∣ 𝑩 ∣` is assumed to be a *set*.

Note that the classical, informal statement of the first homomorphism 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 our formal theorem statement, 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.


```agda


open ≑-Reasoning

FirstHomTheorem|Set : (𝑨 : Algebra Ξ±)(𝑩 : Algebra Ξ²)(h : hom 𝑨 𝑩)
 {- extensionality assumptions -}  (pe : pred-ext Ξ± Ξ²)(fe : swelldef π“₯ Ξ²)
 {- truncation assumptions -}      (Bset : is-set ∣ 𝑩 ∣)
                                   (buip : blk-uip ∣ 𝑨 ∣ ∣ kercon fe {𝑩} h ∣)
     -------------------------------------------------------------------------
 β†’   Ξ£[ Ο† ∈ hom (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) 𝑩  ]
     ( ∣ h ∣ ≑ ∣ Ο† ∣ ∘ ∣ Ο€ker fe{𝑩}h ∣ Γ— IsInjective ∣ Ο† ∣  Γ—  is-embedding ∣ Ο† ∣  )

FirstHomTheorem|Set 𝑨 𝑩 h pe fe Bset buip = (Ο† , Ο†hom) , ≑.refl , Ο†mon , Ο†emb
 where
  ΞΈ : Con 𝑨
  ΞΈ = kercon fe{𝑩} h
  ξ : IsEquivalence ∣ θ ∣
  ΞΎ = IsCongruence.is-equivalence βˆ₯ ΞΈ βˆ₯

  Ο† : ∣ (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) ∣ β†’ ∣ 𝑩 ∣
  Ο† a = ∣ h ∣ ⌞ a ⌟

  Ο†hom : is-homomorphism (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) 𝑩 Ο†
  Ο†hom 𝑓 a =  ∣ h ∣ ( (𝑓 Μ‚ 𝑨) (Ξ» x β†’ ⌞ a x ⌟) )  β‰‘βŸ¨ βˆ₯ h βˆ₯ 𝑓 (Ξ» x β†’ ⌞ a x ⌟)  ⟩
              (𝑓 Μ‚ 𝑩) (∣ h ∣ ∘ (Ξ» x β†’ ⌞ a x ⌟))  β‰‘βŸ¨ ≑.cong (𝑓 Μ‚ 𝑩) ≑.refl     ⟩
              (𝑓 Μ‚ 𝑩) (Ξ» x β†’ Ο† (a x))            ∎

  Ο†mon : IsInjective Ο†
  Ο†mon {_ , mkblk u ≑.refl} {_ , mkblk v ≑.refl} Ο†uv = block-ext|uip pe buip ΞΎ Ο†uv

  Ο†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.


```agda


FirstIsoTheorem|Set : (𝑨 : Algebra Ξ±) (𝑩 : Algebra Ξ²) (h : hom 𝑨 𝑩)
 {- extensionality assumptions -}  (pe : pred-ext Ξ± Ξ²) (fe : swelldef π“₯ Ξ²)
 {- truncation assumptions -}      (Bset : is-set ∣ 𝑩 ∣)
                                   (buip : blk-uip ∣ 𝑨 ∣ ∣ kercon fe{𝑩}h ∣)
 β†’                                 IsSurjective ∣ h ∣
 β†’                                 Ξ£[ f ∈ (epi (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) 𝑩)]
                                   ( ∣ h ∣ ≑ ∣ f ∣ ∘ ∣ Ο€ker fe{𝑩}h ∣
                                   Γ— IsInjective ∣ f ∣ Γ— is-embedding ∣ f ∣ )

FirstIsoTheorem|Set 𝑨 𝑩 h pe fe Bset buip hE =
 (fmap , fhom , fepic) , ≑.refl , (snd βˆ₯ FHT βˆ₯)
  where
  FHT = FirstHomTheorem|Set 𝑨 𝑩 h pe fe Bset buip

  fmap : ∣ ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe ∣ β†’ ∣ 𝑩 ∣
  fmap = fst ∣ FHT ∣

  fhom : is-homomorphism (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) 𝑩 fmap
  fhom = snd ∣ FHT ∣

  fepic : IsSurjective fmap
  fepic b = Goal where
   a : ∣ 𝑨 ∣
   a = SurjInv ∣ h ∣ hE b

   bfa : b ≑ fmap βŸͺ a ⟫
   bfa = ((SurjInvIsInverseʳ ∣ h ∣ hE) b)⁻¹

   Goal : Image fmap βˆ‹ b
   Goal = Image_βˆ‹_.eq βŸͺ a ⟫ bfa
```


Now we prove that the homomorphism `Ο†`, whose existence is guaranteed by `FirstHomTheorem|Set`, is unique.


```agda


module _ {fe : swelldef π“₯ Ξ²}(𝑨 : Algebra Ξ±)(𝑩 : Algebra Ξ²)(h : hom 𝑨 𝑩) where

 FirstHomUnique :  (f g : hom (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) 𝑩)
  β†’                ∣ h ∣ ≑ ∣ f ∣ ∘ ∣ Ο€ker fe{𝑩}h ∣
  β†’                ∣ h ∣ ≑ ∣ g ∣ ∘ ∣ Ο€ker fe{𝑩}h ∣
  β†’                βˆ€ a  β†’  ∣ f ∣ a ≑ ∣ g ∣ a

 FirstHomUnique f g hfk hgk (_ , mkblk a ≑.refl) =
  ∣ f ∣ (_ , mkblk a ≑.refl)  β‰‘βŸ¨ ≑.cong-app(hfk ⁻¹)a ⟩
  ∣ h ∣ a                     β‰‘βŸ¨ ≑.cong-app(hgk)a ⟩
  ∣ g ∣ (_ , mkblk 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.
(See [Legacy.Base.Equality.Truncation][] for a discussion of *truncation*, *sets*,
and *uniqueness of identity proofs*.)

    fe-FirstHomUnique :  {fuww : funext (Ξ± βŠ” lsuc Ξ²) Ξ²}(f g : hom (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) 𝑩)
      β†’                  ∣ h ∣ ≑ ∣ f ∣ ∘ ∣ Ο€ker fe{𝑩}h ∣
      β†’                  ∣ h ∣ ≑ ∣ g ∣ ∘ ∣ Ο€ker fe{𝑩}h ∣
      β†’                  ∣ f ∣ ≑ ∣ g ∣

    fe-FirstHomUnique {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.


```agda


 FirstIsoUnique :  (f g : epi (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ fe) 𝑩)
  β†’                ∣ h ∣ ≑ ∣ f ∣ ∘ ∣ Ο€ker fe{𝑩}h ∣
  β†’                ∣ h ∣ ≑ ∣ g ∣ ∘ ∣ Ο€ker fe{𝑩}h ∣
  β†’                βˆ€ a β†’ ∣ f ∣ a ≑ ∣ g ∣ a

 FirstIsoUnique f g hfk hgk = FirstHomUnique (epiβ†’hom 𝑩 f) (epiβ†’hom 𝑩 g) hfk hgk
```