Skip to content

Setoid.Congruences.CompleteLattice

The Complete Lattice of Congruences

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

Setoid.Congruences.Lattice gave the meet (intersection) and the containment order, and Setoid.Congruences.Generation gave the join ΞΈ ∨ Ο† = Cg(ΞΈ βˆͺ Ο†) via the congruence-generation theorem. This module assembles those pieces into the congruence lattice of an algebra and shows it is complete.

The one wrinkle is universe levels. The meet preserves the relation level β„“, but the join lands at π’ˆ β„“ = π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ βŠ” β„“ (the closure quantifies over the operations and the carrier). To make meet and join the same binary operation on a single type, we evaluate the congruence lattice at a relation level that already absorbs that bump: for a base level β„“β‚€, at which π’ˆ L = L,

L = π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ βŠ” β„“β‚€.

At level L both _∧_ and _∨_ are operations on Con 𝑨 {L}, so they fit a standard-library Lattice bundle, and with the bounds βŠ₯/⊀ a BoundedLattice.

For completeness we add infinitary meets β¨… (intersection of a family) and joins ⨆ (generated by the union of a family), each proved to be the relevant greatest-lower / least-upper bound, and package them in the CompleteLattice record of Order.CompleteLattice.

The family index I is required to live at the base level β„“β‚€, so the lattice is complete with respect to β„“β‚€-small families β€” the usual predicative reading.

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

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

module Setoid.Congruences.CompleteLattice {𝑆 : Signature π“ž π“₯} where

-- Imports from the Agda Standard Library ---------------------------------------
open import Agda.Primitive               using () renaming ( Set to Type )
open import Data.Product                 using ( _,_ ; proj₁ ; projβ‚‚ ; Ξ£-syntax )
open import Level                        using ( Level ; _βŠ”_ )
open import Relation.Binary              using ( Setoid ; IsEquivalence )
open import Relation.Binary.Definitions  using ( Maximum ; Minimum )
open import Relation.Binary.Lattice      using ( Supremum ; IsLattice
                                               ; Lattice ; IsBoundedLattice
                                               ; BoundedLattice )

-- Imports from the Agda Universal Algebras Library ------------------------------
open import Setoid.Algebras.Basic            {𝑆 = 𝑆}  using  ( ov ; Algebra ; π•Œ[_] ; 𝔻[_] )
open import Order.CompleteLattice                     using  ( CompleteLattice )
open import Setoid.Congruences.Basic         {𝑆 = 𝑆}  using  ( Con ; mkcon ; _βˆ£β‰ˆ_
                                                             ; reflexive ; is-equivalence
                                                             ; is-compatible ; 𝟘[_] ; πŸ™[_] )
open import Setoid.Congruences.Lattice       {𝑆 = 𝑆}  using  ( _≑_ ; _βŠ†_ ; _∧_
                                                             ; βŠ†-isPartialOrder
                                                             ; ∧-infimum ; 𝟘-min ; πŸ™-max )
open import Setoid.Congruences.Generation    {𝑆 = 𝑆}  using  ( Cg ; Cg-least ; base
                                                             ; _∨_ ; ∨-upperˑ
                                                             ; ∨-upperʳ ; ∨-least )
private variable Ξ± ρ β„“β‚€ : Level

The congruence lattice at the absorbing level L

We fix an algebra 𝑨 and a base level β„“β‚€, and work with congruences whose relation level is L = π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ βŠ” β„“β‚€. Because level join is idempotent, π’ˆ L = L, so the join _∨_ (whose codomain is Con 𝑨 {π’ˆ L}) is an operation on Con 𝑨 {L}, exactly like the meet.

module _ (𝑨 : Algebra Ξ± ρ) (β„“β‚€ : Level) where
  L : Level
  L = π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ βŠ” β„“β‚€

  private
    Conα΄Έ : Type (Ξ± βŠ” ρ βŠ” ov L)
    Conα΄Έ = Con 𝑨 L

