↑ Top


Kernels of Homomorphisms

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

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

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

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

-- Imports from Agda and the Agda Standard Library ------------------------------------------
open  import Data.Product      using ( _,_ )
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 ()

-- Imports from the Agda Universal Algebra Library ------------------------------------------
open  import Overture          using  ( ∣_∣ ; βˆ₯_βˆ₯ )
open  import Base.Relations    using  ( kerRel ; kerRelOfEquiv )
open  import Setoid.Functions  using  ( Image_βˆ‹_ )

open  import Setoid.Algebras {𝑆 = 𝑆}
      using ( Algebra ; _Μ‚_ ; ov ; _βˆ£β‰ˆ_ ; Con ; mkcon ; _β•±_ ; IsCongruence )

open  import Setoid.Homomorphisms.Basic {𝑆 = 𝑆}
      using ( hom ; IsHom ; epi ; IsEpi ; epi→hom )

open  import Setoid.Homomorphisms.Properties {𝑆 = 𝑆} using ( 𝒾𝒹 )

private variable  Ξ± Ξ² ρᡃ ρᡇ β„“ : Level

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

module _ {𝑨 : Algebra Ξ± ρᡃ}{𝑩 : Algebra Ξ² ρᡇ} (hh : hom 𝑨 𝑩) where

 open Setoid (Domain 𝑨)  renaming ( _β‰ˆ_ to _β‰ˆβ‚_ )  using ( reflexive )
 open Algebra 𝑩          renaming (Domain to B )   using ( Interp )
 open Setoid B           renaming ( _β‰ˆ_ to _β‰ˆβ‚‚_ )
                         using ( sym ; trans ; isEquivalence )
 private h = _⟨$⟩_ ∣ hh ∣

HomKerComp asserts that the kernel of a homomorphism is compatible with the basic operations. That is, if each (u i, v i) belongs to the kernel, then so does the pair ((f Μ‚ 𝑨) u , (f Μ‚ 𝑨) v).

 HomKerComp : 𝑨 βˆ£β‰ˆ kerRel _β‰ˆβ‚‚_ h
 HomKerComp f {u}{v} kuv = Goal
  where
  fhuv : (f Μ‚ 𝑩)(h ∘ u) β‰ˆβ‚‚ (f Μ‚ 𝑩)(h ∘ v)
  fhuv = cong Interp (≑.refl , kuv)

  lem1 : h ((f Μ‚ 𝑨) u) β‰ˆβ‚‚ (f Μ‚ 𝑩)(h ∘ u)
  lem1 = IsHom.compatible βˆ₯ hh βˆ₯

  lem2 : (f Μ‚ 𝑩) (h ∘ v) β‰ˆβ‚‚ h ((f Μ‚ 𝑨) v)
  lem2 = sym (IsHom.compatible βˆ₯ hh βˆ₯)

  Goal : h ((f Μ‚ 𝑨) u) β‰ˆβ‚‚ h ((f Μ‚ 𝑨) v)
  Goal = trans lem1 (trans fhuv lem2)

The kernel of a homomorphism is a congruence of the domain, which we construct as follows.

 kercon : Con 𝑨
 kercon =  kerRel _β‰ˆβ‚‚_ h ,
           mkcon (Ξ» x β†’ cong ∣ hh ∣ x)(kerRelOfEquiv isEquivalence h)(HomKerComp)

Now that we have a congruence, we can construct the quotient relative to the kernel.

 kerquo : Algebra Ξ± ρᡇ
 kerquo = 𝑨 β•± kercon

ker[_β‡’_]_ :  (𝑨 : Algebra Ξ± ρᡃ) (𝑩 : Algebra Ξ² ρᡇ) β†’ hom 𝑨 𝑩 β†’ Algebra _ _
ker[ 𝑨 β‡’ 𝑩 ] h = kerquo h

The canonical projection

Given an algebra 𝑨 and a congruence ΞΈ, the canonical projection is a map from 𝑨 onto 𝑨 β•± ΞΈ that is constructed, and proved epimorphic, as follows.

module _ {𝑨 : Algebra Ξ± ρᡃ}{𝑩 : Algebra Ξ² ρᡇ} (h : hom 𝑨 𝑩) where
 open IsCongruence

 Ο€epi : (ΞΈ : Con 𝑨 {β„“}) β†’ epi 𝑨 (𝑨 β•± ΞΈ)
 Ο€epi ΞΈ = p , pepi
  where

  open Algebra (𝑨 β•± ΞΈ)      using () renaming ( Domain to A/ΞΈ )
  open Setoid A/ΞΈ           using ( sym ; refl )
  open IsHom {𝑨 = (𝑨 β•± ΞΈ)}  using ( compatible )

  p : (Domain 𝑨) ⟢ A/ΞΈ
  p = record { f = id ; cong = reflexive βˆ₯ ΞΈ βˆ₯ }

  pepi : IsEpi 𝑨 (𝑨 β•± ΞΈ) p
  pepi = record  { isHom = record { compatible = sym (compatible βˆ₯ 𝒾𝒹 βˆ₯) }
                 ; isSurjective = Ξ» {y} β†’ Image_βˆ‹_.eq y refl
                 }

In may happen that we don’t care about the surjectivity of Ο€epi, in which case would might prefer to work with the homomorphic reduct of Ο€epi. This is obtained by applying epi-to-hom, like so.

 Ο€hom : (ΞΈ : Con 𝑨 {β„“}) β†’ hom 𝑨 (𝑨 β•± ΞΈ)
 Ο€hom ΞΈ = epiβ†’hom 𝑨 (𝑨 β•± ΞΈ) (Ο€epi ΞΈ)

We combine the foregoing to define a function that takes 𝑆-algebras 𝑨 and 𝑩, and a homomorphism h : hom 𝑨 𝑩 and returns the canonical epimorphism from 𝑨 onto 𝑨 [ 𝑩 ]/ker h. (Recall, the latter is the special notation we defined above for the quotient of 𝑨 modulo the kernel of h.)

 Ο€ker : epi 𝑨 (ker[ 𝑨 β‡’ 𝑩 ] h)
 Ο€ker = Ο€epi (kercon h)

The kernel of the canonical projection of 𝑨 onto 𝑨 / ΞΈ is equal to ΞΈ, but since equality of inhabitants of certain types (like Congruence or Rel) can be a tricky business, we settle for proving the containment 𝑨 / ΞΈ βŠ† ΞΈ. Of the two containments, this is the easier one to prove; luckily it is also the one we need later.

 open IsCongruence

 ker-in-con : {ΞΈ : Con 𝑨 {β„“}} β†’ βˆ€ {x}{y} β†’ ∣ kercon (Ο€hom ΞΈ) ∣ x y β†’  ∣ ΞΈ ∣ x y
 ker-in-con = id

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