### 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 Ξ²) π

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)
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