The join is the least upper bound: the two upper-bound facts come from Generation, and the universality is ∨-least.

  Con-supremum : Supremum (_βŠ†_ {𝑨 = 𝑨} {L}) _∨_
  Con-supremum ΞΈ Ο†  = ∨-upperΛ‘ ΞΈ Ο†
                    , ∨-upperΚ³ ΞΈ Ο†
                    , Ξ» ψ ΞΈβŠ†Οˆ Ο†βŠ†Οˆ β†’ ∨-least ΞΈ Ο† ψ ΞΈβŠ†Οˆ Ο†βŠ†Οˆ

Assembling the partial order, the supremum, and the meet's infimum gives the lattice.

  Con-isLattice : IsLattice (_≑_ {𝑨 = 𝑨} {L}) _βŠ†_ _∨_ _∧_
  Con-isLattice = record  { isPartialOrder  = βŠ†-isPartialOrder
                          ; supremum        = Con-supremum
                          ; infimum         = ∧-infimum
                          }

  Con-Lattice : Lattice (Ξ± βŠ” ρ βŠ” ov L) (Ξ± βŠ” L) (Ξ± βŠ” L)
  Con-Lattice = record  { Carrier    = Conα΄Έ
                        ; _β‰ˆ_        = _≑_
                        ; _≀_        = _βŠ†_
                        ; _∨_        = _∨_
                        ; _∧_        = _∧_
                        ; isLattice  = Con-isLattice
                        }

The bounds: zero and total congruences

The bottom congruence 0ᴬ is the diagonal congruence 𝟘[ 𝑨 ] and the top congruence 1ᴬ is the total congruence πŸ™[ 𝑨 ], both from Setoid.Congruences.Basic, taken at the absorbing level L. Their minimality and maximality are the order facts 𝟘-min / πŸ™-max of Setoid.Congruences.Lattice.

(The least congruence is the diagonal β€” the identity relation viewed as a congruence β€” not the empty relation: the empty relation is not even reflexive, so it is not a congruence at all. An earlier version defined 0ᴬ = Cg 0A as the congruence generated by the empty relation; that is in fact the diagonal, since Cg closes under reflexivity over β‰ˆ, but the direct definition 𝟘[ 𝑨 ] is the standard and clearer one.)

  0ᴬ : Conᴸ
  0ᴬ = 𝟘[ 𝑨 ] {L}

  1ᴬ : Conᴸ
  1ᴬ = πŸ™[ 𝑨 ] {L}

  0ᴬ-minimum : Minimum _βŠ†_ 0ᴬ
  0ᴬ-minimum ΞΈ = 𝟘-min {β„“ = L} ΞΈ

  1ᴬ-maximum : Maximum _βŠ†_ 1ᴬ
  1ᴬ-maximum ΞΈ = πŸ™-max ΞΈ

With the bounds the lattice becomes a bounded lattice (1ᴬ is the maximum, 0ᴬ the minimum).

  Con-isBoundedLattice : IsBoundedLattice (_≑_ {𝑨 = 𝑨} {L}) _βŠ†_ _∨_ _∧_ 1ᴬ 0ᴬ
  Con-isBoundedLattice = record  { isLattice  = Con-isLattice
                                 ; maximum    = 1ᴬ-maximum
                                 ; minimum    = 0ᴬ-minimum
                                 }

  Con-BoundedLattice : BoundedLattice (Ξ± βŠ” ρ βŠ” ov L) (Ξ± βŠ” L) (Ξ± βŠ” L)
  Con-BoundedLattice = record  { Carrier           = Conα΄Έ
                               ; _β‰ˆ_               = _≑_
                               ; _≀_               = _βŠ†_
                               ; _∨_               = _∨_
                               ; _∧_               = _∧_
                               ; ⊀                 = 1ᴬ
                               ; βŠ₯                 = 0ᴬ
                               ; isBoundedLattice  = Con-isBoundedLattice
                               }

