Skip to content

Setoid.Algebras.Products

Products of Setoid Algebras

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

The product of an indexed family of algebras is formed coordinatewise: its carrier is the dependent function type over the index, its equality is pointwise, and each operation symbol is interpreted by applying the corresponding operation in every factor.

This module defines that product, β¨…; the machinery for taking the product of a class of algebras rather than of an indexed family; and the one nontrivial fact about products proved here, which is the following:

The coordinate projections out of a product are surjective when the index type has decidable equality and every factor is nonempty.

Products are one of the three closure operations H, S, P whose composite V defines a variety, so this module is used throughout Setoid.Varieties.Closure and in the proof of Birkhoff's theorem in Setoid.Varieties.HSP.

Homomorphisms into and out of a product are in Setoid.Homomorphisms.Products, and β¨…β‰… of Setoid.Homomorphisms.Isomorphisms shows that products of isomorphic families are isomorphic.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Algebras.Products where

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Agda.Primitive    using () renaming ( Set to Type )
open import Data.Product      using ( _,_ ; Ξ£-syntax ; proj₁ )
open import Function          using ( flip ; Func )
open import Level             using( _βŠ”_ ; Level )
open import Relation.Binary   using ( Setoid ;  IsEquivalence ; Decidable )
open import Relation.Binary.PropositionalEquality  using ( refl ; _≑_ )
open import Relation.Unary    using ( Pred ; _∈_ )

open Func           using ( cong ) renaming ( to to _⟨$⟩_ )
open Setoid         using ( Carrier ; _β‰ˆ_ ) renaming ( isEquivalence to isEqv )
open IsEquivalence  using () renaming ( refl to reflE ; sym to symE ; trans to transE )


-- Imports from agda-algebras -----------------------------------------------------
open import Overture               using ( proj ; projIsOnto ; π“ž ; π“₯ ; Signature ; 𝑆 )
                                   renaming ( IsSurjective to onto )

open import Setoid.Algebras.Basic  using ( Algebra ; _^_ ; ov ; 𝔻[_] ; π•Œ[_])

private variable α ρ ι : Level

open Algebra

β¨… π’œ is the product of the family π’œ : I β†’ Algebra Ξ± ρ. Its carrier is the dependent product βˆ€ i β†’ π•Œ[ π’œ i ] of the carriers of the factors; two elements are equal exactly when they agree in every coordinate; and the interpretation of an operation symbol f is the tuple of interpretations of f in the factors, (f ^ β¨… π’œ) a i = (f ^ π’œ i) (flip a i).

The types involved in the expression (f ^ β¨… π’œ) a i = (f ^ π’œ i) (flip a i) are the following:

I : Type ΞΉ
π’œ : I β†’ Algebra Ξ± ρ
a : ArityOf 𝑆 f β†’ (i : I) β†’ π•Œ[ π’œ i ]
f : OperationSymbolsOf 𝑆

The effect of flip a i is to partially apply a to its second argument, i, which results in a map from ArityOf 𝑆 f to π•Œ[ π’œ i ] and is exactly the right shaped argument "tuple" to pass to f ^ π’œ i.

Reflexivity, symmetry and transitivity are inherited coordinatewise, and so is the congruence proof for Interp.

β¨… : {I : Type ΞΉ }(π’œ : I β†’ Algebra {𝑆 = 𝑆} Ξ± ρ) β†’ Algebra {𝑆 = 𝑆} (Ξ± βŠ” ΞΉ) (ρ βŠ” ΞΉ)

Domain (β¨… π’œ) =
  record  { Carrier = βˆ€ i β†’ π•Œ[ π’œ i ]
          ; _β‰ˆ_ = Ξ» a b β†’ βˆ€ i β†’ 𝔻[ π’œ i ] ._β‰ˆ_ (a i) (b i)
          ; isEquivalence =
             record  { refl   = Ξ» i      β†’ reflE   (isEqv 𝔻[ π’œ i ])
                     ; sym    = Ξ» x i    β†’ symE    (isEqv 𝔻[ π’œ i ])(x i)
                     ; trans  = Ξ» x y i  β†’ transE  (isEqv 𝔻[ π’œ i ])(x i)(y i)
                     }
          }

