↑ Top

Products of Algebras and Product Algebras

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

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

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

module Base.Algebras.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 ( _,_ ; Ξ£ ; Ξ£-syntax )
open import Level           using ( Level ; _βŠ”_ ; suc )
open import Relation.Unary  using ( Pred ; _βŠ†_ ; _∈_ )

-- Imports from agda-algebras ---------------------------------------------------
open import Overture                     using (_⁻¹; 𝑖𝑑; ∣_∣; βˆ₯_βˆ₯)
open import Base.Algebras.Basic {𝑆 = 𝑆}  using ( Algebra ; _Μ‚_ ; algebra )

private variable Ξ± Ξ² ρ π“˜ : Level

From now on, the modules of the agda-algebras library will assume a fixed signature 𝑆 : Signature π“ž π“₯.

Recall the informal definition of a product of 𝑆-algebras. Given a type I : Type π“˜ 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 agda-algebras library a product of 𝑆-algebras is represented by the following type.

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

β¨… {I = I} π’œ =  ( βˆ€ (i : I) β†’ ∣ π’œ i ∣ ) ,        -- domain of the product algebra
                Ξ» 𝑓 π‘Ž i β†’ (𝑓 Μ‚ π’œ i) Ξ» x β†’ π‘Ž x i  -- basic operations of the product algebra

The type just defined is the one that will be used throughout the agda-algebras library 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 : Type π“˜ }(π’œ : I β†’ algebra Ξ± 𝑆) β†’ algebra (π“˜ βŠ” Ξ±) 𝑆
β¨…' {I} π’œ = record  { carrier = βˆ€ i β†’ carrier (π’œ i)                         -- domain
                    ; opsymbol = Ξ» 𝑓 π‘Ž i β†’ (opsymbol (π’œ i)) 𝑓 Ξ» x β†’ π‘Ž x i }  -- basic operations

Notation. Given a signature 𝑆 : Signature π“ž π“₯, the type Algebra Ξ± 𝑆 has type Type(π“ž βŠ” π“₯ βŠ” lsuc Ξ±). Such types occur so often in the agda-algebras library that we define the following shorthand for their universes.

ov : Level β†’ Level
ov Ξ± = π“ž βŠ” π“₯ βŠ” suc Ξ±

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 Ξ± 𝑆 β†’ Type Ξ², 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 Ξ± 𝑆) β†’ Type Ξ²) 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 𝒦.

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.

module _ {𝒦 : Pred (Algebra Ξ± 𝑆)(ov Ξ±)} where
 β„‘ : Type (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.

← Base.Algebras.Basic Base.Algebras.Congruences β†’