Skip to content

Setoid.Varieties.Maltsev.Basic

The Maltsev condition as a theory interpretation

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

A Maltsev condition is a property of a variety equivalent to the existence of terms satisfying prescribed identities. The three most basic concern the shape of the congruence lattices of the algebras in the variety:

  • congruence permutability (CP) β€” composition of congruences is commutative;
  • congruence distributivity (CD) β€” every congruence lattice is distributive;
  • congruence modularity (CM) β€” every congruence lattice is modular.

A Maltsev term for a variety 𝒱 is a ternary term m satisfying

m(x, x, y) β‰ˆ y      and      m(x, y, y) β‰ˆ x,

and a variety has such a term exactly when it is CP.

This is the original Maltsev condition and it is quintessential universal algebra β€” a property of an arbitrary variety, phrased over an arbitrary signature, with no commitment to any particular structure.

This module fixes the abstract data of the condition and frames it as a theory interpretation (Setoid.Varieties.Interpretation): the one-ternary-symbol signature Sig-Maltsev, the two-equation theory Th-Maltsev, and the predicate HasMaltsevTerm β„° = Th-Maltsev β‰Ό β„°. "β„° admits a Maltsev term" is exactly "the Maltsev theory interprets into β„°".

A worked example β€” that x βˆ™ (y ⁻¹ βˆ™ z) is a Maltsev term for the variety of groups β€” is structure-specific (it consumes the group operations and laws), so it lives one layer up, in Classical.Interpretations.Maltsev.

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

module Setoid.Varieties.Maltsev.Basic where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ----------------------------
open import Data.Bool.Base     using ( Bool ; true ; not )
open import Data.Fin.Base      using ( Fin )
open import Data.Fin.Patterns  using ( 0F ; 1F ; 2F )
open import Data.Nat.Base      using ( β„• ; zero ; suc )
open import Data.Product       using ( _Γ—_ ; _,_ ; projβ‚‚ )
open import Level              using ( Level ; 0β„“ ; _βŠ”_ ) renaming ( suc to lsuc )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Overture.Signatures              using ( π“ž ; π“₯ ; Signature )
open import Setoid.Algebras.Basic            using ( Algebra ; 𝔻[_] ; π•Œ[_] )
open import Setoid.Congruences.Basic         using ( Con ; is-compatible )
open import Setoid.Terms.Basic               using ( _[_] ; module Environment )
open import Setoid.Varieties.Interpretation  using ( module Interpret )
import Overture.Terms as Terms

open import Function using ( Func )
open Func using () renaming ( to to _⟨$⟩_ )

private variable Ξ± ρ Ο‡ β„“ : Level

The Maltsev signature and theory

Sig-Maltsev has a single ternary operation symbol; Th-Maltsev carries the two Maltsev equations over the variable carrier Fin 3 (0F for x, 1F for y).

data Op-Maltsev : Type where
  m-Op : Op-Maltsev

ar-Maltsev : Op-Maltsev β†’ Type
ar-Maltsev m-Op = Fin 3

Sig-Maltsev : Signature 0β„“ 0β„“
Sig-Maltsev = Op-Maltsev , ar-Maltsev

-- The canonical 3-element tuple, as a *named* function (not an extended lambda),
-- so the worked-instance proofs can refer to it definitionally.
tri : {β„“ : Level} {A : Type β„“} β†’ A β†’ A β†’ A β†’ Fin 3 β†’ A
tri a b c 0F = a
tri a b c 1F = b
tri a b c 2F = c

module _ where
  open Terms {𝑆 = Sig-Maltsev} using ( Term ; β„Š ; node )
  -- the ternary application m(a, b, c) as a Sig-Maltsev term
  m : {X : Type} β†’ Term X β†’ Term X β†’ Term X β†’ Term X
  m a b c = node m-Op (tri a b c)

  private
    x y z : Term (Fin 3)
    x = β„Š 0F ; y = β„Š 1F ; z = β„Š 2F

  data Eq-Maltsev : Type where
    mxxyβ‰ˆy mxyyβ‰ˆx : Eq-Maltsev

  Th-Maltsev : Eq-Maltsev β†’ Term (Fin 3) Γ— Term (Fin 3)
  Th-Maltsev mxxyβ‰ˆy = m x x y , y   -- m(x, x, y) β‰ˆ y
  Th-Maltsev mxyyβ‰ˆx = m x y y , x   -- m(x, y, y) β‰ˆ x

The Maltsev condition

A theory β„° (equivalently, its variety) has a Maltsev term (equivalently, is congruence-permutable) exactly when the Maltsev theory interprets into it. This is the clean, signature-agnostic statement of the condition; a concrete variety satisfies it by exhibiting an interpretation Th-Maltsev β‰Ό β„°, that is, an β„°-term witnessing the two Maltsev equations.

The target theory's signature is fixed at (0β„“ , 0β„“), matching Sig-Maltsev (the interpretability relation β‰Ό relates theories over a common level pair); this is no restriction for the finitary algebraic theories the Maltsev condition concerns.

module _
  {Ξ± ρ Ο‡ ΞΉ  : Level}
  {𝑆        : Signature 0β„“ 0β„“}
  {X        : Type Ο‡}
  {Idx      : Type ΞΉ}
  where
  open Terms {𝑆 = 𝑆} using (Term)

  HasMaltsevTerm : (Idx β†’ Term X Γ— Term X) β†’ Type (lsuc (Ξ± βŠ” ρ) βŠ” Ο‡ βŠ” ΞΉ)
  HasMaltsevTerm β„° = Th-Maltsev β‰Ό β„°
    where open Interpret α ρ

Miscellaneous prerequisites

Maltsev arguments rely on the fact that the chosen Maltsev term operation respects every congruence. This is an instance of a fundamental fact, which we prove once in full generality: Given an algebra 𝑩 and a term t in the signature of 𝑩, every congruence ψ of 𝑩 is compatible with the evaluation of t β€” if two environments are pointwise ψ-related at the leaves, the values of t are ψ-related. The proof is the obvious structural induction.

module _
  {𝑆 : Signature π“ž π“₯}
  {𝑩 : Algebra {𝑆 = 𝑆} Ξ± ρ}
  where
  open Environment 𝑩 using ( ⟦_⟧ )
  open Terms {𝑆 = 𝑆} using (Term ; β„Š ; node)

  term-compatible : {V : Type Ο‡ } ((_ψ_ , _) : Con 𝑩 β„“ )
    (t : Term V ) {Ξ· Ξ·β€²     : V β†’ π•Œ[ 𝑩 ] }
    β†’ (βˆ€ v β†’ (Ξ· v) ψ (Ξ·β€² v)) β†’ (⟦ t ⟧ ⟨$⟩ Ξ·) ψ (⟦ t ⟧ ⟨$⟩ Ξ·β€²)
  term-compatible _ (β„Š v) h = h v
  term-compatible ψ (node f ts) h = is-compatible (ψ .projβ‚‚) f (Ξ» i β†’ term-compatible ψ (ts i) h)

Finally, a function indicating the parity of a natural number is needed to split the JΓ³nsson/Day "fork" identities by index in Setoid.Varieties.Maltsev.Distributivity and Setoid.Varieties.Maltsev.Modularity.

even? : β„• β†’ Bool
even? zero = true
even? (suc m) = not (even? m)