↑ Top

Kernels of Homomorphisms

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

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

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

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

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Data.Product   using ( _,_ )
open import Function.Base  using ( _∘_ )
open import Level          using ( Level ; _βŠ”_ ; suc )

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

-- Imports from the Agda Universal Algebras Library --------------------------------
open import Overture        using ( ∣_∣ ; βˆ₯_βˆ₯ ; _⁻¹ )
open import Base.Functions  using ( Image_βˆ‹_ ; IsSurjective )
open import Base.Equality   using ( swelldef )
open import Base.Relations  using ( ker ; ker-IsEquivalence ; βŸͺ_⟫ ; mkblk )

open  import Base.Algebras {𝑆 = 𝑆}
      using ( Algebra ; compatible ; _Μ‚_ ; Con ; mkcon ; _β•±_ ; IsCongruence ; /-≑ )

open import Base.Homomorphisms.Basic {𝑆 = 𝑆}  using ( hom ; epi ; epiβ†’hom )

private variable Ξ± Ξ² : Level


The kernel of a homomorphism is a congruence relation and conversely for every congruence relation ΞΈ, there exists a homomorphism with kernel ΞΈ (namely, that canonical projection onto the quotient modulo ΞΈ).

module _ {𝑨 : Algebra Ξ± 𝑆} where
 open ≑-Reasoning
 homker-comp :  swelldef π“₯ Ξ² β†’ {𝑩 : Algebra Ξ² 𝑆}(h : hom 𝑨 𝑩)
  β†’             compatible 𝑨 (ker ∣ h ∣)

 homker-comp wd {𝑩} h f {u}{v} kuv =
  ∣ h ∣((f Μ‚ 𝑨) u)    β‰‘βŸ¨ βˆ₯ h βˆ₯ f u ⟩
  (f Μ‚ 𝑩)(∣ h ∣ ∘ u)  β‰‘βŸ¨ wd(f Μ‚ 𝑩)(∣ h ∣ ∘ u)(∣ h ∣ ∘ v)kuv ⟩
  (f Μ‚ 𝑩)(∣ h ∣ ∘ v)  β‰‘βŸ¨ (βˆ₯ h βˆ₯ f v)⁻¹ ⟩
  ∣ h ∣((f Μ‚ 𝑨) v)    ∎

(Notice, it is here that the swelldef postulate comes into play, and because it is needed to prove homker-comp, it is postulated by all the lemmas below that depend upon homker-comp.)

It is convenient to define a function that takes a homomorphism and constructs a congruence from its kernel. We call this function kercon.

 kercon : swelldef π“₯ Ξ² β†’ {𝑩 : Algebra Ξ² 𝑆} β†’ hom 𝑨 𝑩 β†’ Con{Ξ±}{Ξ²} 𝑨
 kercon wd {𝑩} h = ker ∣ h ∣ , mkcon (ker-IsEquivalence ∣ h ∣)(homker-comp wd {𝑩} h)

With this congruence we construct the corresponding quotient, along with some syntactic sugar to denote it.

 kerquo : swelldef π“₯ Ξ² β†’ {𝑩 : Algebra Ξ² 𝑆} β†’ hom 𝑨 𝑩 β†’ Algebra (Ξ± βŠ” suc Ξ²) 𝑆
 kerquo wd {𝑩} h = 𝑨 β•± (kercon wd {𝑩} h)

ker[_β‡’_]_β†Ύ_ :  (𝑨 : Algebra Ξ± 𝑆)(𝑩 : Algebra Ξ² 𝑆) β†’ hom 𝑨 𝑩 β†’ swelldef π“₯ Ξ²
 β†’             Algebra (Ξ± βŠ” suc Ξ²) 𝑆

ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ wd = kerquo wd {𝑩} h

Thus, given h : hom 𝑨 𝑩, we can construct the quotient of 𝑨 modulo the kernel of h, and the syntax for this quotient in the agda-algebras library is 𝑨 [ 𝑩 ]/ker h β†Ύ fe.

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 _ {Ξ± Ξ² : Level}{𝑨 : Algebra Ξ± 𝑆} where
 Ο€epi : (ΞΈ : Con{Ξ±}{Ξ²} 𝑨) β†’ epi 𝑨 (𝑨 β•± ΞΈ)
 Ο€epi ΞΈ = (Ξ» a β†’ βŸͺ a ⟫) , (Ξ» _ _ β†’ refl) , cΟ€-is-epic  where
  cΟ€-is-epic : IsSurjective (Ξ» a β†’ βŸͺ a ⟫)
  cΟ€-is-epic (C , mkblk a refl ) =  Image_βˆ‹_.eq a 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 :  (wd : swelldef π“₯ Ξ²){𝑩 : Algebra Ξ² 𝑆}(h : hom 𝑨 𝑩)
  β†’      epi 𝑨 (ker[ 𝑨 β‡’ 𝑩 ] h β†Ύ wd)

 Ο€ker wd {𝑩} h = Ο€epi (kercon wd {𝑩} 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 :  {wd : swelldef π“₯ (Ξ± βŠ” suc Ξ²)}(ΞΈ : Con 𝑨)
  β†’            βˆ€ {x}{y} β†’ ∣ kercon wd {𝑨 β•± ΞΈ} (Ο€hom ΞΈ) ∣ x y β†’  ∣ ΞΈ ∣ x y

 ker-in-con ΞΈ hyp = /-≑ ΞΈ hyp

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