 Products of Homomorphisms

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

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

open import Algebras.Basic

module Homomorphisms.Products {𝑆 : Signature 𝓞 𝓥} where

-- Imports from Agda and the Agda Standard Library --------------------------
open import Agda.Primitive using ( _⊔_ ; lsuc ) renaming ( Set to Type )
open import Axiom.Extensionality.Propositional
using () renaming (Extensionality to funext)
open import Data.Product   using ( _,_ )
open import Level          using ( Level )
open import Relation.Binary.PropositionalEquality using ( refl )

-- Imports from the Agda Universal Algebras Library ----------------------
open import Overture.Preliminaries using ( ∣_∣ ; ∥_∥)
open import Algebras.Products    {𝑆 = 𝑆} using (  )
open import Homomorphisms.Basic  {𝑆 = 𝑆} using ( hom ; epi )

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 _ {I : Type 𝓘}( : I  Algebra β 𝑆) where

⨅-hom-co : funext 𝓘 β  {α : Level}(𝑨 : Algebra α 𝑆)  (∀(i : I)  hom 𝑨 ( i))  hom 𝑨 ( )
⨅-hom-co fe 𝑨 𝒽 =  a i   𝒽 i  a) ,  𝑓 𝒶  fe λ i   𝒽 i  𝑓 𝒶)

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.

⨅-hom : funext 𝓘 β  {α : Level}(𝒜 : I  Algebra α 𝑆)  (∀ (i : I)  hom (𝒜 i) ( i))  hom ( 𝒜)( )
⨅-hom fe 𝒜 𝒽 =  x i   𝒽 i  (x i)) ,  𝑓 𝒶  fe λ i   𝒽 i  𝑓  x  𝒶 x i))

Projection out of products

Later we will need a proof of the fact that projecting out of a product algebra onto one of its factors is a homomorphism.

⨅-projection-hom : (i : I)  hom ( ) ( i)
⨅-projection-hom = λ x   z  z x) , λ _ _  refl

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