Skip to content

Setoid.Congruences.Finite.Basic

Finitely enumerable congruence lattices

This is the Setoid.Congruences.Finite.Basic module of the Agda Universal Algebra Library.

While Setoid.Algebras.Finite defines the finiteness interface for a setoid algebra (decidable β‰ˆ and a finite surjective enumeration of the carrier), this module supplies the finiteness interface for congruences, that is, decidable congruences (DecCon) and the record type FiniteCongruences 𝑨.

FiniteCongruences 𝑨 packages a finite list cons of decidable congruences of 𝑨 along with a proof that this list is complete in the sense that every congruence of 𝑨 is, up to mutual containment ≑, one of those in cons.

This provides a searchable congruence lattice that finite-algebra theorems run their algorithms over; its first consumer is the finite Birkhoff theorem of Setoid.Subalgebras.Subdirect.Finite.

Why carrier finiteness does not suffice

Crucially, the data packaged here is strictly stronger than a FiniteAlgebra witness, which is why the two interfaces are separate records. Carrier-finiteness along with decidable setoid equality do not, by themselves, admit a complete congruence enumeration constructively.

Indeed, a congruence is a Type-valued relation π•Œ[ 𝑨 ] β†’ π•Œ[ 𝑨 ] β†’ Type β„“, and an arbitrary such relation on a finite carrier need not be decidable; e.g., on a bare set of two elements, the relation that collapses the two points iff P holds is a congruence for any proposition P, and it is ≑-equal to a decidable congruence only iff P is decidable.

Thus, a complete enumeration of congruences-up-to-≑ is strictly stronger than decidable equality on a finite set; it is exactly the classical content of "finite algebra" for congruence-lattice purposes. Classically every finite algebra furnishes these data; constructively they must be supplied, and this record is the interface through which they are.

The two interfaces are logically independent in the other direction as well: an infinite algebra can perfectly well have a finitely enumerable congruence lattice (consider an algebra that is constructively simple, with decidable equality β€” its complete list is the diagonal and the total congruence), so FiniteCongruences does not presuppose a finite carrier.

There is, however, one overlap, recorded as β‰ˆ-dec below: completeness forces the listed representative of the diagonal to decide setoid equality, so the _β‰Ÿ_ field of FiniteAlgebra is derivable from a FiniteCongruences witness.

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

module Setoid.Congruences.Finite.Basic where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ----------------------------------------------
open import Data.List.Base                         using  ( List ; [] ; _∷_ )
open import Data.List.Membership.Propositional     using  ( _∈_ )
open import Data.List.Relation.Unary.Any           using  ( here )
open import Data.Product                           using  ( _Γ—_ ; _,_ ; Ξ£-syntax
                                                          ; proj₁ ; projβ‚‚ )
open import Data.Unit.Base                         using  ( ⊀ ; tt )
open import Function                               using  ( _∘_ )
open import Level                                  using  ( Level ; _βŠ”_ ; Lift ; lift ; lower )
                                                   renaming ( suc to lsuc )
open import Relation.Binary                        using  ( Setoid )
                                                   renaming ( Rel to BinaryRel )
open import Relation.Binary.PropositionalEquality  using  ( refl )
open import Relation.Nullary                       using  ( Dec ; yes ; no )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture                       using ( π“ž ; π“₯ ; Signature ; 𝑆 )
open import Setoid.Algebras.Basic          using ( Algebra ; π•Œ[_] ; 𝔻[_] )
open import Setoid.Algebras.Finite         using ( 𝟏 )
open import Setoid.Congruences.Basic       using ( Con ; mkcon ; reflexive ; 𝟘[_] )
open import Setoid.Congruences.Lattice     using ( _≑_ )

private variable α ρ : Level

Decidable congruences and the working level

A decidable congruence is a congruence whose membership relation is decidable. The working congruence level is the absorbing level π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ, at which the generated (principal) congruences used downstream (e.g. for the monolith in the finite Birkhoff construction) stay put β€” the same level discipline as in Setoid.Congruences.CompleteLattice.

-- A congruence together with a decision procedure for its membership.
DecCon : {𝑆 : Signature π“ž π“₯}(𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ)(β„“ : Level) β†’ Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ βŠ” lsuc β„“)
DecCon 𝑨 β„“ = Ξ£[ (_ΞΈ_ , _) ∈ Con 𝑨 β„“ ] βˆ€ x y β†’ Dec (x ΞΈ y)

