Classical.Signatures.Finite¶

Finite finitary witnesses for concrete signatures¶

This is the Classical.Signatures.Finite module of the Agda Universal Algebra Library.

The record FiniteSignature of Setoid.Signatures.Finite packages what it means for a signature to be finite finitary: a finite surjective enumeration of its operation symbols, plus the Finitary witness that every arity is finite. This module supplies the following canonical sanity-check instances:¹

Sig-Lattice (Classical.Signatures.Lattice): two binary operation symbols; both halves of the witness are finite case splits;
Sig-Group (Classical.Signatures.Group): three operation symbols, of arities two, zero, and one;
Sig-Unary A (Classical.Signatures.Unary): one unary symbol per element of A; the witness is exactly an enumeration of A.

A caveat on enumerations up to `≈`¶

The symbol type of a signature is a bare type, so opEnum-sur demands surjectivity up to propositional equality _≡_. The carrier enumeration of a FiniteAlgebra (Setoid.Algebras.Finite) is surjective only up to the carrier's setoid equality _≈_, which is not enough here. Indeed, on a quotient carrier the enumeration hits every element up to the coarser ≈ while missing raw elements up to ≡.

Consequently Sig-Unary-FiniteSignature below asks for an honest _≡_-surjective enumeration of the bare type A rather than for a FiniteAlgebra witness. In the intended applications this costs nothing; in points of fact,

for a concrete finite group the raw carrier is typically Fin n or a finite data type, where ≈ is ≡;
the raw carrier of a quotient G / H is that of G itself, so the same bare enumeration serves all coset algebras of G with no choice of coset representatives.

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

module Classical.Signatures.Finite where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive               using () renaming ( Set to Type )
open import Data.Fin.Base                using ( Fin ; zero ; suc )
open import Data.Nat.Base                using ( ℕ )
open import Data.Product                 using ( _,_ ; ∃-syntax )
open import Function.Construct.Identity  using ( ↔-id )
open import Level                        using ( Level )

open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Signatures.Group    using ( Sig-Group ; ∙-Op ; ε-Op ; ⁻¹-Op )
open import Classical.Signatures.Lattice  using ( Sig-Lattice ; ∧-Op ; ∨-Op )
open import Classical.Signatures.Unary    using ( Sig-Unary )
open import Setoid.Congruences.ChainJoin  using ( Finitary )
open import Setoid.Signatures.Finite      using ( FiniteSignature )

open FiniteSignature

The lattice signature is finite and finitary¶

Both lattice operation symbols are binary, so the Finitary witness names the identity bijection once per symbol, and the symbol enumeration lists the two symbols.

-- The lattice signature is finitary: each operation symbol has finite arity.
Sig-Lattice-Finitary : Finitary Sig-Lattice
Sig-Lattice-Finitary ∧-Op = 2 , ↔-id _
Sig-Lattice-Finitary ∨-Op = 2 , ↔-id _

-- The lattice signature is finite: there are two operation symbols.
Sig-Lattice-FiniteSignature : FiniteSignature Sig-Lattice
Sig-Lattice-FiniteSignature .opCard              = 2
Sig-Lattice-FiniteSignature .opEnum zero         = ∧-Op
Sig-Lattice-FiniteSignature .opEnum (suc zero)   = ∨-Op
Sig-Lattice-FiniteSignature .opEnum-sur ∧-Op     = zero , refl
Sig-Lattice-FiniteSignature .opEnum-sur ∨-Op     = suc zero , refl
Sig-Lattice-FiniteSignature .finitary            = Sig-Lattice-Finitary

The group signature is finite and finitary¶

The three group operation symbols have arities Fin 2, Fin 0, and Fin 1, each already of the shape Finitary demands, so the arity half is again the identity bijection in each case. From this witness we can derive the decidable generated congruence of Setoid.Congruences.Presented.Decidable, and hence the normal closure of Classical.Structures.Group.NormalClosure, over a finite group.

-- The group signature is finitary: each operation symbol has finite arity.
Sig-Group-Finitary : Finitary Sig-Group
Sig-Group-Finitary ∙-Op   = 2 , ↔-id _
Sig-Group-Finitary ε-Op   = 0 , ↔-id _
Sig-Group-Finitary ⁻¹-Op  = 1 , ↔-id _

-- The group signature is finite: there are three operation symbols.
Sig-Group-FiniteSignature : FiniteSignature Sig-Group
Sig-Group-FiniteSignature .opCard                    = 3
Sig-Group-FiniteSignature .opEnum zero               = ∙-Op
Sig-Group-FiniteSignature .opEnum (suc zero)         = ε-Op
Sig-Group-FiniteSignature .opEnum (suc (suc zero))   = ⁻¹-Op
Sig-Group-FiniteSignature .opEnum-sur ∙-Op           = zero , refl
Sig-Group-FiniteSignature .opEnum-sur ε-Op           = suc zero , refl
Sig-Group-FiniteSignature .opEnum-sur ⁻¹-Op          = suc (suc zero) , refl
Sig-Group-FiniteSignature .finitary                  = Sig-Group-Finitary

The unary signature over an enumerated symbol type¶

Given a surjective (up to _≡_) enumeration of the bare type A, the unary signature over A is finite and finitary: the symbol enumeration is the given one, and every arity is Fin 1 definitionally.

module _ {ℓ : Level}{A : Type ℓ}
         (n : ℕ)(e : Fin n → A)(e-sur : (a : A) → ∃[ i ] e i ≡ a) where

  -- The unary signature over an enumerated symbol type is finite.
  Sig-Unary-FiniteSignature : FiniteSignature (Sig-Unary A)
  Sig-Unary-FiniteSignature .opCard      = n
  Sig-Unary-FiniteSignature .opEnum      = e
  Sig-Unary-FiniteSignature .opEnum-sur  = e-sur
  Sig-Unary-FiniteSignature .finitary _  = 1 , ↔-id _

We place these instances here, rather than beside the record, because concrete signatures live in the Classical/ tree and the Setoid/ tree does not import it. ↩