↑ Top

Products of Homomorphisms of Algebras

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


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

open import Overture using (π“ž ; π“₯ ; Signature)

module Setoid.Homomorphisms.Products {𝑆 : Signature π“ž π“₯} 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 )
open import Relation.Binary.PropositionalEquality as ≑ using ( _≑_ )

-- Imports from the Agda Universal Algebras Library ----------------------
open import Overture         using ( ∣_∣ ; βˆ₯_βˆ₯)
open import Setoid.Algebras {𝑆 = 𝑆}
                             using ( Algebra ; _Μ‚_ ; β¨… )
open import Setoid.Homomorphisms.Basic {𝑆 = 𝑆}
                             using ( hom ; IsHom ; 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 π“˜}{𝑨 : Algebra Ξ± ρᡃ}(ℬ : I β†’ Algebra Ξ² ρᡇ)  where
 open Algebra 𝑨      using ()        renaming ( Domain to A )
 open Algebra (β¨… ℬ)  using ()        renaming ( Domain to β¨…B )
 open _⟢_            using ( cong )  renaming ( f to _⟨$⟩_ )
 open IsHom

 β¨…-hom-co : (βˆ€(i : I) β†’ hom 𝑨 (ℬ i)) β†’ hom 𝑨 (β¨… ℬ)
 β¨…-hom-co 𝒽 = h , hhom
  where
  h : A ⟢ β¨…B
  (h ⟨$⟩ a) i = ∣ 𝒽 i ∣ ⟨$⟩ a
  cong h xy i = cong ∣ 𝒽 i ∣ xy

  hhom : IsHom 𝑨 (β¨… ℬ) h
  compatible hhom = Ξ» i β†’ compatible βˆ₯ 𝒽 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 : (π’œ : I β†’ Algebra Ξ± ρᡃ) β†’ (βˆ€ (i : I) β†’ hom (π’œ i) (ℬ i)) β†’ hom (β¨… π’œ)(β¨… ℬ)
 β¨…-hom π’œ 𝒽 = F , isHom
  where
  open Algebra (β¨… π’œ) using () renaming ( Domain to β¨…A )

  F : β¨…A ⟢ β¨…B
  (F ⟨$⟩ x) i = ∣ 𝒽 i ∣ ⟨$⟩ x i
  cong F xy i = cong ∣ 𝒽 i ∣ (xy i)

  isHom : IsHom (β¨… π’œ) (β¨… ℬ) F
  compatible isHom i = compatible βˆ₯ 𝒽 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 i = F , isHom
  where
  open Algebra (ℬ i)  using () renaming ( Domain to Bi )
  open Setoid Bi      using () renaming ( refl to reflα΅’ )

  F : β¨…B ⟢ Bi
  F ⟨$⟩ x = x i
  cong F xy = xy i

  isHom : IsHom (β¨… ℬ) (ℬ i) F
  compatible isHom {f} {a} = reflα΅’

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

← Setoid.Homomorphisms.Kernels Setoid.Homomorphisms.Noether β†’