Setoid.Varieties.Maltsev.Permutability¶
Maltsev conditions: permutability¶
This is the Setoid.Varieties.Maltsev.Permutability module of the Agda Universal Algebra Library.
Setoid.Varieties.Maltsev.Basic fixed the term-existence side of CP as a theory
interpretation: HasMaltsevTerm ℰ = Th-Maltsev ≼ ℰ.1
The present module connects that to the lattice side (built in Setoid.Congruences.Permutability) and proves the concrete direction of Maltsev's theorem:2
a variety with a Maltsev term is congruence-permutable.
Maltsev's theorem: a Maltsev term implies congruences permute¶
Fix a theory ℰ over a signature 𝑆 (at the level pair (0ℓ , 0ℓ), as the Maltsev
condition is phrased; this is no restriction for finitary algebraic theories). We
show: if ℰ has a Maltsev term then every model 𝑩 of ℰ is congruence-permutable
(CP).
module _ {𝑆 : Signature 0ℓ 0ℓ} {X : Type χ} {Idx : Type ι} (ℰ : Idx → Term X × Term X) where MaltsevTerm⇒CP : HasMaltsevTerm ℰ → (𝑩 : Algebra α ρ) → 𝑩 ⊨ₑ ℰ → {ℓ : Level} → CongruencePermutable 𝑩 ℓ MaltsevTerm⇒CP mt 𝑩 B⊨ {ℓ} θ φ {x}{y} (z , xθz , zφy) = m𝑩 x z y , xφw , wθy where open Setoid 𝔻[ 𝑩 ] using ( _≈_ ) renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans ) open Environment 𝑩 using ( ⟦_⟧ ) open Environment (reductᴵ 𝑩 (proj₁ mt)) using () renaming ( ⟦_⟧ to ⟦_⟧ᴿ ) -- the witnessing interpretation, and the reduct's satisfaction of Th-Maltsev I : Interpretation Sig-Maltsev 𝑆 I = proj₁ mt satM : reductᴵ 𝑩 I ⊨ₑ Th-Maltsev satM = proj₂ mt 𝑩 B⊨ -- the curried Maltsev term operation: evaluate the derived term I m-Op m𝑩 : 𝕌[ 𝑩 ] → 𝕌[ 𝑩 ] → 𝕌[ 𝑩 ] → 𝕌[ 𝑩 ] m𝑩 a b c = ⟦ I m-Op ⟧ ⟨$⟩ tri a b c -- m𝑩 is a term operation, hence compatible with every congruence m-compat : (ψ : Con 𝑩 ℓ)(a a′ b b′ c c′ : 𝕌[ 𝑩 ]) → proj₁ ψ a a′ → proj₁ ψ b b′ → proj₁ ψ c c′ → proj₁ ψ (m𝑩 a b c) (m𝑩 a′ b′ c′) m-compat ψ a a′ b b′ c c′ pa pb pc = term-compatible ψ (I m-Op) {tri a b c}{tri a′ b′ c′} λ { 0F → pa ; 1F → pb ; 2F → pc } -- evaluating a Maltsev application in the reduct lands on the curried m𝑩 eval-m : (i₀ i₁ i₂ : Fin 3)(η : Fin 3 → 𝕌[ 𝑩 ]) → ⟦ m (ℊ i₀) (ℊ i₁) (ℊ i₂) ⟧ᴿ ⟨$⟩ η ≈ m𝑩 (η i₀) (η i₁) (η i₂) eval-m i₀ i₁ i₂ η = cong ⟦ I m-Op ⟧ (λ { 0F → ≈refl ; 1F → ≈refl ; 2F → ≈refl }) -- the two Maltsev identities, curried, from the reduct's satisfaction of Th-Maltsev mxxy : (a b : 𝕌[ 𝑩 ]) → m𝑩 a a b ≈ b mxxy a b = ≈trans (≈sym (eval-m 0F 0F 1F (tri a b b))) (satM mxxy≈y (tri a b b)) mxyy : (a b : 𝕌[ 𝑩 ]) → m𝑩 a b b ≈ a mxyy a b = ≈trans (≈sym (eval-m 0F 1F 1F (tri a b b))) (satM mxyy≈x (tri a b b)) -- equivalence-relation structure of the two congruences open IsEquivalence (is-equivalence (proj₂ θ)) using () renaming (refl to θ-refl; sym to θ-sym; trans to θ-trans) open IsEquivalence (is-equivalence (proj₂ φ)) using () renaming (refl to φ-refl; trans to φ-trans) -- the witness w = m(x, z, y) lies φ-above x and θ-below y -- x φ m(x,z,z) = x (identity mxyy) then m(x,z,z) φ m(x,z,y) (since z φ y) xφw : proj₁ φ x (m𝑩 x z y) xφw = φ-trans (reflexive (proj₂ φ) (≈sym (mxyy x z))) (m-compat φ x x z z z y φ-refl φ-refl zφy) -- m(x,z,y) θ m(x,x,y) (since z θ x) then m(x,x,y) = y (identity mxxy) wθy : proj₁ θ (m𝑩 x z y) y wθy = θ-trans (m-compat θ x x z x y y θ-refl (θ-sym xθz) θ-refl) (reflexive (proj₂ θ) (mxxy x y))
The theorem above is the required acceptance criterion: CP's Maltsev-term characterization, in its concrete "term ⟹ permutable" direction.
Congruence-permutable varieties¶
Fix a theory ℰ and the level pair (α , ρ) at which models are tested.
A congruence-permutable variety is one in which all models are
congruence-permutable.
The forward Maltsev theorem, restated for the whole variety, asserts that every model of a theory with a Maltsev term is congruence-permutable.
module _ {α ρ ℓ : Level} {𝑆 : Signature 0ℓ 0ℓ} {X : Type χ} {Idx : Type ι} (ℰ : Idx → Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X) where -- "Every model is congruence-permutable." CongruencePermutableVariety : Type (χ ⊔ ι ⊔ lsuc (α ⊔ ρ ⊔ ℓ)) CongruencePermutableVariety = (𝑩 : Algebra α ρ) → 𝑩 ⊨ₑ ℰ → CongruencePermutable 𝑩 ℓ -- Maltsev's theorem, forward direction, as a statement about the variety (PROVED). maltsev⇒CP : HasMaltsevTerm ℰ → CongruencePermutableVariety maltsev⇒CP mt 𝑩 B⊨ = MaltsevTerm⇒CP ℰ mt 𝑩 B⊨
The converse of Maltsev's theorem¶
The converse can be stated formally (as a checked Type), as follows:
-- A congruence-permutable variety has a Maltsev term. CP⇒maltsev-Statement : Type (χ ⊔ ι ⊔ lsuc (α ⊔ ρ ⊔ ℓ)) CP⇒maltsev-Statement = CongruencePermutableVariety → HasMaltsevTerm {α = α}{ρ} ℰ
Our goal in this section is to show that the CP⇒maltsev-Statement
type is inhabited, thereby proving the statement and completing the characterization:
a congruence-permutable variety has a Maltsev term.3
The construction is the classical one (Burris–Sankappanavar, Thm. II.12.2), run through
the free-algebra congruence/derivability bridge cg-pair→⊢
(Setoid.Varieties.FreeSubstitution).
-
Work in
𝔽[ Fin 3 ], the relatively free algebra on three generatorsx , y , z. It is a model of the theory (satisfies), hence congruence-permutable by hypothesis. -
Take the principal congruences
θ = Cg ❴ x , y ❵andφ = Cg ❴ y , z ❵. Thenx θ yandy φ z, so(θ ∘ φ) x z; permutability gives(φ ∘ θ) x z, i.e. a witness termwwithx φ wandw θ z. Since the carrier of𝔽isTerm (Fin 3), thiswis literally the Maltsev termm x y z. -
Translate the two memberships through collapsing-substitution homomorphisms (the bridge
cg-pair→⊢). Collapsingz ↦ yturnsx φ winto the derivable equationm x y y ≈ x; collapsingy ↦ xturnsw θ zintom x x y ≈ y— the two Maltsev identities. -
Package
mas the interpretationI : Th-Maltsev ≼ ℰand discharge the satisfaction obligation, for an arbitrary model𝑩, via⊧-interpandsoundness.
The collapsing substitutions are chosen to be exactly the position maps _✦_ uses when
it interprets a Maltsev application, so the bridge's output equation is definitionally
I ✦ (m x x y) ≈ I ✦ y — only the term-level shim graft≐[] (identifying
the node action graft of _✦_ with the substitution _[_] of the hom) stands between
the two, and it is one ≐→⊢ step.
Because the free algebra is built on the variable type Fin 3 : Type 0ℓ, and the free
construction shares one universe level between the equations' variables and the free
generators, the theory's variable type is taken at level 0ℓ (X : Type 0ℓ); this is
no restriction for the finitary algebraic theories the Maltsev condition concerns.
The theorem¶
Fix a theory ℰ over a signature 𝑆 : Signature 0ℓ 0ℓ, with variables X : Type 0ℓ.
We inhabit CP⇒maltsev-Statement at the levels of the free algebra
𝔽[ Fin 3 ] : Algebra (ov 0ℓ) (ι ⊔ ov 0ℓ) (here ov 0ℓ = lsuc 0ℓ, since
𝓞 = 𝓥 = 0ℓ), and at the congruence level ι ⊔ ov 0ℓ at which its principal
congruences live.
module _ {𝑆 : Signature 0ℓ 0ℓ}{X : Type 0ℓ}{Idx : Type ι} (ℰ : Idx → Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X) where CP⇒maltsev : CP⇒maltsev-Statement ℰ CP⇒maltsev cpv = I , red where -- the theory in the `I → Eq` shape that the free algebra consumes E : Idx → Eq E = toEq ℰ open FreeAlgebra E using ( 𝔽[_] ; satisfies ) -- the relatively free algebra on three generators, and its three generators 𝔽 : Algebra (lsuc 0ℓ) (ι ⊔ lsuc 0ℓ) 𝔽 = 𝔽[ Fin 3 ] x y z : 𝕌[ 𝔽 ] x = ℊ 0F ; y = ℊ 1F ; z = ℊ 2F -- 𝔽 is a model, hence congruence-permutable by hypothesis 𝔽cp : CongruencePermutable 𝔽 (ι ⊔ lsuc 0ℓ) 𝔽cp = cpv 𝔽 satisfies open principal 𝔽[ Fin 3 ] -- the two principal congruences θ φ : Con 𝔽 (ι ⊔ lsuc 0ℓ) θ = Cg ❴ x , y ❵ φ = Cg ❴ y , z ❵ xθy : proj₁ θ x y xθy = base pᵣ yφz : proj₁ φ y z yφz = base pᵣ -- permutability: from (x , z) ∈ θ ∘ φ get (x , z) ∈ φ ∘ θ, with witness w perm : Σ[ v ∈ 𝕌[ 𝔽 ] ] (proj₁ φ x v × proj₁ θ v z) perm = 𝔽cp θ φ (y , xθy , yφz) w : 𝕌[ 𝔽 ] w = proj₁ perm xφw : proj₁ φ x w xφw = proj₁ (proj₂ perm) wθz : proj₁ θ w z wθz = proj₂ (proj₂ perm) -- the witness term packaged as the Maltsev interpretation I : Interpretation Sig-Maltsev 𝑆 I m-Op = w -- the collapsing substitutions: exactly the position maps `I ✦` uses on a -- Maltsev application, so that `graft w σ` is definitionally `I ✦ (m _ _ _)` σxxy σxyy : Sub {𝑆 = 𝑆} (Fin 3) (Fin 3) σxxy i = I ✦ tri (ℊᴹ 0F) (ℊᴹ 0F) (ℊᴹ 1F) i σxyy i = I ✦ tri (ℊᴹ 0F) (ℊᴹ 1F) (ℊᴹ 1F) i -- the bridge: collapse turns each membership into a derivable equation bridge-xxy : E ⊢ Fin 3 ▹ w [ σxxy ] ≈ z [ σxxy ] bridge-xxy = cg-pair→⊢ E σxxy x y refl wθz bridge-xyy : E ⊢ Fin 3 ▹ x [ σxyy ] ≈ w [ σxyy ] bridge-xyy = cg-pair→⊢ E σxyy y z refl xφw -- the two Maltsev identities, as the interpreted equations deriv-xxy : E ⊢ Fin 3 ▹ I ✦ proj₁ (Th-Maltsev mxxy≈y) ≈ I ✦ proj₂ (Th-Maltsev mxxy≈y) deriv-xxy = trans (≐→⊢ (graft≐[] w σxxy)) bridge-xxy deriv-xyy : E ⊢ Fin 3 ▹ I ✦ proj₁ (Th-Maltsev mxyy≈x) ≈ I ✦ proj₂ (Th-Maltsev mxyy≈x) deriv-xyy = trans (≐→⊢ (graft≐[] w σxyy)) (sym bridge-xyy) -- every model satisfying ℰ satisfies the interpreted Maltsev identities red : (𝑩 : Algebra (lsuc 0ℓ) (ι ⊔ lsuc 0ℓ)) → 𝑩 ⊨ₑ ℰ → reductᴵ 𝑩 I ⊨ₑ Th-Maltsev red 𝑩 B⊨ mxxy≈y = Goal where Goal : reductᴵ 𝑩 I ⊧ m (ℊ 0F) (ℊ 0F) (ℊ 1F) ≈ (ℊ 1F) Goal = ⊧-interp 𝑩 I {s = proj₁ (Th-Maltsev mxxy≈y)} {t = proj₂ (Th-Maltsev mxxy≈y)} (Soundness.sound E 𝑩 B⊨ deriv-xxy) red 𝑩 B⊨ mxyy≈x = Goal where Goal : reductᴵ 𝑩 I ⊧ m (ℊ 0F) (ℊ 1F) (ℊ 1F) ≈ (ℊ 0F) Goal = ⊧-interp 𝑩 I {s = proj₁ (Th-Maltsev mxyy≈x)} {t = proj₂ (Th-Maltsev mxyy≈x)} (Soundness.sound E 𝑩 B⊨ deriv-xyy)
-
The design choice — encoding each condition as
Th-X ≼ ℰrather than as a record bundling a term with its identities, or an inductive scheme of identities — is discussed in the design notedocs/notes/m6-3-maltsev-conditions.md; in short, the interpretation encoding is the "term plus its identities", packaged so that the whole interpretability apparatus (Setoid.Varieties.Interpretation) applies uniformly to every condition. ↩ -
A. I. Mal'cev, On the general theory of algebraic systems (Russian), Mat. Sb. (N.S.) 35(77) (1954), 3–20; Engl. transl., Amer. Math. Soc. Transl. (2) 27 (1963), 125–142. Original at Math-Net.Ru; translation in Eighteen Papers on Algebra (AMS). ↩
-
A. I. Mal'cev, On the general theory of algebraic systems (Russian), Mat. Sb. (N.S.) 35(77) (1954), 3–20; Burris and Sankappanavar, A Course in Universal Algebra, Thm. II.12.2. ↩