Skip to content

Setoid.Homomorphisms.Products

Products of Homomorphisms of Algebras

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

{-# 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

The family 𝒽 of homomorphisms inhabits the dependent type Ξ  i κž‰ I , hom 𝑨 (ℬ i). The syntax we use to represent this type is available to us because of the way -Ξ  is defined in the Type Topology library. We like this syntax because it is very close to the notation one finds in the standard type theory literature. However, we could equally well have used one of the following alternatives, which may be closer to "standard Agda" syntax:

Ξ  Ξ» i β†’ hom 𝑨 (ℬ i) or (i : I) β†’ hom 𝑨 (ℬ i) or βˆ€ i β†’ hom 𝑨 (ℬ i).

The foregoing generalizes easily to the case in which the domain is also a product of a family of algebras. That is, if we are given π’œ : I β†’ Algebra Ξ± 𝑆 and ℬ : I β†’ Algebra Ξ² 𝑆 (two families of 𝑆-algebras), and 𝒽 : Ξ  i κž‰ I , hom (π’œ i)(ℬ i) (a family of homomorphisms), then we can 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.