Agda UALib ↑

Product Algebras

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

Notice that we begin this module by assuming a signature 𝑆 : Signature π“ž π“₯ which is then present and available throughout the module.


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

open import Algebras.Signatures using (Signature; π“ž; π“₯)

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

open import Algebras.Algebras hiding (π“ž; π“₯) public

From now on, the modules of the UALib will assume a fixed signature 𝑆 : Signature π“ž π“₯. Notice that we have to import the Signature type from Algebras.Signatures before the module line so that we may declare the signature 𝑆 as a parameter of the Algebras.Products module.

Recall the informal definition of a product of 𝑆-algebras. Given a type I : π“˜ Μ‡ and a family π’œ : I β†’ Algebra 𝓀 𝑆, the product β¨… π’œ is the algebra whose domain is the Cartesian product Ξ  𝑖 κž‰ I , ∣ π’œ 𝑖 ∣ of the domains of the algebras in π’œ, and whose operations are defined as follows: if 𝑓 is a J-ary operation symbol and if π‘Ž : Ξ  𝑖 κž‰ I , J β†’ π’œ 𝑖 is an I-tuple of J-tuples such that π‘Ž 𝑖 is a J-tuple of elements of π’œ 𝑖 (for each 𝑖), then (𝑓 Μ‚ β¨… π’œ) π‘Ž := (i : I) β†’ (𝑓 Μ‚ π’œ i)(π‘Ž i).

In the UALib a product of 𝑆-algebras is represented by the following type.


module _ {𝓀 π“˜ : Universe}{I : π“˜ Μ‡ } where

 β¨… : (π’œ : I β†’ Algebra 𝓀 𝑆 ) β†’ Algebra (π“˜ βŠ” 𝓀) 𝑆

 β¨… π’œ = (Ξ  i κž‰ I , ∣ π’œ i ∣) ,            -- domain of the product algebra
       Ξ» 𝑓 π‘Ž i β†’ (𝑓 Μ‚ π’œ i) Ξ» x β†’ π‘Ž x i   -- basic operations of the product algebra

(Alternative acceptable notation for the domain of the product is βˆ€ i β†’ ∣ π’œ i ∣.)

The type just defined is the one that will be used throughout the UALib whenever the product of an indexed collection of algebras (of type Algebra) is required. However, for the sake of completeness, here is how one could define a type representing the product of algebras inhabiting the record type algebra.


 open algebra

 β¨…' : (π’œ : I β†’ algebra 𝓀 𝑆) β†’ algebra (π“˜ βŠ” 𝓀) 𝑆

 β¨…' π’œ = record { univ = βˆ€ i β†’ univ (π’œ i) ;                 -- domain
                 op = Ξ» 𝑓 π‘Ž i β†’ (op (π’œ i)) 𝑓 Ξ» x β†’ π‘Ž x i } -- basic operations

Notation. Given a signature 𝑆 : Signature π“ž π“₯, the type Algebra 𝓀 𝑆 has type π“ž βŠ” π“₯ βŠ” 𝓀 ⁺ Μ‡. Such types occur so often in the UALib that we define the following shorthand for their universes.


ov : Universe β†’ Universe
ov 𝓀 = π“ž βŠ” π“₯ βŠ” 𝓀 ⁺

Products of classes of algebras

An arbitrary class 𝒦 of algebras is represented as a predicate over the type Algebra 𝓀 𝑆, for some universe level 𝓀 and signature 𝑆. That is, 𝒦 : Pred (Algebra 𝓀 𝑆) 𝓦, for some type 𝓦. Later we will formally state and prove that the product of all subalgebras of algebras in 𝒦 belongs to the class SP(𝒦) of subalgebras of products of algebras in 𝒦. That is, β¨… S(𝒦) ∈ SP(𝒦 ). This turns out to be a nontrivial exercise.

To begin, we need to define types that represent products over arbitrary (nonindexed) families such as 𝒦 or S(𝒦). Observe that Ξ  𝒦 is certainly not what we want. For recall that Pred (Algebra 𝓀 𝑆) 𝓦 is just an alias for the function type Algebra 𝓀 𝑆 β†’ 𝓦 Μ‡, and the semantics of the latter takes 𝒦 𝑨 (and 𝑨 ∈ 𝒦) to mean that 𝑨 belongs to the class 𝒦. Thus, by definition,

Ξ  𝒦 = Ξ  𝑨 κž‰ (Algebra 𝓀 𝑆) , 𝒦 𝑨 Β  Β  = Β  Β  βˆ€ (𝑨 : Algebra 𝓀 𝑆) β†’ 𝑨 ∈ 𝒦,

which asserts that every inhabitant of the type Algebra 𝓀 𝑆 belongs to 𝒦. Evidently this is not the product algebra that we seek.

What we need is a type that serves to index the class 𝒦, and a function 𝔄 that maps an index to the inhabitant of 𝒦 at that index. But 𝒦 is a predicate (of type (Algebra 𝓀 𝑆) β†’ 𝓦 Μ‡) and the type Algebra 𝓀 𝑆 seems rather nebulous in that there is no natural indexing class with which to β€œenumerate” all inhabitants of Algebra 𝓀 𝑆 belonging to 𝒦.1

The solution is to essentially take 𝒦 itself to be the indexing type, at least heuristically that is how one can view the type β„‘ that we now define.2


module class-products {𝓀 : Universe} (𝒦 : Pred (Algebra 𝓀 𝑆)(ov 𝓀)) where

 β„‘ : ov 𝓀 Μ‡
 β„‘ = Ξ£ 𝑨 κž‰ (Algebra 𝓀 𝑆) , (𝑨 ∈ 𝒦)

Taking the product over the index type β„‘ requires a function that maps an index i : β„‘ to the corresponding algebra. Each i : β„‘ is a pair, (𝑨 , p), where 𝑨 is an algebra and p is a proof that 𝑨 belongs to 𝒦, so the function mapping an index to the corresponding algebra is simply the first projection.


 𝔄 : β„‘ β†’ Algebra 𝓀 𝑆
 𝔄 i = ∣ i ∣

Finally, we define class-product which represents the product of all members of 𝒦.


 class-product : Algebra (ov 𝓀) 𝑆
 class-product = β¨… 𝔄

If p : 𝑨 ∈ 𝒦, we view the pair (𝑨 , p) ∈ β„‘ as an index over the class, so we can think of 𝔄 (𝑨 , p) (which is simply 𝑨) as the projection of the product β¨… 𝔄 onto the (𝑨 , p)-th component.

1 If you haven’t seen this before, give it some thought and see if the correct type comes to you organically.

2 Unicode Hints. Some of our types are denoted with with Gothic (β€œmathfrak”) symbols. To produce them in agda2-mode, type \Mf followed by a letter. For example, \MfI ↝ β„‘.

← Algebras.Algebras Algebras.Congruences β†’