This is the Setoid.Homomorphisms.HomomorphicImages module of the Agda Universal Algebra Library.
{-# OPTIONS --without-K --exact-split --safe #-} open import Base.Algebras.Basic using (π ; π₯ ; Signature ) module Setoid.Homomorphisms.HomomorphicImages {π : Signature π π₯} where -- Imports from Agda and the Agda Standard Library ------------------------------------------ open import Agda.Primitive using ( _β_ ; lsuc ) renaming ( Set to Type ) open import Data.Product using ( _,_ ; Ξ£-syntax ) renaming ( _Γ_ to _β§_ ; projβ to fst ; projβ to snd ) open import Function using ( Func ; _on_ ; _β_ ; id ) open import Level using ( Level ) open import Relation.Binary using ( Setoid ; _Preserves_βΆ_ ) open import Relation.Unary using ( Pred ; _β_ ) open import Relation.Binary.PropositionalEquality as β‘ using () -- Imports from the Agda Universal Algebra Library --------------------------------------------- open import Base.Overture.Preliminaries using ( β£_β£ ; β₯_β₯ ; transport ) open import Setoid.Overture.Preliminaries using ( liftβΌlower ) open import Setoid.Overture.Inverses using ( Ran ; _range ; _preimage ; _image ; Inv ) using ( _preimageβimage ; InvIsInverseΚ³ ; Image_β_ ) open import Setoid.Overture.Surjective using ( IsSurjective ; β-IsSurjective ) open import Setoid.Algebras.Basic {π = π} using ( Algebra ; ov ; _Μ_ ; β¦_β§ ; Lift-AlgΛ‘ ) using ( Lift-Alg ; π[_] ) open import Setoid.Homomorphisms.Basic {π = π} using ( hom ; IsHom ) open import Setoid.Homomorphisms.Isomorphisms {π = π} using ( _β _ ; Lift-β ) open import Setoid.Homomorphisms.Properties {π = π} using ( Lift-homΛ‘ ; ToLiftΛ‘ ; lift-hom-lemma ) using ( πΎπΉ ; β-hom ) private variable Ξ± Οα΅ Ξ² Οα΅ : Level open Algebra
We begin with what seems, for our purposes, the most useful way to represent the class of homomorphic images of an algebra in dependent type theory.
open IsHom _IsHomImageOf_ : (π© : Algebra Ξ² Οα΅)(π¨ : Algebra Ξ± Οα΅) β Type (π β π₯ β Ξ± β Ξ² β Οα΅ β Οα΅) π© IsHomImageOf π¨ = Ξ£[ Ο β hom π¨ π© ] IsSurjective β£ Ο β£ HomImages : Algebra Ξ± Οα΅ β Type (Ξ± β Οα΅ β ov (Ξ² β Οα΅)) HomImages {Ξ² = Ξ²}{Οα΅ = Οα΅} π¨ = Ξ£[ π© β Algebra Ξ² Οα΅ ] π© IsHomImageOf π¨ IdHomImage : {π¨ : Algebra Ξ± Οα΅} β π¨ IsHomImageOf π¨ IdHomImage {Ξ± = Ξ±}{π¨ = π¨} = πΎπΉ , Ξ» {y} β Image_β_.eq y refl where open Setoid (Domain π¨) using ( refl )
These types should be self-explanatory, but just to be sure, letβs describe the Sigma type appearing in the second definition. Given an π
-algebra π¨ : Algebra Ξ± Ο
, the type HomImages π¨
denotes the class of algebras π© : Algebra Ξ² Ο
with a map Ο : β£ π¨ β£ β β£ π© β£
such that Ο
is a surjective homomorphism.
Here we show how to construct a Algebra (called ImageAlgebra
below) that is the image of given hom.
module _ {π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} where open Algebra π¨ using (Interp) renaming (Domain to A ) open Algebra π© using () renaming (Domain to B ; Interp to InterpB ) open Setoid A using ( ) renaming ( _β_ to _ββ_ ; Carrier to β£Aβ£) open Setoid B using ( reflexive ) renaming ( _β_ to _ββ_ ; refl to reflβ ) renaming ( sym to symβ ; trans to transβ ; Carrier to β£Bβ£) open Func using ( cong ) renaming (f to _β¨$β©_ ) open IsHom HomImageOf[_] : hom π¨ π© β Algebra (Ξ± β Ξ² β Οα΅) Οα΅ HomImageOf[ h ] = record { Domain = Ran β£ h β£ ; Interp = record { f = f' ; cong = cong' } } where open Setoid (β¦ π β§ (Ran β£ h β£)) using () renaming (Carrier to SRanh ; _β_ to _ββ_ ; refl to reflβ ) hhom : β {π}(x : β₯ π β₯ π β β£ h β£ range ) β (β£ h β£ β¨$β© (π Μ π¨) ((β£ h β£ preimage) β x)) ββ (π Μ π©) ((β£ h β£ image) β x) hhom {π} x = transβ (compatible β₯ h β₯) (cong InterpB (β‘.refl , (β£ h β£ preimageβimage) β x)) f' : SRanh β β£ h β£ range f' (π , x) = (π Μ π©)((β£ h β£ image)β x) -- b : the image in β£Bβ£ , (π Μ π¨)((β£ h β£ preimage) β x) -- a : the preimage in β£Aβ£ , hhom x -- p : proof that `(β£ h β£ β¨$β© a) ββ b` cong' : β {x y} β x ββ y β ((β£ h β£ image) (f' x)) ββ ((β£ h β£ image) (f' y)) cong' {(π , u)} {(.π , v)} (β‘.refl , EqA) = Goal where -- Alternative formulation of the goal: goal : (π Μ π©)(Ξ» i β ((β£ h β£ image)(u i))) ββ (π Μ π©)(Ξ» i β ((β£ h β£ image) (v i))) goal = cong InterpB (β‘.refl , EqA ) Goal : (β£ h β£ image) (f' (π , u)) ββ (β£ h β£ image) (f' (π , v)) Goal = goal -- Note: `EqA : β i β (β£ h β£ image) (u i) ββ (β£ h β£ image) (v i)`
Given a class π¦
of π
-algebras, we need a type that expresses the assertion that a given algebra is a homomorphic image of some algebra in the class, as well as a type that represents all such homomorphic images.
IsHomImageOfClass : {π¦ : Pred (Algebra Ξ± Οα΅)(lsuc Ξ±)} β Algebra Ξ± Οα΅ β Type (ov (Ξ± β Οα΅)) IsHomImageOfClass {π¦ = π¦} π© = Ξ£[ π¨ β Algebra _ _ ] ((π¨ β π¦) β§ (π© IsHomImageOf π¨)) HomImageOfClass : Pred (Algebra Ξ± Οα΅) (lsuc Ξ±) β Type (ov (Ξ± β Οα΅)) HomImageOfClass π¦ = Ξ£[ π© β Algebra _ _ ] IsHomImageOfClass {π¦ = π¦} π©
Here are some tools that have been useful (e.g., in the road to the proof of Birkhoffβs HSP theorem). The first states and proves the simple fact that the lift of an epimorphism is an epimorphism.
module _ {π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} where open Algebra π¨ using () renaming ( Domain to A ) open Algebra π© using () renaming ( Domain to B ) open Setoid B using ( sym ; trans ) renaming ( _β_ to _ββ_ ) open Func using ( cong ) renaming ( f to _β¨$β©_ ) open Level Lift-epi-is-epiΛ‘ : (h : hom π¨ π©)(βα΅ βα΅ : Level) β IsSurjective β£ h β£ β IsSurjective β£ Lift-homΛ‘ {π¨ = π¨}{π©} h βα΅ βα΅ β£ Lift-epi-is-epiΛ‘ h βα΅ βα΅ hepi {b} = Goal where open Algebra (Lift-AlgΛ‘ π© βα΅) using () renaming (Domain to lB ) open Setoid lB using () renaming ( _β_ to _βββ_ ) a : π[ π¨ ] a = Inv β£ h β£ hepi lem1 : b βββ (lift (lower b)) lem1 = liftβΌlower {π¨ = B} b lem2' : (lower b) ββ (β£ h β£ β¨$β© a) lem2' = sym (InvIsInverseΚ³ hepi) lem2 : (lift (lower b)) βββ (lift (β£ h β£ β¨$β© a)) lem2 = cong{From = B} β£ ToLiftΛ‘{π¨ = π©}{βα΅} β£ lem2' lem3 : (lift (β£ h β£ β¨$β© a)) βββ ((β£ Lift-homΛ‘ h βα΅ βα΅ β£ β¨$β© lift a)) lem3 = lift-hom-lemma h a βα΅ βα΅ Ξ· : b βββ (β£ Lift-homΛ‘ h βα΅ βα΅ β£ β¨$β© lift a) Ξ· = trans lem1 (trans lem2 lem3) Goal : Image β£ Lift-homΛ‘ h βα΅ βα΅ β£ β b Goal = Image_β_.eq (lift a) Ξ· Lift-Alg-hom-imageΛ‘ : (βα΅ βα΅ : Level) β π© IsHomImageOf π¨ β (Lift-AlgΛ‘ π© βα΅) IsHomImageOf (Lift-AlgΛ‘ π¨ βα΅) Lift-Alg-hom-imageΛ‘ βα΅ βα΅ ((Ο , Οhom) , Οepic) = Goal where lΟ : hom (Lift-AlgΛ‘ π¨ βα΅) (Lift-AlgΛ‘ π© βα΅) lΟ = Lift-homΛ‘ {π¨ = π¨}{π©} (Ο , Οhom) βα΅ βα΅ lΟepic : IsSurjective β£ lΟ β£ lΟepic = Lift-epi-is-epiΛ‘ (Ο , Οhom) βα΅ βα΅ Οepic Goal : (Lift-AlgΛ‘ π© βα΅) IsHomImageOf (Lift-AlgΛ‘ π¨ βα΅) Goal = lΟ , lΟepic module _ {π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} where open _β _ Lift-HomImage-lemma : β{Ξ³} β (Lift-Alg π¨ Ξ³ Ξ³) IsHomImageOf π© β π¨ IsHomImageOf π© Lift-HomImage-lemma {Ξ³} Ο = β-hom β£ Ο β£ (from Lift-β ) , β-IsSurjective β₯ Ο β₯ (fromIsSurjective (Lift-β {π¨ = π¨})) module _ {π¨ π¨' : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} where open _β _ HomImage-β : π¨ IsHomImageOf π¨' β π¨ β π© β π© IsHomImageOf π¨' HomImage-β Ο Aβ B = β-hom β£ Ο β£ (to Aβ B) , β-IsSurjective β₯ Ο β₯ (toIsSurjective Aβ B) HomImage-β ' : π¨ IsHomImageOf π¨' β π¨' β π© β π¨ IsHomImageOf π© HomImage-β ' Ο A'β B = (β-hom (from A'β B) β£ Ο β£) , β-IsSurjective (fromIsSurjective A'β B) β₯ Ο β₯