Skip to content

Setoid.Homomorphisms.Products

Products of Homomorphisms of Algebras

This is the Setoid.Homomorphisms.Products module of the Agda Universal Algebra Library.

This module defines some of the homomorphisms associated with a product.

  • β¨…-hom-co is the induced map into a product: a family of homomorphisms out of a single algebra 𝑨, one for each index, assembles into a single homomorphism from 𝑨 to the product;
  • β¨…-hom takes a family of homomorphisms π’œ i β†’ ℬ i to their product, β¨… π’œ β†’ β¨… ℬ;
  • β¨…-proj is the coordinate projection β¨… π’œ β†’ π’œ i.

All three are defined coordinatewise, and their compatibility proofs are inherited coordinatewise from the factors, because that is how β¨… of Setoid.Algebras.Products interprets the operations in the first place.1

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Homomorphisms.Products where

-- Imports from Agda and the Agda Standard Library --------------------------
open import Agda.Primitive              using () renaming ( Set to Type )
open import Function                    using () renaming ( Func to _⟢_ )
open import Data.Product                using ( _,_ )
open import Level                       using ( Level )
open import Relation.Binary             using ( Setoid )

-- Imports from the Agda Universal Algebras Library ----------------------
open import Overture                    using ( proj₁ ; projβ‚‚ ; π“ž ; π“₯ ; Signature)
open import Setoid.Algebras             using ( Algebra ; β¨… ; 𝔻[_] )
open import Setoid.Homomorphisms.Basic  using ( hom ; IsHom )

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

private variable Ξ± ρ Ξ² ρᡇ π“˜ : Level

Suppose we have an algebra 𝑨, a type I : Type π“˜, and a family ℬ : I β†’ Algebra Ξ² 𝑆 of algebras. We sometimes refer to the inhabitants of I as indices, and call ℬ an indexed family of algebras.

If in addition we have a family 𝒽 : (i : I) β†’ hom 𝑨 (ℬ i) of homomorphisms, then we can construct a homomorphism from 𝑨 to the product β¨… ℬ in the natural way.

module _ {𝑆 : Signature π“ž π“₯} {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ } {I : Type π“˜} (ℬ : I β†’ Algebra Ξ² ρᡇ)  where

  β¨…-hom-co : (βˆ€(i : I) β†’ hom 𝑨 (ℬ i)) β†’ hom 𝑨 (β¨… ℬ)
  β¨…-hom-co 𝒽 = h , hhom
    where
    h : 𝔻[ 𝑨 ] ⟢ 𝔻[ β¨… ℬ ]
    h ⟨$⟩ a = Ξ» i β†’ 𝒽 i .proj₁ ⟨$⟩ a
    h .cong xy = Ξ» i β†’ 𝒽 i .proj₁ .cong xy

    hhom : IsHom 𝑨 (β¨… ℬ) h
    hhom .compatible = Ξ» i β†’ 𝒽 i .projβ‚‚ .compatible

If we are given π’œ : I β†’ Algebra Ξ± 𝑆 and ℬ : I β†’ Algebra Ξ² 𝑆 (two families of 𝑆-algebras), then a family 𝒽 of homomorphisms inhabits the dependent type βˆ€ (i : I) β†’ hom (π’œ i) (ℬ i), from which we construct a homomorphism from β¨… π’œ to β¨… ℬ in the following natural way.

module _  {𝑆 : Signature π“ž π“₯} {I : Type π“˜} (π’œ : I β†’ Algebra {𝑆 = 𝑆} Ξ± ρ) where
  β¨…-hom : (ℬ : I β†’ Algebra Ξ² ρᡇ) β†’ (βˆ€ (i : I) β†’ hom (π’œ i) (ℬ i)) β†’ hom (β¨… π’œ)(β¨… ℬ)
  β¨…-hom ℬ 𝒽 = F , isHom
    where

    F : 𝔻[ β¨… π’œ ] ⟢ 𝔻[ β¨… ℬ ]
    F ⟨$⟩ x = Ξ» i β†’ 𝒽 i .proj₁ ⟨$⟩ x i
    F .cong xy = Ξ» i β†’ 𝒽 i .proj₁ .cong (xy i)

    isHom : IsHom (β¨… π’œ) (β¨… ℬ) F
    isHom .compatible = Ξ» i β†’ 𝒽 i .projβ‚‚ .compatible

Projection out of products

The projection of a product algebra onto its i-th factor is a homomorphism.

  β¨…-proj : (i : I) β†’ hom (β¨… π’œ) (π’œ i)
  β¨…-proj i = F , isHom
    where
    F : 𝔻[ β¨… π’œ ] ⟢ 𝔻[ π’œ i ]
    F ⟨$⟩ x = x i
    F .cong xy = xy i

    isHom : IsHom (β¨… π’œ) (π’œ i) F
    isHom .compatible = Setoid.refl 𝔻[ π’œ i ]

We could prove a more general result involving projections onto multiple factors, but so far the single-factor result has sufficed.

  1. β¨…-hom-co does real work later: the proof of Birkhoff's theorem in Setoid.Varieties.HSP uses it to build the homomorphism homβ„­ from the term algebra into the product β„­ that the whole argument turns on. ↩