↑ 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 Base.Algebras.Basic using ( π“ž ; π“₯ ; Signature )

module Setoid.Homomorphisms.Products {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library --------------------------
open import Agda.Primitive    using ( _βŠ”_ ; lsuc )  renaming ( Set to Type )
open import Function.Bundles  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 Base.Overture.Preliminaries               using ( ∣_∣ ; βˆ₯_βˆ₯)
open import Setoid.Algebras.Basic       {𝑆 = 𝑆}  using ( Algebra )
open import Setoid.Algebras.Products    {𝑆 = 𝑆}  using ( β¨… )
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 Setoid A             using ()       renaming ( refl to refl₁ )
 open Algebra (β¨… ℬ)  using ()       renaming ( Domain to β¨…B )
 open _⟢_                 using ( cong )  renaming ( f to _⟨$⟩_ )
 open Algebra        using ( Domain )
 open Setoid               using ( refl )
 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 π’œ 𝒽 = {!!} -- (Ξ» x i β†’ ∣ 𝒽 i ∣ (x i)) , (Ξ» 𝑓 𝒢 β†’ Ξ» 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.


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