↑ Top

Homomorphism Theorems for Setoid Algebras

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


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

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

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

-- Imports from Agda and the Agda Standard Library ---------------------------
open import Data.Product     using (Ξ£-syntax ; _,_ )  renaming ( _Γ—_ to _∧_ ; proj₁ to fst)
open import Function         using ( id )             renaming ( Func to _⟢_ )
open import Level            using ( Level )
open import Relation.Binary  using ( Setoid )

open import Relation.Binary.PropositionalEquality as ≑ using ( _≑_ )

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

-- Imports from agda-algebras ------------------------------------------------
open import Overture          using ( ∣_∣ ; βˆ₯_βˆ₯ )
open import Setoid.Functions  using ( IsInjective )

open import Setoid.Algebras {𝑆 = 𝑆}               using ( Algebra ; _Μ‚_)
open import Setoid.Homomorphisms.Basic {𝑆 = 𝑆}    using ( hom ; IsHom )
open import Setoid.Homomorphisms.Kernels {𝑆 = 𝑆}  using ( kerquo ; Ο€ker )

private variable Ξ± ρᡃ Ξ² ρᡇ Ξ³ ρᢜ ΞΉ : Level

The First Homomorphism Theorem for setoid algebras


open _⟢_ using ( cong ) renaming ( f to _⟨$⟩_ )
open Algebra using ( Domain )

module _ {𝑨 : Algebra Ξ± ρᡃ}{𝑩 : Algebra Ξ² ρᡇ}(hh : hom 𝑨 𝑩) where
 open Algebra 𝑩 using ( Interp ) renaming ( Domain to B )
 open Setoid B using ( _β‰ˆ_ ; refl ; sym ; trans ) -- renaming ( _β‰ˆ_ to _β‰ˆβ‚‚_ )
 open Algebra (kerquo hh) using () renaming ( Domain to A/hKer )

 open IsHom
 private
  hfunc = ∣ hh ∣
  h = _⟨$⟩_ hfunc

 FirstHomTheorem :  Ξ£[ Ο† ∈ hom (kerquo hh) 𝑩  ]
                    ( βˆ€ a β†’ h a β‰ˆ ∣ Ο† ∣ ⟨$⟩ (∣ Ο€ker hh ∣ ⟨$⟩ a) )
                     ∧ IsInjective ∣ Ο† ∣

 FirstHomTheorem = (Ο† , Ο†hom) , (Ξ» _ β†’ refl) , Ο†mon
  where
  Ο† : A/hKer ⟢ B
  _⟨$⟩_ Ο† = h
  cong Ο† = id

  Ο†hom : IsHom (kerquo hh) 𝑩 Ο†
  compatible Ο†hom = trans (compatible βˆ₯ hh βˆ₯) (cong Interp (≑.refl , (Ξ» _ β†’ refl)))

  Ο†mon : IsInjective Ο†
  Ο†mon = id

Now we prove that the homomorphism whose existence is guaranteed by FirstHomTheorem is unique.


 FirstHomUnique :  (f g : hom (kerquo hh) 𝑩)
  β†’                ( βˆ€ a β†’  h a β‰ˆ ∣ f ∣ ⟨$⟩ (∣ Ο€ker hh ∣ ⟨$⟩ a) )
  β†’                ( βˆ€ a β†’  h a β‰ˆ ∣ g ∣ ⟨$⟩ (∣ Ο€ker hh ∣ ⟨$⟩ a) )
  β†’                βˆ€ [a]  β†’  ∣ f ∣ ⟨$⟩ [a] β‰ˆ ∣ g ∣ ⟨$⟩ [a]

 FirstHomUnique fh gh hfk hgk a = trans (sym (hfk a)) (hgk a)

← Setoid.Homomorphisms.Products Setoid.Homomorphisms.Factor β†’