Setoid.Homomorphisms.Kernels

Kernels of Homomorphisms

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

The kernel of a homomorphism h : hom 𝑨 𝑩 is the binary relation on the carrier of 𝑨 that relates a₀ and a₁ when h a₀ and h a₁ are equal in 𝑩.

It is an equivalence relation because it is the pullback of one along h, which is kerRelOfEquiv of Overture.Relations; what this module adds is that it is also compatible with the basic operations, hence a congruence, so that the quotient by the kernel is again an algebra.

HomKerComp is the compatibility proof, kercon is the congruence, and kerquo, also written ker[ 𝑨 ⇒ 𝑩 ] h, is the quotient.

This module also supplies the homomorphisms that go with a quotient:

• πepi is the canonical projection of 𝑨 onto 𝑨 ╱ θ, for any congruence θ, presented as an epimorphism;
• πhom is its homomorphism reduct;
• πker is the special case that projects onto a kernel quotient;
• ker-in-con says the kernel of πhom θ is contained in θ.

Together with the congruences of Setoid.Congruences, these are the components with which the first homomorphism theorem of Setoid.Homomorphisms.Noether is stated.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Homomorphisms.Kernels where

-- Imports from Agda and the Agda Standard Library ------------------------------------------
open  import Data.Product                           using ( _,_ ;  proj₁ ; proj₂ )
open  import Function   renaming ( Func to _⟶_ )    using ( _∘_ ; id )
open  import Level                                  using ( Level )
open  import Relation.Binary                        using ( Setoid )
open  import Relation.Binary.PropositionalEquality  using (refl)

-- Imports from the Agda Universal Algebra Library ------------------------------------------
open  import Overture                    using ( kerRel ; kerRelOfEquiv ; 𝓞 ; 𝓥 ; Signature)
open  import Setoid.Functions            using ( Image_∋_ )
open  import Setoid.Algebras             using ( Algebra ; _^_ ; 𝔻[_] )
open  import Setoid.Congruences          using ( _∣≈_ ; Con ; mkcon ; _╱_ ; IsCongruence )
open  import Setoid.Homomorphisms.Basic  using ( hom ; IsHom ; epi ; IsEpi ; epi→hom ; 𝒾𝒹 )

private variable  α β ρᵃ ρᵇ ℓ : Level

open _⟶_ using ( cong ) renaming ( to to _⟨$⟩_ )

module _ {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra β ρᵇ} ((hmap , hhom) : hom 𝑨 𝑩) where
  open Algebra 𝑩   using ( Interp ) renaming ( Domain to B )
  open Setoid B    using ( _≈_ ; sym ; trans ; isEquivalence )
  private h = _⟨$⟩_ hmap

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 hhom

    lem2 : (f ^ 𝑩) (h ∘ v) ≈ h ((f ^ 𝑨) v)
    lem2 = sym (IsHom.compatible hhom)

    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 hmap 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[_⇒_]_ :  {𝑆 : Signature 𝓞 𝓥} (𝑨 : 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 _ {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ}{𝑩 : Algebra β ρᵇ} (h : hom 𝑨 𝑩) where
  open IsCongruence

  πepi : (θ : Con 𝑨 ℓ) → epi 𝑨 (𝑨 ╱ θ)
  πepi θ = p , pepi
    where

    open Setoid 𝔻[ 𝑨 ╱ θ ]    using () renaming ( sym to ≈sym ; refl to ≈refl )
    open IsHom {𝑨 = (𝑨 ╱ θ)}  using ( compatible )
    open IsEpi

    p : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑨 ╱ θ ]
    p ⟨$⟩ x = x
    p .cong = reflexive (θ .proj₂)

    pepi : IsEpi 𝑨 (𝑨 ╱ θ) p
    pepi .isHom .compatible = ≈sym (𝒾𝒹 .proj₂ .compatible)
    pepi .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.

  ker-in-con : {θ : Con 𝑨 ℓ} → ∀ {x}{y} → kercon (πhom θ) .proj₁ x y →  θ .proj₁ x y
  ker-in-con = id