Skip to content

Setoid.Congruences.Basic

Congruences of Setoid Algebras

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

A congruence of an algebra 𝑨 is a binary relation on the carrier of 𝑨 that is an equivalence relation, contains the setoid equality of 𝑨, and is compatible with the basic operations: applying an operation to argument tuples that are related coordinatewise gives related results.

The compatibility half is _βˆ£β‰ˆ_; IsCongruence adds the other two conditions, and Con is the bundled Ξ£-form that the rest of the library passes around, with IsCongruenceβ†’Con and Conβ†’IsCongruence converting between them.

The reason to require containment of the setoid equality is that a congruence has to be an equivalence relation on the setoid, not merely on the carrier: a quotient by a relation that split an equality class would not be well defined.

With the congruence in hand _β•±_ forms the quotient algebra, which is the same carrier under the coarser equivalence, needing neither a quotient type nor extensionality. Kernels of homomorphisms are the primary source of congruences; see Setoid.Homomorphisms.Kernels.

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

module Setoid.Congruences.Basic where

-- Imports from the Agda Standard Library ---------------------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _,_ ; Ξ£-syntax ; projβ‚‚ )
open import Data.Unit.Base   using ( ⊀ ; tt )
open import Function         using ( Func )
open import Level            using ( Level ; _βŠ”_ ; Lift ; lift ; lower )
open import Relation.Binary  using ( Setoid ; IsEquivalence )
                             renaming ( Rel to BinaryRel )

open import Relation.Binary.PropositionalEquality using ( refl )

-- Imports from the Agda Universal Algebras Library ------------------------------
open import Overture               using ( _|:_ ; Equivalence ; π“ž ; π“₯ ; Signature ; 𝑆 )
open import Setoid.Relations       using ( βŸͺ_⟫ ; _/_ ; βŸͺ_∼_⟫-elim )
open import Setoid.Algebras.Basic  using ( ov ; Algebra ; 𝔻[_] ; π•Œ[_] ; _^_ )

private variable Ξ± ρ β„“ : Level

We now define the predicate _βˆ£β‰ˆ_ so that, if 𝑨 denotes an algebra and R a binary relation, then 𝑨 βˆ£β‰ˆ R will represent the assertion that R is compatible with all basic operations of 𝑨. The formal definition is immediate since all the work is done by the relation |:, which we defined above (see Setoid.Relations.Discrete).

-- Algebra compatibility with binary relation
_βˆ£β‰ˆ_ : (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) β†’ BinaryRel π•Œ[ 𝑨 ] β„“ β†’ Type _
𝑨 βˆ£β‰ˆ R = βˆ€ 𝑓 β†’ (𝑓 ^ 𝑨) |: R

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.

As mentioned above, congruences should contain the equality relation on the underlying setoid. That is, they must be reflexive; hence, the reflexive field in the definition of IsCongruence.

module _ {𝑆 : Signature π“ž π“₯} (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) where
  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ )
  record IsCongruence (ΞΈ : BinaryRel π•Œ[ 𝑨 ] β„“) : Type (π“ž βŠ” π“₯ βŠ” ρ βŠ” β„“ βŠ” Ξ±)  where
    constructor mkcon
    field
      reflexive : βˆ€ {aβ‚€ a₁} β†’ aβ‚€ β‰ˆ a₁ β†’ ΞΈ aβ‚€ a₁
      is-equivalence : IsEquivalence ΞΈ
      is-compatible  : 𝑨 βˆ£β‰ˆ ΞΈ

    Eqv : Equivalence π•Œ[ 𝑨 ] {β„“}
    Eqv = ΞΈ , is-equivalence

  open IsCongruence public

  Con : (β„“ : Level) β†’ Type (Ξ± βŠ” ρ βŠ” ov {𝑆 = 𝑆} β„“)
  Con β„“ = Ξ£[ ΞΈ ∈ BinaryRel π•Œ[ 𝑨 ] β„“ ] 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.

module _ {𝑆 : Signature π“ž π“₯} {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ} where
  IsCongruenceβ†’Con : (ΞΈ : BinaryRel π•Œ[ 𝑨 ] β„“) β†’ IsCongruence 𝑨 ΞΈ β†’ Con 𝑨 β„“
  IsCongruence→Con θ p = θ , p

  Conβ†’IsCongruence : ((ΞΈ , _) : Con 𝑨 β„“) β†’ IsCongruence 𝑨 ΞΈ
  Con→IsCongruence (_ , p) = p

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.

(Note that the forward-slash we use to denote the quotient is produced by typing \--- (in the Agda input method); it is a unicode character, and it is not the ascii forward-slash that appears in the preceding paragraph.)

