This is the Setoid.Homomorphisms.Kernels module of the Agda Universal Algebra Library.
{-# OPTIONS --without-K --exact-split --safe #-} open import Overture using (π ; π₯ ; Signature) module Setoid.Homomorphisms.Kernels {π : Signature π π₯} where -- Imports from Agda and the Agda Standard Library ------------------------------------------ open import Data.Product using ( _,_ ) open import Function using ( _β_ ; id ) renaming ( Func to _βΆ_ ) open import Level using ( Level ) open import Relation.Binary using ( Setoid ) open import Relation.Binary.PropositionalEquality as β‘ using () -- Imports from the Agda Universal Algebra Library ------------------------------------------ open import Overture using ( β£_β£ ; β₯_β₯ ) open import Base.Relations using ( kerRel ; kerRelOfEquiv ) open import Setoid.Functions using ( Image_β_ ) open import Setoid.Algebras {π = π} using ( Algebra ; _Μ_ ; ov ; _β£β_ ; Con ; mkcon ; _β±_ ; IsCongruence ) open import Setoid.Homomorphisms.Basic {π = π} using ( hom ; IsHom ; epi ; IsEpi ; epiβhom ) open import Setoid.Homomorphisms.Properties {π = π} using ( πΎπΉ ) private variable Ξ± Ξ² Οα΅ Οα΅ β : Level open Algebra using ( Domain ) open _βΆ_ using ( cong ) renaming ( to to _β¨$β©_ ) module _ {π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} (hh : hom π¨ π©) where open Setoid (Domain π¨) renaming ( _β_ to _ββ_ ) using ( reflexive ) open Algebra π© renaming (Domain to B ) using ( Interp ) open Setoid B renaming ( _β_ to _ββ_ ) using ( sym ; trans ; isEquivalence ) private h = _β¨$β©_ β£ hh β£
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 β₯ hh β₯ lem2 : (f Μ π©) (h β v) ββ h ((f Μ π¨) v) lem2 = sym (IsHom.compatible β₯ hh β₯) 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 β£ hh β£ 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[_β_]_ : (π¨ : Algebra Ξ± Οα΅) (π© : Algebra Ξ² Οα΅) β hom π¨ π© β Algebra _ _ ker[ π¨ β π© ] h = kerquo h
Given an algebra π¨
and a congruence ΞΈ
, the canonical projection is a map from π¨
onto π¨ β± ΞΈ
that is constructed, and proved epimorphic, as follows.
module _ {π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} (h : hom π¨ π©) where open IsCongruence Οepi : (ΞΈ : Con π¨ {β}) β epi π¨ (π¨ β± ΞΈ) Οepi ΞΈ = p , pepi where open Algebra (π¨ β± ΞΈ) using () renaming ( Domain to A/ΞΈ ) open Setoid A/ΞΈ using ( sym ; refl ) open IsHom {π¨ = (π¨ β± ΞΈ)} using ( compatible ) p : (Domain π¨) βΆ A/ΞΈ p = record { to = id ; cong = reflexive β₯ ΞΈ β₯ } pepi : IsEpi π¨ (π¨ β± ΞΈ) p pepi = record { isHom = record { compatible = sym (compatible β₯ πΎπΉ β₯) } ; 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.
open IsCongruence ker-in-con : {ΞΈ : Con π¨ {β}} β β {x}{y} β β£ kercon (Οhom ΞΈ) β£ x y β β£ ΞΈ β£ x y ker-in-con = id
β Setoid.Homomorphisms.Properties Setoid.Homomorphisms.Products β