This is the Base.Homomorphisms.HomomorphicImages module of the Agda Universal Algebra Library.
{-# OPTIONS --without-K --exact-split --safe #-} open import Overture using ( Signature ; π ; π₯ ) module Base.Homomorphisms.HomomorphicImages {π : Signature π π₯} where -- Imports from Agda and the Agda Standard Library ------------------------------------------ open import Agda.Primitive using () renaming ( Set to Type ) open import Data.Product using ( _,_ ; Ξ£-syntax ; Ξ£ ; _Γ_ ) open import Level using ( Level ; _β_ ; suc ) open import Relation.Unary using ( Pred ; _β_ ) open import Relation.Binary.PropositionalEquality as β‘ using ( _β‘_ ; module β‘-Reasoning ) -- Imports from the Agda Universal Algebra Library ------------------------------------------ open import Overture using ( ππ ; β£_β£ ; β₯_β₯ ; lowerβΌlift ; liftβΌlower ) open import Base.Functions using ( Image_β_ ; Inv ; InvIsInverseΚ³ ; eq ; IsSurjective ) open import Base.Algebras {π = π} using ( Algebra ; Level-of-Carrier ; Lift-Alg ; ov ) open import Base.Homomorphisms.Basic {π = π} using ( hom ; ππΎπ»π ; πβ΄πβ―π ) open import Base.Homomorphisms.Properties {π = π} using ( Lift-hom )
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.
module _ {Ξ± Ξ² : Level } where _IsHomImageOf_ : (π© : Algebra Ξ² π)(π¨ : Algebra Ξ± π) β Type _ π© IsHomImageOf π¨ = Ξ£[ Ο β hom π¨ π© ] IsSurjective β£ Ο β£ HomImages : Algebra Ξ± π β Type(π β π₯ β Ξ± β suc Ξ²) HomImages π¨ = Ξ£[ π© β Algebra Ξ² π ] π© IsHomImageOf π¨
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.
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.
module _ {Ξ± : Level} where IsHomImageOfClass : {π¦ : Pred (Algebra Ξ± π)(suc Ξ±)} β Algebra Ξ± π β Type(ov Ξ±) IsHomImageOfClass {π¦ = π¦} π© = Ξ£[ π¨ β Algebra Ξ± π ] ((π¨ β π¦) Γ (π© IsHomImageOf π¨)) HomImageOfClass : Pred (Algebra Ξ± π) (suc Ξ±) β 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 _ {Ξ± Ξ² : Level} where open Level open β‘-Reasoning Lift-epi-is-epi : {π¨ : Algebra Ξ± π}(βα΅ : Level){π© : Algebra Ξ² π}(βα΅ : Level)(h : hom π¨ π©) β IsSurjective β£ h β£ β IsSurjective β£ Lift-hom βα΅ {π©} βα΅ h β£ Lift-epi-is-epi {π¨ = π¨} βα΅ {π©} βα΅ h hepi y = eq (lift a) Ξ· where lh : hom (Lift-Alg π¨ βα΅) (Lift-Alg π© βα΅) lh = Lift-hom βα΅ {π©} βα΅ h ΞΆ : Image β£ h β£ β (lower y) ΞΆ = hepi (lower y) a : β£ π¨ β£ a = Inv β£ h β£ ΞΆ Ξ½ : lift (β£ h β£ a) β‘ β£ Lift-hom βα΅ {π©} βα΅ h β£ (Level.lift a) Ξ½ = β‘.cong (Ξ» - β lift (β£ h β£ (- a))) (lowerβΌlift {Level-of-Carrier π¨}{Ξ²}) Ξ· : y β‘ β£ lh β£ (lift a) Ξ· = y β‘β¨ (β‘.cong-app liftβΌlower) y β© lift (lower y) β‘β¨ β‘.cong lift (β‘.sym (InvIsInverseΚ³ ΞΆ)) β© lift (β£ h β£ a) β‘β¨ Ξ½ β© β£ lh β£ (lift a) β Lift-Alg-hom-image : {π¨ : Algebra Ξ± π}(βα΅ : Level){π© : Algebra Ξ² π}(βα΅ : 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 _ Goal = lΟ , lΟepic