module _ {𝑆 : Signature π“ž π“₯}  where
  open Algebra  using ( Domain ; Interp )
  open Func     using ( cong ) renaming ( to to _⟨$⟩_ )

  _β•±_ : (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) β†’ Con 𝑨 β„“ β†’ Algebra Ξ± β„“
  (𝑨 β•± ΞΈ) .Domain = π•Œ[ 𝑨 ] / (Eqv (projβ‚‚ ΞΈ))
  (𝑨 β•± ΞΈ) .Interp ⟨$⟩ (f , a) = (f ^ 𝑨) a
  (𝑨 β•± ΞΈ) .Interp .cong {f , u} {.f , v} (refl , a) = is-compatible (projβ‚‚ ΞΈ) f a

  module _ (𝑨 : Algebra Ξ± ρ) where
    open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ )

    _/βˆ™_ : π•Œ[ 𝑨 ] β†’ (ΞΈ : Con 𝑨 β„“) β†’ π•Œ[ 𝑨 β•± ΞΈ ]
    a /βˆ™ ΞΈ = a

    /-≑ : ((_ΞΈ_ , ΞΈcon) : Con 𝑨 β„“){u v : π•Œ[ 𝑨 ]}
      β†’ βŸͺ u ⟫{Eqv ΞΈcon} β‰ˆ βŸͺ v ⟫{Eqv ΞΈcon} β†’ u ΞΈ v

    /-≑ ΞΈ uv = reflexive (Conβ†’IsCongruence ΞΈ) uv

The least and greatest congruences

Every algebra has a least and a greatest congruence. The least is the diagonal (identity) congruence 𝟘[ 𝑨 ], which relates exactly the β‰ˆ-equal elements β€” it is the setoid equality, viewed as a congruence. The greatest is the total congruence πŸ™[ 𝑨 ], which relates everything. These are the bottom and top of the congruence lattice (their order properties β€” that they really are least and greatest β€” are recorded in Setoid.Congruences.Lattice, where the containment order _βŠ†_ is available).

Both are level-polymorphic via Lift, so they can be taken at whatever relation level the surrounding context dictates (e.g. the absorbing level at which the congruence lattice is assembled in Setoid.Congruences.CompleteLattice); the diagonal's result lives at ρ βŠ” β„“, the total's at β„“.

The only non-trivial obligation is compatibility with the operations. For the diagonal this is exactly the statement that the operations of 𝑨 respect its setoid equality β€” i.e. the cong field of Interp 𝑨 β€” which is why the diagonal congruence cannot live in Overture (which has no algebra to appeal to) and belongs here. For the total congruence compatibility is trivial, since every two elements are related.

  -- The least (diagonal) congruence of 𝑨: relates exactly the β‰ˆ-equal pairs.
  𝟘[_] : (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ){β„“ : Level} β†’ Con 𝑨 (ρ βŠ” β„“)
  𝟘[ 𝑨 ] {β„“} = (Ξ» x y β†’ Lift β„“ (x β‰ˆ y)) , mkcon (Ξ» e β†’ lift e) 𝟘-isEquiv 𝟘-compatible
    where
    open Setoid 𝔻[ 𝑨 ]  using ( _β‰ˆ_ )
                         renaming ( refl to β‰ˆrefl ; sym to β‰ˆsym ; trans to β‰ˆtrans )

    𝟘-isEquiv : IsEquivalence (Ξ» x y β†’ Lift β„“ (x β‰ˆ y))
    𝟘-isEquiv = record  { refl   = lift β‰ˆrefl
                        ; sym    = Ξ» p β†’ lift (β‰ˆsym (lower p))
                        ; trans  = Ξ» p q β†’ lift (β‰ˆtrans (lower p) (lower q)) }

    -- compatibility is precisely that the operations respect β‰ˆ (the cong of Interp)
    𝟘-compatible : 𝑨 βˆ£β‰ˆ Ξ» x y β†’ Lift β„“ (x β‰ˆ y)
    𝟘-compatible f h = lift (𝑨 .Interp .cong (refl , Ξ» i β†’ lower (h i)))

  -- The greatest (total) congruence of 𝑨: relates every pair.
  πŸ™[_] : (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ){β„“ : Level} β†’ Con 𝑨 β„“
  πŸ™[ 𝑨 ] {β„“} = (Ξ» _ _ β†’ Lift β„“ ⊀) , mkcon (Ξ» _ β†’ lift tt) πŸ™-isEquiv (Ξ» _ _ β†’ lift tt)
    where
    πŸ™-isEquiv : IsEquivalence (Ξ» (_ _ : π•Œ[ 𝑨 ]) β†’ Lift β„“ ⊀)
    πŸ™-isEquiv = record { refl = lift tt ; sym = Ξ» _ β†’ lift tt ; trans = Ξ» _ _ β†’ lift tt }