↑ Top


Homomorphic Images

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

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

open import Algebras.Basic

module 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 ; Ξ£ ; _Γ—_ )
open import Level          using ( Level )
open import Relation.Binary.PropositionalEquality
                           using ( _≑_ ; module ≑-Reasoning ; cong ; cong-app ; sym )
open import Relation.Unary using ( Pred ; _∈_ )

-- Imports from the Agda Universal Algebra Library ------------------------------------------
open import Overture.Preliminaries      using ( 𝑖𝑑 ; ∣_∣ ; βˆ₯_βˆ₯ ; lower∼lift ; lift∼lower )
open import Overture.Inverses           using ( Image_βˆ‹_ ; Inv ; InvIsInverseΚ³ ; eq )
open import Overture.Surjective         using ( IsSurjective )
open import Algebras.Products   {𝑆 = 𝑆} using ( ov )
open import Homomorphisms.Basic {𝑆 = 𝑆} using ( hom ; 𝓁𝒾𝒻𝓉 ; π“β„΄π“Œβ„―π“‡ )
open import Homomorphisms.Properties {𝑆 = 𝑆} using ( Lift-hom )

Images of a single 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.

module _ {Ξ± Ξ² : Level } where

 _IsHomImageOf_ : (𝑩 : Algebra Ξ² 𝑆)(𝑨 : Algebra Ξ± 𝑆) β†’ Type _
 𝑩 IsHomImageOf 𝑨 = Ξ£[ Ο† ∈ hom 𝑨 𝑩 ] IsSurjective ∣ Ο† ∣

 HomImages : Algebra Ξ± 𝑆 β†’ Type(π“ž βŠ” π“₯ βŠ” Ξ± βŠ” lsuc Ξ²)
 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.

Images of a class of 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.

module _ {Ξ± : Level} where

 IsHomImageOfClass : {𝒦 : Pred (Algebra Ξ± 𝑆)(lsuc Ξ±)} β†’ Algebra Ξ± 𝑆 β†’ Type(ov Ξ±)
 IsHomImageOfClass {𝒦 = 𝒦} 𝑩 = Ξ£[ 𝑨 ∈ Algebra Ξ± 𝑆 ] ((𝑨 ∈ 𝒦) Γ— (𝑩 IsHomImageOf 𝑨))

 HomImageOfClass : Pred (Algebra Ξ± 𝑆) (lsuc Ξ±) β†’ Type(ov Ξ±)
 HomImageOfClass 𝒦 = Ξ£[ 𝑩 ∈ Algebra Ξ± 𝑆 ] 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 _ {Ξ± Ξ² : 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


← Homomorphisms.Isomorphisms Homomorphisms.Func β†’