↑ Top


Homomorphic images of setoid algebras

This is the Homomorphisms.Func.HomomorphicImages module of the Agda Universal Algebra Library.

{-# OPTIONS --without-K --exact-split --safe #-}

open import Algebras.Basic using (π“ž ; π“₯ ; Signature )

module Homomorphisms.Func.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 Overture.Preliminaries                using ( ∣_∣ ; βˆ₯_βˆ₯ ; transport )
open import Overture.Func.Preliminaries           using ( lift∼lower )
open import Overture.Func.Inverses                using ( Ran ; _range ; _preimage ; _image ; Inv
                                                        ; _preimageβ‰ˆimage ; InvIsInverseΚ³ ; Image_βˆ‹_ )
open import Overture.Func.Surjective              using ( IsSurjective ; ∘-IsSurjective )
open import Algebras.Func.Basic           {𝑆 = 𝑆} using ( SetoidAlgebra ; ov ; _Μ‚_ ; ⟦_⟧ ; Lift-AlgΛ‘
                                                        ; Lift-Alg ; π•Œ[_] )
open import Homomorphisms.Func.Basic      {𝑆 = 𝑆} using ( hom ; IsHom )
open import Homomorphisms.Func.Isomorphisms {𝑆 = 𝑆} using ( _β‰…_ ; Lift-β‰… )
open import Homomorphisms.Func.Properties {𝑆 = 𝑆} using ( Lift-homΛ‘ ; ToLiftΛ‘ ; lift-hom-lemma ; 𝒾𝒹 ; ∘-hom )

private variable
 Ξ± ρᡃ Ξ² ρᡇ : Level

open SetoidAlgebra

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_ : (𝑩 : SetoidAlgebra Ξ² ρᡇ)(𝑨 : SetoidAlgebra Ξ± ρᡃ) β†’ Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” Ξ² βŠ” ρᡃ βŠ” ρᡇ)
𝑩 IsHomImageOf 𝑨 = Ξ£[ Ο† ∈ hom 𝑨 𝑩 ] IsSurjective ∣ Ο† ∣

HomImages : SetoidAlgebra Ξ± ρᡃ β†’ Type (Ξ± βŠ” ρᡃ βŠ” ov (Ξ² βŠ” ρᡇ))
HomImages {Ξ² = Ξ²}{ρᡇ = ρᡇ} 𝑨 = Ξ£[ 𝑩 ∈ SetoidAlgebra Ξ² ρᡇ ] 𝑩 IsHomImageOf 𝑨

IdHomImage : {𝑨 : SetoidAlgebra Ξ± ρᡃ} β†’ 𝑨 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 𝑨 : SetoidAlgebra Ξ± ρ, the type HomImages 𝑨 denotes the class of algebras 𝑩 : SetoidAlgebra Ξ² ρ with a map Ο† : ∣ 𝑨 ∣ β†’ ∣ 𝑩 ∣ such that Ο† is a surjective homomorphism.

The image algebra of a hom

Here we show how to construct a SetoidAlgebra (called ImageAlgebra below) that is the image of given hom.

module _ {𝑨 : SetoidAlgebra Ξ± ρᡃ}{𝑩 : SetoidAlgebra Ξ² ρᡇ} where
 open SetoidAlgebra 𝑨 using (Interp) renaming (Domain to A )
 open SetoidAlgebra 𝑩 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β‚‚ ; sym to symβ‚‚ ; trans to transβ‚‚ ; Carrier to ∣B∣)

 open Func using ( cong ) renaming (f to _⟨$⟩_ )
 open IsHom

 HomImageOf[_] : hom 𝑨 𝑩 β†’ SetoidAlgebra (Ξ± βŠ” Ξ² βŠ” ρᡇ) ρᡇ
 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)`

Homomorphic images of classes of setoid algebras

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 (SetoidAlgebra Ξ± ρᡃ)(lsuc Ξ±)} β†’ SetoidAlgebra Ξ± ρᡃ β†’ Type (ov (Ξ± βŠ” ρᡃ))
IsHomImageOfClass {𝒦 = 𝒦} 𝑩 = Ξ£[ 𝑨 ∈ SetoidAlgebra _ _ ] ((𝑨 ∈ 𝒦) ∧ (𝑩 IsHomImageOf 𝑨))

HomImageOfClass : Pred (SetoidAlgebra Ξ± ρᡃ) (lsuc Ξ±) β†’ Type (ov (Ξ± βŠ” ρᡃ))
HomImageOfClass 𝒦 = Ξ£[ 𝑩 ∈ SetoidAlgebra _ _ ] IsHomImageOfClass {𝒦 = 𝒦} 𝑩

Lifting tools

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 _ {𝑨 : SetoidAlgebra Ξ± ρᡃ}{𝑩 : SetoidAlgebra Ξ² ρᡇ} where

 open SetoidAlgebra 𝑨 using ()              renaming ( Domain to A )
 open SetoidAlgebra 𝑩 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 SetoidAlgebra (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 _ {𝑨 : SetoidAlgebra Ξ± ρᡃ}{𝑩 : SetoidAlgebra Ξ² ρᡇ} where
 open _β‰…_
 Lift-HomImage-lemma : βˆ€{Ξ³} β†’ (Lift-Alg 𝑨 Ξ³ Ξ³) IsHomImageOf 𝑩 β†’ 𝑨 IsHomImageOf 𝑩
 Lift-HomImage-lemma {Ξ³} Ο† = ∘-hom ∣ Ο† ∣ (from Lift-β‰…) ,
                             ∘-IsSurjective βˆ₯ Ο† βˆ₯ (fromIsSurjective (Lift-β‰…{𝑨 = 𝑨}))

module _ {𝑨 𝑨' : SetoidAlgebra Ξ± ρᡃ}{𝑩 : SetoidAlgebra Ξ² ρᡇ} 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) βˆ₯ Ο† βˆ₯


← Homomorphisms.Func.Isomorphisms Terms β†’