Agda UALib ↑

Congruence Relations

This section presents the Algebras.Congruences module of the Agda Universal Algebra Library.


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

open import Algebras.Signatures using (Signature; π“ž; π“₯)

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

open import Algebras.Products {𝑆 = 𝑆} public

A congruence relation of an algebra 𝑨 is defined to be an equivalence relation that is compatible with the basic operations of 𝑨. This concept can be represented in a number of alternative but equivalent ways. Formally, we define a record type (IsCongruence) to represent the property of being a congruence, and we define a Sigma type (Con) to represent the type of congruences of a given algebra.


module _ {𝓦 𝓀 : Universe} where

 record IsCongruence (𝑨 : Algebra 𝓀 𝑆)(ΞΈ : Rel ∣ 𝑨 ∣ 𝓦) : ov 𝓦 βŠ” 𝓀 Μ‡  where
  constructor mkcon
  field       is-equivalence : IsEquivalence ΞΈ
              is-compatible  : compatible 𝑨 ΞΈ

 Con : (𝑨 : Algebra 𝓀 𝑆) β†’ 𝓀 βŠ” ov 𝓦 Μ‡
 Con 𝑨 = Ξ£ ΞΈ κž‰ ( Rel ∣ 𝑨 ∣ 𝓦 ) , IsCongruence 𝑨 ΞΈ

Each of these types captures what it means to be a congruence and they are equivalent in the sense that each implies the other. One implication is the β€œuncurry” operation and the other is the second projection.


 IsCongruenceβ†’Con : {𝑨 : Algebra 𝓀 𝑆}(ΞΈ : Rel ∣ 𝑨 ∣ 𝓦) β†’ IsCongruence 𝑨 ΞΈ β†’ Con 𝑨
 IsCongruence→Con θ p = θ , p

 Conβ†’IsCongruence : {𝑨 : Algebra 𝓀 𝑆} β†’ ((ΞΈ , _) : Con 𝑨) β†’ IsCongruence 𝑨 ΞΈ
 Conβ†’IsCongruence ΞΈ = βˆ₯ ΞΈ βˆ₯

Example

We defined the zero relation 𝟎 in the Relations.Discrete module. We now build the trivial congruence, which has 𝟎 as its underlying relation. Observe that 𝟎 is equivalent to the identity relation ≑ and these are obviously both equivalence relations. In fact, we already proved this of ≑ in the Overture.Equality module, so we simply apply the corresponding proofs.


𝟎-IsEquivalence : {A : 𝓀 Μ‡} β†’  IsEquivalence {A = A} 𝟎
𝟎-IsEquivalence = record {rfl = refl; sym = ≑-sym; trans = ≑-trans}

Next we formally record another obvious factβ€”that 𝟎-rel is compatible with all operations of all algebras.


𝟎-compatible-op : funext π“₯ 𝓀 β†’ {𝑨 : Algebra 𝓀 𝑆} (𝑓 : ∣ 𝑆 ∣) β†’ (𝑓 Μ‚ 𝑨) |: 𝟎
𝟎-compatible-op fe {𝑨} 𝑓 {i}{j} ptws0  = ap (𝑓 Μ‚ 𝑨) (fe ptws0)

𝟎-compatible : funext π“₯ 𝓀 β†’ {𝑨 : Algebra 𝓀 𝑆} β†’ compatible 𝑨 𝟎
𝟎-compatible fe {𝑨} = Ξ» 𝑓 args β†’ 𝟎-compatible-op fe {𝑨} 𝑓 args

Finally, we have the ingredients need to construct the zero congruence of any algebra we like.


Ξ” : (𝑨 : Algebra 𝓀 𝑆){fe : funext π“₯ 𝓀} β†’ IsCongruence 𝑨 𝟎
Ξ” 𝑨 {fe} = mkcon 𝟎-IsEquivalence (𝟎-compatible fe)

𝟘 : (𝑨 : Algebra 𝓀 𝑆){fe : funext π“₯ 𝓀} β†’ Con{𝓀} 𝑨
𝟘 𝑨 {fe} = IsCongruenceβ†’Con 𝟎 (Ξ” 𝑨 {fe})

A concrete example is βŸͺ𝟎⟫[ 𝑨 β•± ΞΈ ], presented in the next subsection.

Quotient algebras

In many areas of abstract mathematics the quotient of an algebra 𝑨 with respect to a congruence relation ΞΈ of 𝑨 plays an important role. This quotient is typically denoted by 𝑨 / ΞΈ and Agda allows us to define and express quotients using this standard notation.1


module _ {𝓀 𝓦 : Universe} where

 _β•±_ : (𝑨 : Algebra 𝓀 𝑆) β†’ Con{𝓦} 𝑨 β†’ Algebra (𝓀 βŠ” 𝓦 ⁺) 𝑆

 𝑨 β•± ΞΈ = (∣ 𝑨 ∣ / ∣ ΞΈ ∣)  ,                               -- the domain of the quotient algebra

         Ξ» 𝑓 π‘Ž β†’ βŸͺ (𝑓 Μ‚ 𝑨)(Ξ» i β†’  fst βˆ₯ π‘Ž i βˆ₯) ⟫           -- the basic operations of the quotient algebra

Example. If we adopt the notation 𝟎[ 𝑨 β•± ΞΈ ] for the zero (or identity) relation on the quotient algebra 𝑨 β•± ΞΈ, then we define the zero relation as follows.



 𝟘[_β•±_] : (𝑨 : Algebra 𝓀 𝑆)(ΞΈ : Con {𝓦} 𝑨) β†’ Rel (∣ 𝑨 ∣ / ∣ ΞΈ ∣)(𝓀 βŠ” 𝓦 ⁺)
 𝟘[ 𝑨 β•± ΞΈ ] = Ξ» u v β†’ u ≑ v

From this we easily obtain the zero congruence of 𝑨 β•± ΞΈ by applying the Ξ” function defined above.


 𝟎[_β•±_] : (𝑨 : Algebra 𝓀 𝑆)(ΞΈ : Con{𝓦} 𝑨){fe : funext π“₯ (𝓀 βŠ” 𝓦 ⁺)} β†’ Con (𝑨 β•± ΞΈ)
 𝟎[ 𝑨 β•± ΞΈ ] {fe} = 𝟘[ 𝑨 β•± ΞΈ ] , Ξ” (𝑨 β•± ΞΈ) {fe}

Finally, the following elimination rule is sometimes useful.


module _ {𝓀 𝓦 : Universe}{𝑨 : Algebra 𝓀 𝑆} where
 open IsCongruence

 /-≑ : (ΞΈ : Con{𝓦} 𝑨){u v : ∣ 𝑨 ∣} β†’ βŸͺ u ⟫ {∣ ΞΈ ∣} ≑ βŸͺ v ⟫ β†’ ∣ ΞΈ ∣ u v
 /-≑ ΞΈ refl = IsEquivalence.rfl (is-equivalence βˆ₯ ΞΈ βˆ₯)

1 Unicode Hints. Produce the β•± symbol in agda2-mode by typing \--- and then C-f a number of times.



← Algebras.Products Homomorphisms β†’