Setoid.Congruences.Permutability¶
Relation composition and congruence permutability¶
This is the Setoid.Congruences.Permutability module of the Agda Universal Algebra Library.
Setoid.Congruences.Lattice and Setoid.Congruences.Generation built the congruence lattice of an algebra — meet (intersection), join (generated by the union), and the containment order. Permutability is a property transverse to that lattice: it asks how two congruences sit relative to one another under relation composition, an operation that is not part of the lattice structure and does not in general return a congruence.
The relational composition θ ∘ φ holds at (x , y) exactly when some z has
x θ z and z φ y. Two congruences permute when θ ∘ φ ⊆ φ ∘ θ; because the
reverse inclusion is the same statement with θ and φ swapped, the assertion that
every pair of congruences permute is the assertion that composition is commutative
on Con 𝑨.
An algebra (or a variety) with this property is called congruence-permutable, and
this is the property that the classical Maltsev condition characterizes by a single
ternary term (Setoid.Varieties.Maltsev).
This module is pure congruence theory: it depends only on the congruence record of Setoid.Congruences.Basic, not on terms, interpretations, or the lattice bundles.
Relation composition of congruences¶
For congruences θ φ : Con 𝑨 ℓ we write θ ∘ φ for the composition of their
underlying relations: (θ ∘ φ) x y is inhabited by a witness z together with
proofs x θ z and z φ y. The composition is a bare binary relation, not a
congruence — it need not be transitive — so its codomain is BinaryRel, and the
existential bumps the relation level from ℓ to α ⊔ ℓ, the witness ranging over
the carrier 𝕌[ 𝑨 ] : Type α.
module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρ} where _∘_ : Con 𝑨 ℓ → Con 𝑨 ℓ → BinaryRel 𝕌[ 𝑨 ] (α ⊔ ℓ) ((_θ_ , _) ∘ (_φ_ , _)) x y = ∃[ z ∈ 𝕌[ 𝑨 ] ] x θ z × z φ y infixr 7 _∘_
A composition θ ∘ φ always contains each factor, because a congruence is
reflexive (it contains the underlying setoid equality, hence is reflexive in the
ordinary sense). Inserting the relevant reflexive step on the right (resp. left)
embeds θ (resp. φ) into the composite.
open IsEquivalence using (refl) -- θ ⊆ θ ∘ φ ∘-inˡ : (θ φ : Con 𝑨 ℓ){x y : 𝕌[ 𝑨 ]} → proj₁ θ x y → (θ ∘ φ) x y ∘-inˡ _ (_ , isCongφ) {x}{y} xθy = y , xθy , isCongφ .is-equivalence .refl -- φ ⊆ θ ∘ φ ∘-inʳ : (θ φ : Con 𝑨 ℓ){x y : 𝕌[ 𝑨 ]} → proj₁ φ x y → (θ ∘ φ) x y ∘-inʳ (_ , isCongθ) _ {x} xφy = x , isCongθ .is-equivalence .refl , xφy
Permutability¶
A pair of congruences permutes when θ ∘ φ is contained in φ ∘ θ.
(Here _⊆_ is the standard-library relation-inclusion _⇒_: R ⊆ S means
∀ {x y} → R x y → S x y.)
-- θ and φ permute: θ ∘ φ ⊆ φ ∘ θ. Permutes : Con 𝑨 ℓ → Con 𝑨 ℓ → Type (α ⊔ ℓ) Permutes θ φ = θ ∘ φ ⊆ φ ∘ θ
Congruence-permutable algebras¶
An algebra is congruence-permutable (at relation level ℓ) when every pair of
its congruences permutes.
CongruencePermutable : (𝑨 : Algebra {𝑆 = 𝑆} α ρ)(ℓ : Level) → Type (α ⊔ ρ ⊔ ov {𝑆 = 𝑆} ℓ) CongruencePermutable 𝑨 ℓ = (θ φ : Con 𝑨 ℓ) → Permutes θ φ
Permutability of every pair is symmetric "for free"; from Permutes θ φ and
Permutes φ θ we get mutual containment: θ ∘ φ ⊆ φ ∘ θ and φ ∘ θ ⊆ θ ∘ φ.
Hence in a congruence-permutable algebra composition is genuinely commutative on
congruences — the conventional statement θ ∘ φ = φ ∘ θ, read here as mutual
containment, the setoid notion of equal relations.
module _ {𝑨 : Algebra {𝑆 = 𝑆} α ρ} where -- In a congruence-permutable algebra, every two congruences commute (both -- inclusions hold), since CP supplies `Permutes` in either order. permutable⇒commute : CongruencePermutable 𝑨 ℓ → (θ φ : Con 𝑨 ℓ) → (θ ∘ φ) ⊆ (φ ∘ θ) × (φ ∘ θ) ⊆ (θ ∘ φ) permutable⇒commute cp θ φ = cp θ φ , cp φ θ