Interp (β¨… π’œ) ⟨$⟩ (f , a) = Ξ» i β†’ (f ^ π’œ i) (flip a i)
cong (Interp (β¨… π’œ)) (refl , f=g) = Ξ» i β†’ cong  (Interp (π’œ i)) (refl , flip f=g i)

Note that both levels of the resulting algebra absorb the level ΞΉ of the index type, since the carrier is a function out of I and the equality is an I-indexed conjunction. A product therefore sits at the join of its factors' levels with the level of its index. Correspondingly, the operator P of Setoid.Varieties.Closure, defining the class of products of a class, states membership up to isomorphism, 𝑩 β‰… β¨… π’œ, which leaves 𝑩 with its own pair of levels.

Products of classes of Algebras

A class of algebras is given as a predicate 𝒦 : Pred (Algebra Ξ± ρ) _, not as an indexed family, so β¨… cannot be applied to it directly; and the dependent product over the predicate is not what we want either, since βˆ€ 𝑨 β†’ 𝑨 ∈ 𝒦 asserts that every algebra belongs to 𝒦.

The remedy is to take the class itself as the index:

  • β„‘ is the type of pairs (𝑨 , p) with p : 𝑨 ∈ 𝒦,
  • 𝔄 sends such a pair to its first component, and
  • class-product is β¨… 𝔄, the product of all the members of 𝒦.

Given a proof, p : 𝑨 ∈ 𝒦, that 𝑨 belongs to 𝒦, we view the pair (𝑨 , p) ∈ β„‘ as an index over the class, and 𝔄 (𝑨 , p) (which is simply 𝑨) as the projection of the product β¨… 𝔄 onto the (𝑨 , p)-th component.

module _ {𝑆 : Signature π“ž π“₯} {𝒦 : Pred (Algebra {𝑆 = 𝑆} Ξ± ρ) (ov {𝑆 = 𝑆} Ξ±)} where

  β„‘ : Type (ov {𝑆 = 𝑆} (Ξ± βŠ” ρ))
  β„‘ = Ξ£[ 𝑨 ∈ (Algebra {𝑆 = 𝑆} Ξ± ρ) ] 𝑨 ∈ 𝒦

  𝔄 : β„‘ β†’ Algebra {𝑆 = 𝑆} Ξ± ρ
  𝔄 (𝑨 , _) = 𝑨

  class-product : Algebra (ov {𝑆 = 𝑆} (Ξ± βŠ” ρ)) (ov {𝑆 = 𝑆} (Ξ± βŠ” ρ))
  class-product = β¨… 𝔄

One subtlety of indexing by proofs rather than by algebras is that an algebra carrying two membership proofs contributes two identical factors; the result is a product of members of 𝒦 regardless. A variant that indexes by an environment as well appears as ℑ⁺, 𝔄⁺ and β„­ in Setoid.Varieties.HSP.

Surjectivity of coordinate projections

Suppose I is an index type and π’œ : I β†’ Algebra Ξ± ρ is an indexed collection of algebras. Let β¨… π’œ be the product algebra defined in the first section of this module. Given i : I, consider the projection of β¨… π’œ onto the i-th coordinate.

This projection ought to be a surjective map from β¨… π’œ onto π’œ i, but this is not so if I is an arbitrary type. Indeed, we need an equality on I, the equality must be decidable, and each factor of the product must be nonempty.

In the Setoid.Functions.Surjective module we showed how to define a decidable index type in Agda. Here we use this to prove that the projection of a product of algebras over such an index type is surjective.

module _
  {I   : Type ΞΉ}                   -- index type
  {_β‰Ÿ_ : Decidable{A = I} _≑_}     -- with decidable equality
  {π’œ   : I β†’ Algebra {𝑆 = 𝑆} Ξ± ρ}  -- indexed collection of algebras
  {π’œI  : βˆ€ i β†’ π•Œ[ π’œ i ] }         -- each of which is nonempty
  where

  ProjAlgIsOnto : βˆ€{i} β†’ Ξ£[ h ∈ (π•Œ[ β¨… π’œ ] β†’ π•Œ[ π’œ i ]) ] onto h
  ProjAlgIsOnto {i} = (proj _β‰Ÿ_ π’œI i) , projIsOnto _β‰Ÿ_ π’œI