↑ Top


Homomorphism Theorems

This is the Homomorphisms.Noether module of the Agda Universal Algebra Library.

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

open import Algebras.Basic using ( π“ž ; π“₯ ; Signature )

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

-- Imports from Agda and the Agda Standard Library ---------------------------------------
open import Agda.Primitive  using ( Level ) renaming ( Set to Type )
open import Data.Product    using ( Ξ£-syntax ; _,_ )
                            renaming ( _Γ—_ to _∧_ ; proj₁ to fst ; projβ‚‚ to snd)
open import Function.Base   using ( _∘_ ; id )
open import Relation.Binary using ( IsEquivalence )
open import Relation.Binary.PropositionalEquality
                            using ( module ≑-Reasoning ; _≑_ ; cong ; refl ; cong-app )

-- Imports from agda-algebras --------------------------------------------------------------
open import Overture.Preliminaries        using ( ∣_∣ ; βˆ₯_βˆ₯ ; _⁻¹ )
open import Overture.Inverses             using ( Image_βˆ‹_ )
open import Overture.Injective            using ( IsInjective )
open import Overture.Surjective           using ( IsSurjective ; SurjInv ; SurjInvIsInverseΚ³ )
open import Relations.Quotients           using ( ⌞_⌟ ; mkblk ; βŸͺ_⟫ )
open import Equality.Welldefined          using ( swelldef )
open import Equality.Truncation           using ( is-set ; blk-uip ; is-embedding ; monic-is-embedding|Set )
open import Equality.Extensionality       using ( pred-ext ; block-ext|uip )
open import Algebras.Basic                using ( Algebra ; _Μ‚_)
open import Algebras.Congruences  {𝑆 = 𝑆} using ( Con ; IsCongruence )
open import Homomorphisms.Basic   {𝑆 = 𝑆} using ( hom ; is-homomorphism ; epi ; epiβ†’hom )
open import Homomorphisms.Kernels {𝑆 = 𝑆} using ( kercon ; ker[_β‡’_]_β†Ύ_ ; Ο€ker )
private variable Ξ± Ξ² Ξ³ : Level

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

To prove that Ο† is an embedding we require

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.

open ≑-Reasoning

FirstHomTheorem|Set :

    (𝑨 : Algebra Ξ± 𝑆)(𝑩 : Algebra Ξ² 𝑆)(h : hom 𝑨 𝑩)
    (pe : pred-ext Ξ± Ξ²)(fe : swelldef π“₯ Ξ²)                          -- extensionality assumptions
    (Bset : is-set ∣ 𝑩 ∣)(buip : blk-uip ∣ 𝑨 ∣ ∣ kercon fe {𝑩} h ∣) -- truncation assumptions
    ----------------------------------------------------------------
 β†’  Ξ£[ Ο† ∈ 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.

FirstIsoTheorem|Set :

     (𝑨 : Algebra Ξ± 𝑆) (𝑩 : Algebra Ξ² 𝑆) (h : hom 𝑨 𝑩)
     (pe : pred-ext Ξ± Ξ²) (fe : swelldef π“₯ Ξ²)                        -- extensionality assumptions
     (Bset : is-set ∣ 𝑩 ∣)(buip : blk-uip ∣ 𝑨 ∣ ∣ kercon fe{𝑩}h ∣)  -- truncation assumptions
 β†’   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.

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

 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


← Homomorphisms.Basic Homomorphisms.Factor β†’