---
layout: default
title : "Setoid.Homomorphisms.Products module (The Agda Universal Algebra Library)"
date : "2021-09-21"
author: "agda-algebras development team"
---

#### 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`{.AgdaFunction} 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`{.AgdaFunction} takes a family of homomorphisms `π’œ i β†’ ℬ i` to their
   product, `β¨… π’œ β†’ β¨… ℬ`;
+  `β¨…-proj`{.AgdaFunction} is the coordinate projection `β¨… π’œ β†’ π’œ i`.

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

<!--
```agda
{-# 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.

```agda
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.

```agda
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.

```agda
  β¨…-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`{.AgdaFunction} 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.