↑ Top

Products of Homomorphisms

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

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

open import Overture using (Signature ; 𝓞 ; 𝓥 )

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

-- Imports from Agda and the Agda Standard Library -----------------------
open import Agda.Primitive  using () renaming ( Set to Type )
open import Data.Product    using ( _,_ )
open import Level           using ( Level ;  _⊔_ ; suc )

open import Relation.Binary.PropositionalEquality using ( refl )

open import Axiom.Extensionality.Propositional renaming (Extensionality to funext)
  using ()

-- Imports from the Agda Universal Algebras Library ----------------------
open import Overture using ( ∣_∣ ; ∥_∥)

open import Base.Algebras             {𝑆 = 𝑆}  using ( Algebra ;  )
open import Base.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 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.

← Base.Homomorphisms.Kernels Base.Homomorphisms.Noether →