Infinitary meets and joins

For a family f : I β†’ Con 𝑨 {L} indexed by I : Type β„“β‚€, the infinitary meet is the intersection β‹€ f (which holds at (x , y) iff every f i does), and the infinitary join is the congruence generated by the union, ⋁ f = Cg(⋃ f). Both stay at level L because I is β„“β‚€-small. The meet is the greatest lower bound and the join the least upper bound of the family.

  module _ {I : Type β„“β‚€} (f : I β†’ Conα΄Έ) where

    -- Infinitary meet: the intersection of the family.
    β‹€ : Conα΄Έ
    β‹€ = (Ξ» x y β†’ (i : I) β†’ proj₁ (f i) x y) , mkcon m-refl m-equiv m-comp
      where
      open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ )
      m-refl : βˆ€ {aβ‚€ a₁} β†’ aβ‚€ β‰ˆ a₁ β†’ (i : I) β†’ proj₁ (f i) aβ‚€ a₁
      m-refl e i = reflexive (projβ‚‚ (f i)) e

      m-equiv : IsEquivalence (Ξ» x y β†’ (i : I) β†’ proj₁ (f i) x y)
      m-equiv = record
        { refl   = Ξ» i β†’ IsEquivalence.refl (is-equivalence (projβ‚‚ (f i)))
        ; sym    = Ξ» p i β†’ IsEquivalence.sym (is-equivalence (projβ‚‚ (f i))) (p i)
        ; trans  = Ξ» p q i β†’ IsEquivalence.trans (is-equivalence (projβ‚‚ (f i))) (p i) (q i)
        }

      m-comp : 𝑨 βˆ£β‰ˆ (Ξ» x y β†’ (i : I) β†’ proj₁ (f i) x y)
      m-comp g h i = is-compatible (projβ‚‚ (f i)) g (Ξ» k β†’ h k i)

    -- Infinitary join: the congruence generated by the union of the family.
    ⋁ : Conα΄Έ
    ⋁ = Cg (Ξ» x y β†’ Ξ£[ i ∈ I ] proj₁ (f i) x y)

    β‹€-lower : (i : I) β†’ β‹€ βŠ† f i
    β‹€-lower i p = p i

    β‹€-greatest : (ψ : Conα΄Έ) β†’ (βˆ€ i β†’ ψ βŠ† f i) β†’ ψ βŠ† β‹€
    β‹€-greatest ψ ΟˆβŠ†f p i = ΟˆβŠ†f i p

    ⋁-upper : (i : I) β†’ f i βŠ† ⋁
    ⋁-upper i p = base (i , p)

    ⋁-least : (ψ : Conα΄Έ) β†’ (βˆ€ i β†’ f i βŠ† ψ) β†’ ⋁ βŠ† ψ
    ⋁-least ψ fβŠ†Οˆ = Cg-least {𝑨 = 𝑨} ψ (Ξ» (i , p) β†’ fβŠ†Οˆ i p)

The complete lattice

Packaging the order with the infinitary operations and their universal properties yields the complete lattice of congruences.

  Con-CompleteLattice : CompleteLattice (Ξ± βŠ” ρ βŠ” ov L) (Ξ± βŠ” L) (Ξ± βŠ” L) β„“β‚€
  Con-CompleteLattice = record
    { Carrier          = Conα΄Έ
    ; _β‰ˆ_              = _≑_
    ; _≀_              = _βŠ†_
    ; isPartialOrder   = βŠ†-isPartialOrder
    ; ⨆                = ⋁
    ; β¨…                = β‹€
    ; ⨆-upper          = Ξ» f i β†’ ⋁-upper f i
    ; ⨆-least          = Ξ» f x h β†’ ⋁-least f x h
    ; β¨…-lower          = Ξ» f i β†’ β‹€-lower f i
    ; β¨…-greatest       = Ξ» f x h β†’ β‹€-greatest f x h
    }