Skip to content

Setoid.Congruences.Finite

Finitely enumerable congruence lattices

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

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 #-}

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

module Setoid.Congruences.Finite {𝑆 : Signature π“ž π“₯} 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 ; _βŠ”_ ; 0β„“
                                                          ; 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 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 clv Ξ± ρ = π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ, 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.

-- The absorbing congruence level at which the enumeration below is carried out.
clv : (Ξ± ρ : Level) β†’ Level
clv Ξ± ρ = π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ

-- A congruence together with a decision procedure for its membership.
DecCon : (𝑨 : Algebra Ξ± ρ)(β„“ : Level) β†’ Type (clv Ξ± ρ βŠ” 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.

record FiniteCongruences (𝑨 : Algebra Ξ± ρ) : Type (lsuc (clv Ξ± ρ)) where
  field
    -- a finite list of decidable congruences of 𝑨 ...
    cons      : List (DecCon 𝑨 (clv Ξ± ρ))
    -- ... exhausting the congruence lattice of 𝑨, up to ≑
    complete  : (Ο† : Con 𝑨 (clv Ξ± ρ))
              β†’ Ξ£[ d ∈ DecCon 𝑨 (clv Ξ± ρ) ] (d ∈ cons) Γ— (Ο† ≑ proj₁ d)

  witness : (Ο† : Con 𝑨 (clv Ξ± ρ)) β†’ DecCon 𝑨 (clv Ξ± ρ)
  witness = proj₁ ∘ complete

  witness∈ : (Ο† : Con 𝑨 (clv Ξ± ρ)) β†’ witness Ο† ∈ cons
  witness∈ = proj₁ ∘ projβ‚‚ ∘ complete

  witness≑ : (Ο† : Con 𝑨 (clv Ξ± ρ)) β†’ Ο† ≑ 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 _ {𝑨 : Algebra Ξ± ρ} (π‘ͺ : FiniteCongruences 𝑨) where
  open FiniteCongruences π‘ͺ
  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ )

  private
    -- The diagonal congruence at the working level.
    Ξ” : Con 𝑨 (clv Ξ± ρ)
    Ξ” = 𝟘[ 𝑨 ] {clv Ξ± ρ}

  -- 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).
𝟏-Ξ” : DecCon 𝟏 (clv 0β„“ 0β„“)
𝟏-Ξ” = ((Ξ» _ _ β†’ Lift (clv 0β„“ 0β„“) ⊀)
      , 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