↑ Top

Kernels of Homomorphisms

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

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

open import Algebras.Basic

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

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Agda.Primitive using ( _βŠ”_ ; lsuc )
open import Data.Product   using ( _,_ )
open import Function.Base  using ( _∘_ )
open import Level          using ( Level )
open import Relation.Binary.PropositionalEquality
                           using ( _≑_ ; module ≑-Reasoning ; refl )

-- -- Imports from the Agda Universal Algebras Library --------------------------------
open import Overture.Preliminaries       using ( ∣_∣ ; βˆ₯_βˆ₯ ; _⁻¹ )
open import Overture.Inverses            using ( Image_βˆ‹_ )
open import Overture.Surjective          using ( IsSurjective )
open import Equality.Welldefined         using ( swelldef )
open import Relations.Discrete           using ( ker )
open import Relations.Quotients          using ( ker-IsEquivalence ; βŸͺ_⟫ ; mkblk )
open import Algebras.Congruences {𝑆 = 𝑆} using ( Con ; mkcon ; _β•±_ ; IsCongruence ; /-≑ )
open import Homomorphisms.Basic  {𝑆 = 𝑆} using ( hom ; epi ; epiβ†’hom )

private variable Ξ± Ξ² : Level

Kernels of homomorphisms

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 (Ξ± βŠ” lsuc Ξ²) 𝑆
 kerquo wd {𝑩} h = 𝑨 β•± (kercon wd {𝑩} h)

ker[_β‡’_]_β†Ύ_ : (𝑨 : Algebra Ξ± 𝑆)(𝑩 : Algebra Ξ² 𝑆) β†’ hom 𝑨 𝑩 β†’ swelldef π“₯ Ξ² β†’ Algebra (Ξ± βŠ” lsuc Ξ²) 𝑆
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 π“₯ (Ξ± βŠ” lsuc Ξ²)}(ΞΈ : Con 𝑨)
  β†’           βˆ€ {x}{y} β†’ ∣ kercon wd {𝑨 β•± ΞΈ} (Ο€hom ΞΈ) ∣ x y β†’  ∣ ΞΈ ∣ x y

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

← Homomorphisms.Properties Homomorphisms.Products β†’