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

And proving that Ο† is an embedding requires

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:
  β†’                       is-set ∣ 𝑩 ∣
  β†’                       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:
  β†’                       is-set ∣ 𝑩 ∣
  β†’                       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 𝑨 𝑩 f β†’ is-homomorphism 𝑩 π‘ͺ 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.}



← Homomorphisms.Basic Homomorphisms.Isomorphisms β†’