Setoid.Congruences.Properties

Distributive and modular congruence lattices

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

Setoid.Congruences.CompleteLattice assembled the congruence lattice of an algebra. This module names two properties that lattice may have — being distributive and being modular — which the Maltsev conditions of congruence distributivity (Jónsson) and congruence modularity (Day) characterize by the existence of terms (Setoid.Varieties.Maltsev).

As in Setoid.Congruences.CompleteLattice, the lattice equations are stated at the absorbing relation level 𝐋 ℓ₀ = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ₀. At this level the join _∨_ (whose codomain otherwise bumps the level to 𝒈 ℓ) lands back at the level of the meet _∧_, so both are operations on Con 𝑨 (𝐋 ℓ₀) and the equations type-check.

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

open import Overture using ( 𝓞 ; 𝓥 ; Signature )

module Setoid.Congruences.Properties {𝑆 : Signature 𝓞 𝓥} where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive  using () renaming ( Set to Type )
open import Level           using ( Level ; _⊔_ ) renaming (suc to lsuc)

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Setoid.Algebras.Basic          {𝑆 = 𝑆} using ( Algebra )
open import Setoid.Congruences.Basic       {𝑆 = 𝑆} using ( Con )
open import Setoid.Congruences.Lattice     {𝑆 = 𝑆} using ( _⊆_ ; _≑_ ; _∧_ )
open import Setoid.Congruences.Generation  {𝑆 = 𝑆} using ( _∨_ )

The absorbing relation level

-- The relation level at which both meet and join are operations on Con 𝑨.
Ł : Level → Level → Level → Level
Ł α ρ ℓ₀ = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ₀

Congruence distributivity

An algebra 𝑨 is congruence-distributive (CD) when its congruence lattice satisfies the distributive law θ ∧ (φ ∨ ψ) ≑ (θ ∧ φ) ∨ (θ ∧ ψ). (The reverse containment half of this ≑ is automatic in any lattice; the distributive law is the forward containment θ ∧ (φ ∨ ψ) ⊆ (θ ∧ φ) ∨ (θ ∧ ψ), but we state the full symmetric ≑ result for uniformity.)

module _ {α ρ : Level} (𝑨 : Algebra α ρ)(ℓ₀ : Level) where
  CongruenceDistributive : Type (lsuc (Ł α ρ ℓ₀))
  CongruenceDistributive = (θ φ ψ : Con 𝑨 (Ł α ρ ℓ₀)) → θ ∧ (φ ∨ ψ) ≑ (θ ∧ φ) ∨ (θ ∧ ψ)

Congruence modularity

An algebra 𝑨 is congruence-modular (CM) when its congruence lattice satisfies the modular law: whenever θ ⊆ ψ, θ ∨ (φ ∧ ψ) ≑ (θ ∨ φ) ∧ ψ. Distributivity implies modularity, so the congruence-distributive algebras form a subclass of the congruence-modular ones.

  CongruenceModular : Type (lsuc (Ł α ρ ℓ₀))
  CongruenceModular = (θ φ ψ : Con 𝑨 (Ł α ρ ℓ₀)) → θ ⊆ ψ → θ ∨ (φ ∧ ψ) ≑ (θ ∨ φ) ∧ ψ