### 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
```

#### Definition

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