-- The underlying relation of a decidable congruence.
ConRel : {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ}{β„“ : Level} β†’ DecCon 𝑨 β„“ β†’ BinaryRel π•Œ[ 𝑨 ] β„“
ConRel ((ΞΈ , _) , _) = ΞΈ

The congruence-side finiteness interface

The record bundles a finite list cons of decidable congruences and a proof complete that the list exhausts the congruence lattice up to ≑. The witness* helpers project, for any congruence, its listed representative together with the membership and ≑-equality proofs.1

record FiniteCongruences {𝑆 : Signature π“ž π“₯}(𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) : Type (lsuc (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ)) where
  field
    -- a finite list of decidable congruences of 𝑨 ...
    cons      : List (DecCon 𝑨 (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ))
    -- ... exhausting the congruence lattice of 𝑨, up to ≑
    complete  : βˆ€ Ο† β†’ Ξ£[ d ∈ DecCon 𝑨 _ ] d ∈ cons Γ— Ο† ≑ proj₁ d

  witness : βˆ€ Ο† β†’ DecCon 𝑨 (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ)
  witness = proj₁ ∘ complete

  witness∈ : βˆ€ Ο† β†’ witness Ο† ∈ cons
  witness∈ = proj₁ ∘ projβ‚‚ ∘ complete

  witness≑ : βˆ€ Ο† β†’ Ο† ≑ proj₁ (witness Ο†)
  witness≑ = projβ‚‚ ∘ projβ‚‚ ∘ complete

As promised, a FiniteCongruences witness decides setoid equality: the diagonal congruence 𝟘[ 𝑨 ] has a listed representative whose decidable membership coincides, up to the two containments of ≑, with β‰ˆ.

module _ {π“ž π“₯ : Level}{𝑆 : Signature π“ž π“₯}{𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ} (π‘ͺ : FiniteCongruences 𝑨) where
  open FiniteCongruences π‘ͺ
  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ )

  private
    -- The diagonal congruence at the working level.
    Ξ” : Con 𝑨 (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ)
    Ξ” = 𝟘[ 𝑨 ] {π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ}

  -- Setoid equality is decidable whenever the congruence lattice is
  -- finitely enumerable: ask the diagonal's listed representative.
  β‰ˆ-dec : (x y : π•Œ[ 𝑨 ]) β†’ Dec (x β‰ˆ y)
  β‰ˆ-dec x y with projβ‚‚ (witness Ξ”) x y
  ... | yes dxy  = yes (lower (projβ‚‚ (witness≑ Ξ”) dxy))
  ... | no Β¬dxy  = no Ξ» xβ‰ˆy β†’ Β¬dxy (proj₁ (witness≑ Ξ”) (lift xβ‰ˆy))

Non-vacuity: the one-element algebra

The one-element algebra 𝟏 of Setoid.Algebras.Finite has, up to ≑, exactly one congruence β€” the all-relation, which on a one-point carrier is also the diagonal β€” so its complete list is a singleton.

-- The sole decidable congruence of 𝟏: the all-relation (= the diagonal on a point).
𝟏-Ξ” : {π“ž π“₯ : Level}{𝑆 : Signature π“ž π“₯} β†’ DecCon (𝟏 {𝑆 = 𝑆}) (π“ž βŠ” π“₯)
𝟏-Ξ” {π“ž = π“ž}{π“₯ = π“₯} = ((Ξ» _ _ β†’ Lift (π“ž βŠ” π“₯) ⊀)
      , mkcon  (Ξ» _ β†’ lift tt)
               (record { refl = lift tt ; sym = Ξ» _ β†’ lift tt ; trans = Ξ» _ _ β†’ lift tt })
               (Ξ» _ _ β†’ lift tt))
      , (Ξ» _ _ β†’ yes (lift tt))

-- The congruence lattice of 𝟏 is finitely enumerable.
open FiniteCongruences
𝟏-FiniteCongruences : FiniteCongruences (𝟏 {𝑆 = 𝑆})
𝟏-FiniteCongruences .cons = 𝟏-Ξ” ∷ []
𝟏-FiniteCongruences .complete ( _ , Ο†con ) =
  𝟏-Ξ” , here refl , (Ξ» _ β†’ lift tt) , Ξ» x β†’ reflexive Ο†con tt

  1. In the definition of FiniteCongruences, each occurrence of βˆ€ Ο† β†’ ... could be expressed more explicitly as Ο† : Con 𝑨 (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ) β†’ .... ↩