Setoid.Varieties.Maltsev.Modularity¶
Day's theorem¶
This is the Setoid.Varieties.Maltsev.Modularity module of the Agda Universal Algebra Library.
This module records the Maltsev term condition for congruence modularity (CM) — the Day
identities, as a theory interpretation Th-Day n ≼ ℰ — and proves Day's theorem:
- Day terms ⟹ CM: the two-column ladder of Freese–McKenzie's Lemma 2.3,3 run
along finite alternating chains by induction on the number of
φ-steps, with the finitary collapse of the join; - CM ⟹ Day terms: the converse, which extracts the chain of Day terms from a
congruence of the free algebra
𝔽[ Fin 4 ].
For a finitary signature the two halves assemble into the complete iff
Day-theorem. Although this is exactly what
jonsson-theorem does for distributivity in
Setoid.Varieties.Maltsev.Distributivity, the forward half here is not
a mechanical mirror of the Jónsson staircase.
The construction that does work is explained below and in
design note m6-6-forward-jonsson-day.md.
Modularity of the congruence lattice¶
Congruence modularity (CM) is a property of the congruence lattice of an algebra,
defined in Setoid.Congruences.Properties as CongruenceModular (at the absorbing
relation level, so that meet and join are operations on a single type). We use it
here to phrase the Day variety condition below.
Day terms¶
Congruence modularity is characterized by a chain of quaternary terms m₀ , … , mₙ,
the Day terms (Day 1969; Burris–Sankappanavar, Thm. 12.4), with identities2
m₀(x, y, z, u) ≈ x,
mᵢ(x, y, y, x) ≈ x (all i),
mᵢ(x, x, u, u) ≈ mᵢ₊₁(x, x, u, u) (i even),
mᵢ(x, y, y, u) ≈ mᵢ₊₁(x, y, y, u) (i odd),
mₙ(x, y, z, u) ≈ u.
-- the canonical 4-element tuple over the variable carrier Fin 4 quad : {ℓ : Level}{A : Type ℓ}(a b c d : A) → Fin 4 → A quad a b c d 0F = a quad a b c d 1F = b quad a b c d 2F = c quad a b c d 3F = d -- n+1 quaternary operation symbols. Sig-Day : {n : ℕ} → Signature 0ℓ 0ℓ Sig-Day {n} = Fin (suc n) , (λ _ → Fin 4) data Eq-Day {n : ℕ} : Type where mxyzu≈x : Eq-Day -- m₀(x,y,z,u) ≈ x mxyyx≈x : Fin (suc n) → Eq-Day -- mᵢ(x,y,y,x) ≈ x mxyzu≈u : Eq-Day -- mₙ(x,y,z,u) ≈ u m-fork : Fin n → Eq-Day -- consecutive mᵢ, mᵢ₊₁ agree (parity-dependent) private d : {n : ℕ} → Fin (suc n) → (a b c d : Term (Fin 4)) → Term (Fin 4) d i a b c d = node i (quad a b c d) module _ {n : ℕ} where private x y z u : Term {𝑆 = Sig-Day{n}} (Fin 4) x = ℊ 0F ; y = ℊ 1F ; z = ℊ 2F ; u = ℊ 3F Th-Day : Eq-Day → Term (Fin 4) × Term (Fin 4) Th-Day mxyzu≈x = d fzero x y z u , x Th-Day mxyzu≈u = d (fromℕ n) x y z u , u Th-Day (mxyyx≈x i) = d i x y y x , x Th-Day (m-fork i) = if even? (toℕ i) then ( d (inject₁ i) x x u u , d (fsuc i) x x u u ) -- i even: agree on (x,x,u,u) else ( d (inject₁ i) x y y u , d (fsuc i) x y y u ) -- i odd: agree on (x,y,y,u) HasDayTerms : (n : ℕ){α ρ : Level}{𝑆 : Signature 0ℓ 0ℓ}{X : Type χ}{Idx : Type ι} → (Idx → Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X) → Type (lsuc (α ⊔ ρ) ⊔ χ ⊔ ι) HasDayTerms n {α} {ρ} ℰ = Th-Day {n} ≼ ℰ where open Interpret α ρ
Day terms imply modularity along chains¶
The forward direction of Day's theorem runs the Day terms along a
finite alternating walk from a to b whose steps lie in ϑ or in φ, the
relations of two congruences Θ, Φ. As in the Jónsson development, the walk
relation is the type Chain (Setoid.Congruences.ChainJoin), the theorem is proved
against it in full generality, and the identification with the library's generated
join Cg(Θ ∪ Φ) — JoinIsChain, finitary⇒JoinIsChain — is paid
exactly once, for the finitary signatures, which is the usual setting in
"ordinary" universal algebra.
The argument along the chain, however, is not the Jónsson staircase. Jónsson's
θ-pinning holds at every element dᵢ(a, u, b) because dᵢ(x, y, x) ≈ x leaves the middle
argument free; Day's pinning mᵢ(x, y, y, x) ≈ x requires the two middle arguments to be
equal, so the even-fork column mᵢ(a, a, b, b) is not pinnable and the two-column
staircase has no analogue. (This dead end is recorded in the design note.1) What works
instead is the classical two-part construction of Day (1969),2 in the streamlined
form of Freese–McKenzie:3
-
A collector lemma (Freese–McKenzie, Lemma 2.3): for every congruence
μand pairb μ d, if the two ladder columnsmᵢ(a, a, c, c)andmᵢ(a, b, d, c)areμ-related rung by rung, thena μ c. The climb alternates: even forks advance the first column directly (mᵢ(x, x, u, u) ≈ mᵢ₊₁(x, x, u, u)at(a, c)), odd forks advance the second (mᵢ(x, y, y, u) ≈ mᵢ₊₁(x, y, y, u)at(a, b, c), reachable becauseb μ dmoves the third slot). -
An induction on the number of
φ-steps in the chain, which manufactures the collector's hypotheses at the joinΔ = Θ ∨ (Φ ∧ Ψ). ϑ-steps absorb for free. At the first genuine alternationa φ t₁ ϑ t₂ φ t₃ ⋯ cthe collector is applied with the ϑ-pair(t₁ , t₂) ∈ Δ, and its rung hypothesis is the induction hypothesis at the pair(mᵢ(a, t₁, t₂, c) , mᵢ(a, a, c, c)): the two flanking φ-stepsa φ t₁andt₂ φ t₃fuse into a single simultaneous move in the second and third slots ofmᵢ, the remaining chain pushes through the third slot coordinatewise (m-compat), and the fused chain has strictly fewer φ-steps. Both elements of the pair areψ-tied toaby the pinning identity (usinga ψ candΘ ⊆ Ψ), which is what lets the induction hypothesis — whose statement demands aψ-tie — apply to them.
The fusion step is precisely where modularity differs from distributivity: it has no
single-column analogue, and it is what the mᵢ(x, y, y, x) ≈ x pinning buys.
The curried extraction¶
Fix a model 𝑩 of a theory ℰ with n+1 Day terms. The witnessing interpretation
Iₘ sends the i-th Day symbol to a derived 𝑆-term, whose evaluation
against the named quadruple is the curried operation m𝑩 i. The single
evaluation lemma eval-m rewrites a Day application in the reduct to
m𝑩, and the endpoint, pinning, and compatibility facts fall out by instantiating the
reduct's satisfaction of Th-Day — the verbatim quaternary analogue of the Jónsson
d𝑩 / eval-d block (over quad in place
of tri).
module _ {𝑆 : Signature 0ℓ 0ℓ}{X : Type χ}{Idx : Type ι} {ℰ : Idx → Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X}{n : ℕ} (dt : HasDayTerms n {α} {ρ} ℰ)(𝑩 : Algebra {𝑆 = 𝑆} α ρ)(B⊨ : 𝑩 ⊨ₑ ℰ) where open Setoid 𝔻[ 𝑩 ] using ( _≈_ ) renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans ) open Environment 𝑩 using ( ⟦_⟧ ) open Environment (reductᴵ 𝑩 (proj₁ dt)) using () renaming ( ⟦_⟧ to ⟦_⟧ᴿ ) -- the witnessing interpretation and the reduct's satisfaction of the Day theory Iₘ : Interpretation (Sig-Day {n}) 𝑆 Iₘ = proj₁ dt satₘ : reductᴵ 𝑩 Iₘ ⊨ₑ Th-Day satₘ = proj₂ dt 𝑩 B⊨ -- the curried i-th Day term operation m𝑩 : Fin (suc n) → (a b c d : 𝕌[ 𝑩 ]) → 𝕌[ 𝑩 ] m𝑩 i a b c d = ⟦ Iₘ i ⟧ ⟨$⟩ quad a b c d -- evaluating a Day application in the reduct lands on the curried m𝑩 eval-m : (i : Fin (suc n)){i₀ i₁ i₂ i₃ : Fin 4}(η : Fin 4 → 𝕌[ 𝑩 ]) → ⟦ node i (quad (ℊ i₀) (ℊ i₁) (ℊ i₂) (ℊ i₃)) ⟧ᴿ ⟨$⟩ η ≈ m𝑩 i (η i₀) (η i₁) (η i₂) (η i₃) eval-m i η = cong ⟦ Iₘ i ⟧ λ { 0F → ≈refl ; 1F → ≈refl ; 2F → ≈refl ; 3F → ≈refl } -- the two endpoint identities and the pinning family, curried, from satₘ m-fst : {a b c d : 𝕌[ 𝑩 ]} → m𝑩 fzero a b c d ≈ a m-fst = ≈trans (≈sym (eval-m fzero (quad _ _ _ _))) (satₘ mxyzu≈x (quad _ _ _ _)) m-lst : {a b c d : 𝕌[ 𝑩 ]} → m𝑩 (fromℕ n) a b c d ≈ d m-lst = ≈trans (≈sym (eval-m (fromℕ n) (quad _ _ _ _))) (satₘ mxyzu≈u (quad _ _ _ _)) m-mid : (i : Fin (suc n)){a b : 𝕌[ 𝑩 ]} → m𝑩 i a b b a ≈ a m-mid i {a} {b} = ≈trans (≈sym (eval-m i (quad a b b a))) (satₘ (mxyyx≈x i) (quad a b b a)) -- m𝑩 i is a term operation, hence compatible with every congruence m-compat : ((μ , _) : Con 𝑩 ℓ) (i : Fin (suc n)) {a a′ b b′ c c′ d d′ : 𝕌[ 𝑩 ]} → μ a a′ → μ b b′ → μ c c′ → μ d d′ → μ (m𝑩 i a b c d) (m𝑩 i a′ b′ c′ d′) m-compat μ i pa pb pc pd = term-compatible μ (Iₘ i) λ { 0F → pa ; 1F → pb ; 2F → pc ; 3F → pd }
The collector¶
m-collect is the substantive direction of Lemma 2.3 in
Freese–McKenzie3 for an arbitrary congruence μ: given a pair b μ d, if the
columns mᵢ(a, a, c, c) and mᵢ(a, b, d, c) are μ-related at every rung, then
a μ c.
The climb is <-weakInduction on the rung predicate
a μ mᵢ(a, a, c, c):
- the base is the endpoint identity
m₀(a, a, c, c) ≈ a; - an even fork advances the first column by the
(x, x, u, u)identity alone; - an odd fork crosses to the second column by the hypothesis, advances it — moving
the third slot
d → b(b μ d), applying the(x, y, y, u)fork, and movingb → dback — and crosses home by the hypothesis at the next rung; - the final endpoint identity
mₙ(a, a, c, c) ≈ ccloses the walk.
The walk it produces, spelled out for the first few rungs (≈ from the identities,
μ from the hypothesis, the pair b μ d, and their composites):
a ≈ m₀(a, a, c, c) -- m-fst
≈ m₁(a, a, c, c) -- even fork at 0
μ m₁(a, b, d, c) -- hypothesis at 1
μ m₂(a, b, d, c) -- odd fork at 1 (b μ d moves slot three there and back)
μ m₂(a, a, c, c) -- hypothesis at 2
≈ m₃(a, a, c, c) -- even fork at 2
⋮
mₙ(a, a, c, c) ≈ c -- m-lst
Nothing here mentions Θ, Φ, Ψ, or chains; the lemma is a fact about a single
congruence.
m-collect : ((μ , _) : Con 𝑩 ℓ){a c b d : 𝕌[ 𝑩 ]} → μ b d → ((i : Fin (suc n)) → μ (m𝑩 i a a c c) (m𝑩 i a b d c)) → μ a c m-collect {ℓ = ℓ} (μ , μcon) {a} {c} {b} {d} bμd hyp = μ-trans (rungs (fromℕ n)) (reflexive μcon m-lst) where open IsEquivalence (is-equivalence μcon) using () renaming ( refl to μ-refl ; sym to μ-sym ; trans to μ-trans ) -- the rung predicate: a is μ-below the first ladder column Rung : Fin (suc n) → Type ℓ Rung i = μ a (m𝑩 i a a c c) base-rung : Rung fzero base-rung = reflexive μcon (≈sym m-fst) -- climb one rung; the fork identity (parity-split) glues to the next index step-rung : (i : Fin n) → Rung (inject₁ i) → Rung (fsuc i) step-rung i aμu with even? (toℕ i) | satₘ (m-fork i) ... | true | fk = μ-trans aμu (reflexive μcon feq) where feq : m𝑩 (inject₁ i) a a c c ≈ m𝑩 (fsuc i) a a c c feq = ≈trans (≈sym (eval-m (inject₁ i) (quad a a c c))) (≈trans (fk (quad a a c c)) (eval-m (fsuc i) (quad a a c c))) ... | false | fk = μ-trans aμu (μ-trans (hyp (inject₁ i)) (μ-trans odd-step (μ-sym (hyp (fsuc i))))) where feq : m𝑩 (inject₁ i) a b b c ≈ m𝑩 (fsuc i) a b b c feq = ≈trans (≈sym (eval-m (inject₁ i) (quad a b b c))) (≈trans (fk (quad a b b c)) (eval-m (fsuc i) (quad a b b c))) -- advance the second column: move slot three d → b, fork, move back odd-step : μ (m𝑩 (inject₁ i) a b d c) (m𝑩 (fsuc i) a b d c) odd-step = μ-trans (m-compat (μ , μcon) (inject₁ i) μ-refl μ-refl (μ-sym bμd) μ-refl) (μ-trans (reflexive μcon feq) (m-compat (μ , μcon) (fsuc i) μ-refl μ-refl bμd μ-refl)) rungs : (i : Fin (suc n)) → Rung i rungs = <-weakInduction Rung base-rung step-rung
The chain induction¶
Fix congruences Θ, Φ, Ψ with Θ ⊆ Ψ and write Δ = Θ ∨ (Φ ∧ Ψ) for the join of
the modular law's conclusion. Throughout this block, capital letters denote the
packaged congruences and the corresponding lowercase letters ϑ, φ, ψ, δ their
underlying relations — private infix aliases for the proj₁ projections, so that the
statements below read as mathematics (x ψ y, a δ c) rather than as projections.
Two joins are in play and they must be kept straight: the hypothesis join Θ ∨ Φ
is what gets decomposed — that is why the theorem consumes a Chain — while the
conclusion join Δ is only ever introduced (∨-upperˡ/ʳ and the transitivity of
δ), never eliminated.
The induction is on the number of φ-steps in the chain (countφ),
with an inner structural recursion that normalizes the head of the chain:
absorb-ϑabsorbs ϑ-steps (a ϑ-step lands inδoutright, andΘ ⊆ Ψre-ties the new head to the far end);onφholds one open φ-step and merges any φ-steps that follow it (φ is transitive, so merging only lowers the count);onφϑholds an openφ-then-ϑhead and merges subsequent ϑ-steps likewise.
The bases are degenerate chains:
- a pure-ϑ chain collapses into
ϑ(ϑ-collapse); - a lone φ-step meets the
ψ-tie inφ ∧ ψ; - a
φ-then-ϑchain splits as(φ ∧ ψ) ∘ ϑ.
The genuine case is a head a φ t₁ ϑ t₂ φ t₃ followed by the rest of the chain.
There m-collect is applied at μ = Δ with the ϑ-pair (t₁ , t₂),
and its rung hypotheses come from the induction hypothesis at the pair
(mᵢ(a, t₁, t₂, c) , mᵢ(a, a, c, c)):
-
the ψ-tie (
m-rail):mᵢ(a, b, c, d)is ψ-tied toawhenever the outer pair(a, d)and the inner pair(b, c)are each ψ-related — the pinningm-mid, reached by ψ-moves in the third and fourth slots. Both columns qualify: formᵢ(a, t₁, t₂, c)the inner move isΘ ⊆ Ψatt₁ ϑ t₂and the outer is the ambienta ψ c; formᵢ(a, a, c, c)both area ψ c; -
the crossing chain: its first step moves slots two and three simultaneously (
t₁ → aby the opening φ-step reversed,t₂ → t₃by the closing one) — the fusion of two φ-steps of the original chain into one — and the remaining chain pushes through slot three bym-push, preserving step tags (m-push-countφ). The fused chain therefore has strictly fewer φ-steps, and the outer induction applies.
module _ (Θ Φ Ψ : Con 𝑩 ℓ)(Θ⊆Ψ : Θ ⊆ Ψ) where -- the conclusion join Δ, at the absorbing level 𝒈 ℓ = α ⊔ ρ ⊔ ℓ (since 𝓞 = 𝓥 = 0ℓ), -- and lowercase infix aliases for the underlying relations of Θ, Φ, Ψ, Δ. All are -- private abbreviations of this block (Δ in particular must not escape: the library -- already exports a Δ, in Setoid.Subalgebras.Subdirect.Finite) private Δ : Con 𝑩 (α ⊔ ρ ⊔ ℓ) Δ = Θ ∨ (Φ ∧ Ψ) _ϑ_ _φ_ _ψ_ : BinaryRel 𝕌[ 𝑩 ] ℓ _ϑ_ = Θ .proj₁ _φ_ = Φ .proj₁ _ψ_ = Ψ .proj₁ _δ_ : BinaryRel 𝕌[ 𝑩 ] (α ⊔ ρ ⊔ ℓ) _δ_ = Δ .proj₁ open IsEquivalence (is-equivalence (proj₂ Θ)) using () renaming ( refl to ϑ-refl ; trans to ϑ-trans ) 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 ; sym to ψ-sym ; trans to ψ-trans ) open IsEquivalence (is-equivalence (proj₂ Δ)) using () renaming ( sym to δ-sym ; trans to δ-trans ) -- the induction measure: the number of φ-steps in a chain countφ : {x y : 𝕌[ 𝑩 ]} → Chain 𝑩 (Θ ∪ᵣ Φ) x y → ℕ countφ (nil _) = 0 countφ (cons (inj₁ _) C) = countφ C countφ (cons (inj₂ _) C) = suc (countφ C) -- a chain with no φ-steps collapses into ϑ ϑ-collapse : {x y : 𝕌[ 𝑩 ]}(C : Chain 𝑩 (Θ ∪ᵣ Φ) x y) → countφ C ≤ 0 → x ϑ y ϑ-collapse (nil x≈y) _ = reflexive (proj₂ Θ) x≈y ϑ-collapse (cons (inj₁ s) C) le = ϑ-trans s (ϑ-collapse C le) ϑ-collapse (cons (inj₂ _) C) () -- push a chain through the third slot of m𝑩 i, coordinatewise and tag-preserving m-push : (i : Fin (suc n)) {a c u v : 𝕌[ 𝑩 ]} → Chain 𝑩 (Θ ∪ᵣ Φ) u v → Chain 𝑩 (Θ ∪ᵣ Φ) (m𝑩 i a a u c) (m𝑩 i a a v c) m-push i (nil u≈v) = nil (cong ⟦ Iₘ i ⟧ λ { 0F → ≈refl ; 1F → ≈refl ; 2F → u≈v ; 3F → ≈refl }) m-push i (cons (inj₁ s) C) = cons (inj₁ (m-compat Θ i ϑ-refl ϑ-refl s ϑ-refl)) (m-push i C) m-push i (cons (inj₂ s) C) = cons (inj₂ (m-compat Φ i φ-refl φ-refl s φ-refl)) (m-push i C) -- the push preserves the φ-count m-push-countφ : (i : Fin (suc n)) {a c u v : 𝕌[ 𝑩 ]} → (C : Chain 𝑩 (Θ ∪ᵣ Φ) u v) → countφ (m-push i {a} {c} C) ≡ countφ C m-push-countφ i (nil _) = ≡refl m-push-countφ i (cons (inj₁ _) C) = m-push-countφ i C m-push-countφ i (cons (inj₂ _) C) = ≡cong suc (m-push-countφ i C) -- the ψ-rail: mᵢ(a, b, c, d) is ψ-tied to a whenever the outer pair (a, d) and -- the inner pair (b, c) are each ψ-related — the pinning mᵢ(a, b, b, a) ≈ a, -- reached by ψ-moves in the third and fourth slots. Both ladder columns qualify m-rail : (i : Fin (suc n)){a b c d : 𝕌[ 𝑩 ]} → a ψ d → b ψ c → (m𝑩 i a b c d) ψ a m-rail i aψd bψc = ψ-trans (m-compat Ψ i ψ-refl ψ-refl (ψ-sym bψc) (ψ-sym aψd)) (reflexive (proj₂ Ψ) (m-mid i)) -- one round of the induction: the outer hypothesis `ih` covers chains with at -- most K φ-steps; the inner recursion is structural in the chain chainModStep : (K : ℕ) → ( {x y : 𝕌[ 𝑩 ]} → x ψ y → (C : Chain 𝑩 (Θ ∪ᵣ Φ) x y) → countφ C ≤ K → x δ y ) → {a c : 𝕌[ 𝑩 ]} → a ψ c → (C : Chain 𝑩 (Θ ∪ᵣ Φ) a c) → countφ C ≤ suc K → a δ c chainModStep K ih = absorb-ϑ where onφ : {x w y : 𝕌[ 𝑩 ]} → x ψ y → x φ w → (C : Chain 𝑩 (Θ ∪ᵣ Φ) w y) → suc (countφ C) ≤ suc K → x δ y onφϑ : {x t₁ t₂ y : 𝕌[ 𝑩 ]} → x ψ y → x φ t₁ → t₁ ϑ t₂ → (C : Chain 𝑩 (Θ ∪ᵣ Φ) t₂ y) → suc (countφ C) ≤ suc K → x δ y -- one open φ-step: merge following φ-steps; a lone φ-step meets the ψ-tie onφ pψ xφw (nil w≈y) _ = ∨-upperʳ Θ (Φ ∧ Ψ) (φ-trans xφw (reflexive (proj₂ Φ) w≈y) , pψ) onφ pψ xφw (cons (inj₂ s) C) le = onφ pψ (φ-trans xφw s) C (≤-trans (n≤1+n _) le) onφ pψ xφw (cons (inj₁ s) C) le = onφϑ pψ xφw s C le -- an open φ-then-ϑ head: merge following ϑ-steps; a φ∘ϑ chain splits as -- (φ ∧ ψ) ∘ ϑ; a further φ-step is the collector case onφϑ pψ xφt₁ t₁ϑt₂ (nil t₂≈y) _ = δ-trans (∨-upperʳ Θ (Φ ∧ Ψ) (xφt₁ , ψ-trans pψ (ψ-sym (Θ⊆Ψ t₁ϑy)))) (∨-upperˡ Θ (Φ ∧ Ψ) t₁ϑy) where t₁ϑy : _ ϑ _ t₁ϑy = ϑ-trans t₁ϑt₂ (reflexive (proj₂ Θ) t₂≈y) onφϑ pψ xφt₁ t₁ϑt₂ (cons (inj₁ s) C) le = onφϑ pψ xφt₁ (ϑ-trans t₁ϑt₂ s) C le onφϑ {x}{t₁}{t₂}{y} pψ xφt₁ t₁ϑt₂ (cons (inj₂ t₂φt₃) C) le = m-collect Δ (∨-upperˡ Θ (Φ ∧ Ψ) t₁ϑt₂) hyps where -- the induction hypothesis, at the ψ-railed pair of ladder columns; the -- crossing chain fuses the two flanking φ-steps into its first step and -- pushes the remaining chain through the third slot sδr : (i : Fin (suc n)) → (m𝑩 i x t₁ t₂ y) δ (m𝑩 i x x y y) sδr i = ih sψr crossing le′ where sψr : (m𝑩 i x t₁ t₂ y) ψ (m𝑩 i x x y y) sψr = ψ-trans (m-rail i pψ (Θ⊆Ψ t₁ϑt₂)) (ψ-sym (m-rail i pψ pψ)) crossing : Chain 𝑩 (Θ ∪ᵣ Φ) (m𝑩 i x t₁ t₂ y) (m𝑩 i x x y y) crossing = cons (inj₂ (m-compat Φ i φ-refl (φ-sym xφt₁) t₂φt₃ φ-refl)) (m-push i C) le′ : countφ crossing ≤ K le′ = ≤-trans (≤-reflexive (≡cong suc (m-push-countφ i C))) (s≤s⁻¹ le) hyps : (i : Fin (suc n)) → (m𝑩 i x x y y) δ (m𝑩 i x t₁ t₂ y) hyps i = δ-sym (sδr i) -- absorb ϑ-steps; a ϑ-step is a δ-step, and Θ ⊆ Ψ re-ties the head absorb-ϑ : {x y : 𝕌[ 𝑩 ]} → x ψ y → (C : Chain 𝑩 (Θ ∪ᵣ Φ) x y) → countφ C ≤ suc K → x δ y absorb-ϑ pψ (nil x≈y) _ = reflexive (proj₂ Δ) x≈y absorb-ϑ pψ (cons (inj₁ s) C) le = δ-trans (∨-upperˡ Θ (Φ ∧ Ψ) s) (absorb-ϑ (ψ-trans (ψ-sym (Θ⊆Ψ s)) pψ) C le) absorb-ϑ pψ (cons (inj₂ s) C) le = onφ pψ s C le -- the outer induction on the φ-count; at zero the chain collapses into ϑ chainModAt : (K : ℕ){a c : 𝕌[ 𝑩 ]} → a ψ c → (C : Chain 𝑩 (Θ ∪ᵣ Φ) a c) → countφ C ≤ K → a δ c chainModAt zero pψ C le = ∨-upperˡ Θ (Φ ∧ Ψ) (ϑ-collapse C le) chainModAt (suc K) pψ C le = chainModStep K (chainModAt K) pψ C le -- the chain-level modular law: ψ-tied chain endpoints are δ-related chainMod : {a c : 𝕌[ 𝑩 ]} → a ψ c → Chain 𝑩 (Θ ∪ᵣ Φ) a c → a δ c chainMod pψ C = chainModAt (countφ C) pψ C ≤-refl
Packaging the ladder as a forward statement: a variety with Day terms satisfies the
modular inclusion (θ ∨ ϕ) ∧ ψ ⊆ θ ∨ (ϕ ∧ ψ) (for θ ⊆ ψ) along every θ/ϕ-chain.
This is the finiteness-free content of Day's theorem; composing it with Gen ⊆ Chain
(the collapse of the generated join Cg(θ ∪ ϕ) to finite chains, valid for finitary
signatures) upgrades it to the literal CongruenceModular type.
module _ {𝑆 : Signature 0ℓ 0ℓ}{X : Type χ}{Idx : Type ι} {ℰ : Idx → Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X} ( (n , dt) : Σ[ n ∈ ℕ ] HasDayTerms n ℰ ) {𝑩 : Algebra {𝑆 = 𝑆} α ρ} (B⊨ : 𝑩 ⊨ₑ ℰ) where Day⇒chainModular : (θ ϕ ψ : Con 𝑩 ℓ) → θ ⊆ ψ → {a b : 𝕌[ 𝑩 ]} → proj₁ ψ a b → Chain 𝑩 (θ ∪ᵣ ϕ) a b → proj₁ (θ ∨ (ϕ ∧ ψ)) a b Day⇒chainModular = chainMod {ℰ = ℰ}{n = n} dt 𝑩 B⊨
To land the ladder in the literal CongruenceModular type (whose
join is the generated congruence Cg(θ ∪ ϕ)), the one extra ingredient is
JoinIsChain (Setoid.Congruences.ChainJoin), applied once, to the hypothesis
join. The other inclusion of the ≑ — θ ∨ (ϕ ∧ ψ) ⊆ (θ ∨ ϕ) ∧ ψ — is the trivial
lattice direction: both joinands sit below θ ∨ ϕ and, using θ ⊆ ψ, below ψ.
-- Day terms ⟹ congruence modularity (the forward half of Day's theorem), modulo -- the hypothesis JoinIsChain. The substantive inclusion is the chain ladder; the -- reverse inclusion holds in any lattice. Day⇒CongruenceModular : JoinIsChain 𝑩 (α ⊔ ρ ⊔ ℓ) → CongruenceModular 𝑩 ℓ Day⇒CongruenceModular jic θ ϕ ψ θ⊆ψ = fwd , bwd where fwd : θ ∨ (ϕ ∧ ψ) ⊆ (θ ∨ ϕ) ∧ ψ fwd = ∨-least θ (ϕ ∧ ψ) ((θ ∨ ϕ) ∧ ψ) (λ xθy → ∨-upperˡ θ ϕ xθy , θ⊆ψ xθy) (λ (xϕy , xψy) → ∨-upperʳ θ ϕ xϕy , xψy) bwd : (θ ∨ ϕ) ∧ ψ ⊆ θ ∨ (ϕ ∧ ψ) bwd (x∨y , xψy) = Day⇒chainModular θ ϕ ψ θ⊆ψ xψy (jic θ ϕ x∨y)
The Maltsev condition as a property of a variety¶
Fix a theory ℰ and the level pair (α , ρ) at which models are tested.
A congruence-modular variety is one in which all models are
congruence-modular (CM). Day's characterization of CM varieties is the iff statement
Day-Statement. The forward (term ⟹ CM) direction is proved just
below — Day+finjoin⇒CM and its unconditional finitary form
Day⇒CM — and the reverse (CM ⟹ terms) direction is proved at the
end of this module (CM⇒Day), so for finitary signatures the two halves
assemble into the complete iff Day-theorem.
module _ {α ρ : Level} {𝑆 : Signature 0ℓ 0ℓ} {X : Type χ} {Idx : Type ι} (ℓ : Level) (ℰ : Idx → Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X) where -- Every model is congruence-modular. CongruenceModularVariety : Type (χ ⊔ ι ⊔ lsuc (α ⊔ ρ ⊔ ℓ)) CongruenceModularVariety = (𝑩 : Algebra α ρ) → 𝑩 ⊨ₑ ℰ → CongruenceModular 𝑩 ℓ -- Day's theorem: CM ⇔ existence of Day terms. Both halves are PROVED: the -- forward (term ⟹ CM) half is `Day+finjoin⇒CM` below (and, finiteness-free, -- `Day⇒chainModular`); the reverse (CM ⟹ terms) half is `CM⇒Day` at the end -- of this module. `Day-theorem` assembles the iff for finitary signatures. Day-Statement : Type (χ ⊔ ι ⊔ lsuc (α ⊔ ρ ⊔ ℓ)) Day-Statement = CongruenceModularVariety ⇔ ∃[ n ] HasDayTerms n {α} {ρ} ℰ -- Forward Day at the variety level: with Day terms — and `JoinIsChain`, the -- finitary collapse of the generated join `Cg(θ ∪ ϕ)` to finite chains — every -- model is congruence-modular. This is the proj₂ (term ⟹ CM) direction of -- `Day-Statement`, modulo `JoinIsChain`. Day+finjoin⇒CM : ∃[ n ] HasDayTerms n ℰ → ( ∀ 𝑩 → JoinIsChain 𝑩 (α ⊔ ρ ⊔ ℓ) ) → CongruenceModularVariety Day+finjoin⇒CM dh jic 𝑩 B⊨ = Day⇒CongruenceModular {ℰ = ℰ} dh B⊨ {ℓ = ℓ} (jic 𝑩) -- ★ The finitary forward Day theorem. For a finitary signature the JoinIsChain -- hypothesis is automatic (`finitary⇒JoinIsChain`), so a variety with Day terms is -- congruence-modular outright — the term ⟹ CM direction of `Day-Statement` with no -- residual side condition. As everywhere in this development, the finiteness -- witness `fin` is `λ _ → _ , ↔-id _` for every `Fin`-arity signature (see -- `Examples.Setoid.FinitarySignatures`). Day⇒CM : Finitary 𝑆 → ∃[ n ] HasDayTerms n ℰ → CongruenceModularVariety Day⇒CM fin dh = Day+finjoin⇒CM dh (λ _ → finitary⇒JoinIsChain fin)
The converse of Day's theorem: CM ⟹ Day terms¶
The construction is the classical one (Day 1969; Burris–Sankappanavar, Thm. II.12.4, the
(1) ⟹ (2) direction4), run through the free-algebra congruence/derivability bridge
(cg-pair→⊢ / cg-pairs→⊢,
Setoid.Varieties.FreeSubstitution) and the parity-chain machinery of the Jónsson
converse (ParityChain, Setoid.Varieties.Maltsev.Distributivity),
which was designed to be reused here.
-
Work in
𝔽 = 𝔽[ Fin 4 ], the relatively free algebra on four generatorsx , y , z , u. It is a model of the theory (satisfies), hence congruence-modular by hypothesis. -
Take
θ = Cg ❴ y , z ❵,ϕ = Cg ❴ x , y ❵ ∨ Cg ❴ z , u ❵, andψ = Cg ❴ x , u ❵ ∨ Cg ❴ y , z ❵. Where the Jónsson converse takes three principal congruences, two of Day's are joins of two principal congruences — each must be collapsed by a substitution identifying two generator pairs at once, which is what the two-pair bridgecg-pairs→⊢is for — andθ ⊆ ψ, exactly the side condition of the modular law. The pair(x , u)lies inψ(a generator pair) and inθ ∨ ϕ(the walkx ϕ y θ z ϕ u), so the modular lawθ ∨ (ϕ ∧ ψ) ≑ (θ ∨ ϕ) ∧ ψ, read right to left, moves it intoθ ∨ (ϕ ∧ ψ). -
For a finitary signature that join membership is witnessed by a finite alternating chain (
finitary⇒JoinIsChain), which the off-phase normalizationchain→parityᵒaligns:(ϕ ∧ ψ)-steps at even positions,θ-steps at odd ones. (The join presents itsθ-steps in the first tag, but the even forks ofTh-Dayare theϕ-collapses, so the phase is swapped relative to the Jónsson converse — hence theᵒpass.) Itsn + 1elements are quaternary terms — the carrier of𝔽isTerm (Fin 4)— and they are the Day termsm₀ , … , mₙ, packaged as the interpretationI i = tᵢ. The chain length is thenof the∃[ n ]inDay-Statement. -
Each Day identity is an endpoint fact about the chain, or a congruence membership pushed through a collapsing substitution (
cg-pair→⊢for the principalθ,cg-pairs→⊢for the two-pair joinsϕandψ). The endpoint identities are the chain's endpoints (m₀is exactlyx;mₙis derivablyu). The middle familymᵢ(x, y, y, x) ≈ xcollapsesz ↦ y , u ↦ x— the twoψ-pairs — using that every chain element isψ-tied tox(head-linked: both step relations lie belowψ, the meet by its second component andθbyθ ⊆ ψ, so the walk never leaves theψ-class ofx). The fork aticollapsesy ↦ x , z ↦ u(the twoϕ-pairs) wheniis even andz ↦ y(theθ-pair) wheniis odd — precisely the parity of the normalized chain'si-th step. -
As in the Maltsev and Jónsson converses, the collapsing substitutions are chosen to be exactly the position maps
I ✦_uses on a Day application, so each bridge output is definitionally the interpreted identity, modulo the one term-level shimgraft≐[];⊧-interpandSoundness.soundthen discharge the satisfaction obligation in an arbitrary model.
Because the free algebra is built on the variable type Fin 4 : 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ℓ), and the
converse inhabits the proj₁ direction of Day-Statement at the levels
of 𝔽[ Fin 4 ] : Algebra (lsuc 0ℓ) (ι ⊔ lsuc 0ℓ) — the same instantiation as
CD⇒jonsson and CP⇒maltsev.
module _ {𝑆 : Signature 0ℓ 0ℓ} {X : Type 0ℓ} {Idx : Type ι} (ℰ : Idx → Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X) 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 four generators, and its generators 𝔽 : Algebra (lsuc 0ℓ) (ι ⊔ lsuc 0ℓ) 𝔽 = 𝔽[ Fin 4 ] private x y z u : 𝕌[ 𝔽 ] x = ℊ 0F ; y = ℊ 1F ; z = ℊ 2F ; u = ℊ 3F -- The converse half of Day's theorem: a congruence-modular variety -- over a finitary signature has a chain of Day terms. CM⇒Day : Finitary 𝑆 → CongruenceModularVariety 0ℓ ℰ → ∃[ n ] HasDayTerms n ℰ CM⇒Day fin cmv = n , I , red where -- 𝔽 is a model, hence congruence-modular by hypothesis 𝔽cm : CongruenceModular 𝔽 0ℓ 𝔽cm = cmv 𝔽 satisfies open principal 𝔽[ Fin 4 ] -- the three congruences of Day's construction; θ ⊆ ψ is the modular side condition θ ϕ ψ : Con 𝔽 (ι ⊔ lsuc 0ℓ) θ = Cg ❴ y , z ❵ ϕ = Cg ❴ x , y ❵ ∨ Cg ❴ z , u ❵ ψ = Cg ❴ x , u ❵ ∨ Cg ❴ y , z ❵ θ⊆ψ : θ ⊆ ψ θ⊆ψ = ∨-upperʳ (Cg ❴ x , u ❵) (Cg ❴ y , z ❵) -- (x , u) lies in (θ ∨ ϕ) ∧ ψ: the ψ-pair is a generator, and θ ∨ ϕ walks -- x ϕ y θ z ϕ u (the two outer steps through ϕ's two principal components) xψu : ψ .proj₁ x u xψu = ∨-upperˡ (Cg ❴ x , u ❵) (Cg ❴ y , z ❵) (base pᵣ) xθ∨ϕu : (θ ∨ ϕ) .proj₁ x u xθ∨ϕu = transitive (∨-upperʳ θ ϕ (∨-upperˡ (Cg ❴ x , y ❵) (Cg ❴ z , u ❵) (base pᵣ))) ( transitive (∨-upperˡ θ ϕ (base pᵣ)) (∨-upperʳ θ ϕ (∨-upperʳ (Cg ❴ x , y ❵) (Cg ❴ z , u ❵) (base pᵣ))) ) -- the modular law (right to left) moves the pair into θ ∨ (ϕ ∧ ψ) xδu : (θ ∨ (ϕ ∧ ψ)) .proj₁ x u xδu = (𝔽cm θ ϕ ψ θ⊆ψ) .proj₂ (xθ∨ϕu , xψu) -- the finite chain (the signature is finitary), parity-normalized *off-phase*: -- (ϕ∧ψ)-steps at even positions, θ-steps at odd positions. The proof never -- computes this chain — it only reads its fields — so it is `abstract`, which -- keeps the extraction pipeline from being unfolded during type-checking abstract pc : ParityChain 𝔽 ((ϕ ∧ ψ) .proj₁) (θ .proj₁) x u pc = chain→parityᵒ θ (ϕ ∧ ψ) (finitary⇒JoinIsChain fin θ (ϕ ∧ ψ) xδu) open ParityChain pc renaming ( len to n ; elt to t ; elt-fst to t-fst ; elt-lst to t-lst ; step to t-step ) -- the chain elements are terms — the carrier of 𝔽 is Term (Fin 4) — and they are -- the Day terms: the i-th element interprets the i-th Day symbol I : Interpretation Sig-Day 𝑆 I i = t i -- the generators of the Day signature (the source side of I) xD yD zD uD : Term {𝑆 = Sig-Day} (Fin 4) xD = ℊ 0F ; yD = ℊ 1F ; zD = ℊ 2F ; uD = ℊ 3F -- the four Day application families appearing in Th-Day, as Sig-Day terms: -- mxyzu i is mᵢ(x,y,z,u), mxyyx i is mᵢ(x,y,y,x), and so on mxyzu mxyyx mxxuu mxyyu : Fin (suc n) → Term {𝑆 = Sig-Day} (Fin 4) mxyzu i = node i (quad xD yD zD uD) mxyyx i = node i (quad xD yD yD xD) mxxuu i = node i (quad xD xD uD uD) mxyyu i = node i (quad xD yD yD uD) -- the matching collapsing substitutions: exactly the position maps `I ✦_` uses on -- the corresponding application, so `graft (t i) σ` is definitionally `I ✦ m· i` σxyzu σxyyx σxxuu σxyyu : Sub {𝑆 = 𝑆} (Fin 4) (Fin 4) σxyzu j = I ✦ quad xD yD zD uD j -- the identity positions (no collapse) σxyyx j = I ✦ quad xD yD yD xD j -- z ↦ y , u ↦ x : collapses ψ's pairs (x,u), (y,z) σxxuu j = I ✦ quad xD xD uD uD j -- y ↦ x , z ↦ u : collapses ϕ's pairs (x,y), (z,u) σxyyu j = I ✦ quad xD yD yD uD j -- z ↦ y : collapses the θ-pair (y,z) -- every chain element is ψ-tied to x: both step relations lie below ψ — the meet -- by its second component, θ by θ ⊆ ψ — so the walk never leaves the ψ-class of x xψt : (i : Fin (suc n)) → proj₁ ψ x (t i) xψt = head-linked pc ψ proj₂ θ⊆ψ -- the chain head, as a derivable equation: the setoid equality of 𝔽 *is* -- derivability, and the head is even a propositional equality (t-fst) t₀≈x : E ⊢ Fin 4 ▹ t fzero ≈ x t₀≈x = Setoid.reflexive 𝔻[ 𝔽 ] t-fst -- align the interpretation's node action (`graft`) with the bridge's substitution -- hom (`_[ σ ]`). The shim `graft≐[]` is needed only on chain-element sides: on a -- *generator* v, `graft (ℊ v) σ` and `(ℊ v) [ σ ]` are both literally `σ v`. So a -- generator right-hand side uses the one-sided form, and only the forks (chain -- elements on both sides) need the two-sided one graft-bridgeˡ : (w : 𝕌[ 𝔽 ]){v : 𝕌[ 𝔽 ]}(σ : Sub {𝑆 = 𝑆} (Fin 4) (Fin 4)) → E ⊢ Fin 4 ▹ (w [ σ ]) ≈ v → E ⊢ Fin 4 ▹ graft w σ ≈ v graft-bridgeˡ w σ d = trans (≐→⊢ (graft≐[] w σ)) d graft-bridge : (w w′ : 𝕌[ 𝔽 ])(σ : Sub {𝑆 = 𝑆} (Fin 4) (Fin 4)) → E ⊢ Fin 4 ▹ (w [ σ ]) ≈ (w′ [ σ ]) → E ⊢ Fin 4 ▹ graft w σ ≈ graft w′ σ graft-bridge w w′ σ d = trans (graft-bridgeˡ w σ d) (sym (≐→⊢ (graft≐[] w′ σ))) -- the five identity families of Th-Day, one derivation each: an endpoint fact or -- a collapsed (join of) principal-congruence membership(s), through the bridge deriv-fst : E ⊢ Fin 4 ▹ (I ✦ mxyzu fzero) ≈ (I ✦ xD) deriv-fst = graft-bridgeˡ (t fzero) σxyzu (sub t₀≈x σxyzu) deriv-lst : E ⊢ Fin 4 ▹ (I ✦ mxyzu (fromℕ n)) ≈ (I ✦ uD) deriv-lst = graft-bridgeˡ (t (fromℕ n)) σxyzu (sub t-lst σxyzu) deriv-mid : (i : Fin (suc n)) → E ⊢ Fin 4 ▹ (I ✦ mxyyx i) ≈ (I ✦ xD) deriv-mid i = graft-bridgeˡ (t i) σxyyx (sym (cg-pairs→⊢ E σxyyx x u y z refl refl (xψt i))) deriv-fork-ϕ : (i : Fin n) → proj₁ ϕ (t (inject₁ i)) (t (fsuc i)) → E ⊢ Fin 4 ▹ (I ✦ mxxuu (inject₁ i)) ≈ (I ✦ mxxuu (fsuc i)) deriv-fork-ϕ i st = graft-bridge (t (inject₁ i)) (t (fsuc i)) σxxuu (cg-pairs→⊢ E σxxuu x y z u refl refl st) deriv-fork-θ : (i : Fin n) → proj₁ θ (t (inject₁ i)) (t (fsuc i)) → E ⊢ Fin 4 ▹ (I ✦ mxyyu (inject₁ i)) ≈ (I ✦ mxyyu (fsuc i)) deriv-fork-θ i st = graft-bridge (t (inject₁ i)) (t (fsuc i)) σxyyu (cg-pair→⊢ E σxyyu y z refl st) -- discharge one interpreted identity in an arbitrary model, by soundness and the -- satisfaction condition; the equation sides p, q are passed explicitly, since -- they are not recoverable from the interpreted terms I ✦ p, I ✦ q discharge : (𝑩 : Algebra (lsuc 0ℓ) (ι ⊔ lsuc 0ℓ)) → 𝑩 ⊨ₑ ℰ → (p q : Term {𝑆 = Sig-Day} (Fin 4)) → E ⊢ Fin 4 ▹ (I ✦ p) ≈ (I ✦ q) → reductᴵ 𝑩 I ⊧ p ≈ q discharge 𝑩 B⊨ p q d = ⊧-interp 𝑩 I {s = p} {t = q} (Soundness.sound E 𝑩 B⊨ d) -- every model of ℰ satisfies the interpreted Day identities; the fork clause -- splits on the parity of i, matching the parity-normalized step of the chain red : (𝑩 : Algebra (lsuc 0ℓ) (ι ⊔ lsuc 0ℓ)) → 𝑩 ⊨ₑ ℰ → reductᴵ 𝑩 I ⊨ₑ Th-Day red 𝑩 B⊨ mxyzu≈x = discharge 𝑩 B⊨ (mxyzu fzero) xD deriv-fst red 𝑩 B⊨ (mxyyx≈x i) = discharge 𝑩 B⊨ (mxyyx i) xD (deriv-mid i) red 𝑩 B⊨ mxyzu≈u = discharge 𝑩 B⊨ (mxyzu (fromℕ n)) uD deriv-lst red 𝑩 B⊨ (m-fork i) with even? (toℕ i) | t-step i ... | true | s = discharge 𝑩 B⊨ (mxxuu (inject₁ i)) (mxxuu (fsuc i)) (deriv-fork-ϕ i (proj₁ s)) ... | false | s = discharge 𝑩 B⊨ (mxyyu (inject₁ i)) (mxyyu (fsuc i)) (deriv-fork-θ i s)
Day's theorem, the complete iff¶
With both halves in hand, Day-Statement itself is inhabited for every
finitary signature, at the levels of the free-algebra construction: a variety over a
finitary signature is congruence-modular exactly when it has a chain of Day terms.
This mirrors jonsson-theorem exactly, and closes the trio of classical
Maltsev-condition characterizations (Maltsev, Jónsson, Day) as complete iffs.
-- ★ Day's theorem (Day 1969; Freese–McKenzie, Thm. 2.2), as a complete iff. Day-theorem : Finitary 𝑆 → Day-Statement 0ℓ ℰ Day-theorem fin = CM⇒Day fin , Day⇒CM 0ℓ ℰ fin
-
A. Day, A characterization of modularity for congruence lattices of algebras, Canad. Math. Bull. 12 (1969), 167–173. doi:10.4153/CMB-1969-016-6. ↩↩
-
R. Freese and R. McKenzie, Commutator Theory for Congruence Modular Varieties, London Math. Soc. Lecture Note Series 125, Cambridge University Press (1987), Thm. 2.2 and Lemma 2.3. Free online edition. ↩↩↩
-
S. Burris and H. P. Sankappanavar, A Course in Universal Algebra, Graduate Texts in Mathematics 78, Springer (1981), Thm. II.12.4. Free online edition. ↩