Setoid.Subalgebras.Subdirect.Finite¶
Finite Birkhoff: a constructive subdirect SI-representation¶
This is the Setoid.Subalgebras.Subdirect.Finite module of the Agda Universal Algebra Library.
Setoid.Subalgebras.Subdirect.BirkhoffSI proved the choice-free core of
Birkhoff's subdirect representation theorem and stated the general theorem
Birkhoff-subdirect relative to the choice principle SubdirectSIRep 𝑨.
Recall, the theorem asserts the existence, for every algebra, of a separating family of congruences whose quotients are subdirectly irreducible.
Producing that family for an arbitrary algebra is a Zorn's-lemma step (a congruence maximal among those excluding a given pair), which is incompatible with a postulate-free formalization in constructive type theory.
This module discharges that parameter for a class of finite algebras; it constructs
SubdirectSIRep 𝑨 outright, with no choice and no postulate, and feeds it to the
choice-free reduction SIRep→Representable.1
What "finite" must mean here¶
The classical proof selects, for each pair a ≢ b, a congruence maximal among
those not relating a and b; such a congruence is completely meet-irreducible, so
its quotient is subdirectly irreducible. To find that maximal congruence by a
search we must enumerate the congruence lattice, and to recognise subdirect
irreducibility (whose monolith condition quantifies over all congruences of the
quotient) the enumeration must be complete — every congruence must equal a listed
one, up to mutual containment (denote here ≑).
Crucially, carrier-finiteness along with decidable setoid equality do not, by themselves, admit such an enumeration constructively (see Setoid.Congruences.Finite for the counterexample), so the finiteness data comes through two independent interfaces.
FiniteAlgebra, from Setoid.Algebras.Finite: decidable≈and a finite surjective enumeration of the carrier, used here to count the pairs a congruence relates;FiniteCongruences, from Setoid.Congruences.Finite: a finite list of decidable congruences (DecCon), complete up to≑— the searchable congruence lattice.
Everything downstream is then fully constructive and computes. Classically every
finite algebra furnishes both witnesses, so finite-Birkhoff is Birkhoff's theorem
for finite algebras; the two records are precisely the constructive data that make
the search go through under --safe Agda.
Two generic list lemmas¶
The maximal-congruence search is driven by counting, so we first record two
elementary, signature-agnostic facts about the length of a filtered list under two
decidable predicates P ⊆ Q: the count is monotone, and it is strictly smaller
whenever some listed element satisfies Q but not P.
private variable ℓ₁ ℓ₂ ℓ₃ : Level private module _ {X : Type ℓ₁}{P : X → Type ℓ₂}{Q : X → Type ℓ₃} (P? : (x : X) → Dec (P x))(Q? : (x : X) → Dec (Q x)) (sub : ∀ {x} → P x → Q x) where -- If P entails Q then no more elements pass the P-filter than the Q-filter. filter-length-mono : (xs : List X) → length (filter P? xs) ≤ length (filter Q? xs) filter-length-mono [] = z≤n filter-length-mono (x ∷ xs) with P? x | Q? x ... | yes _ | yes _ = s≤s (filter-length-mono xs) ... | yes px | no ¬qx = ⊥-elim (¬qx (sub px)) ... | no _ | yes _ = m≤n⇒m≤1+n (filter-length-mono xs) ... | no _ | no _ = filter-length-mono xs -- If moreover some w ∈ xs has Q w and ¬ P w, the P-filter is strictly shorter. filter-length-strict : (xs : List X){w : X} → w ∈ xs → Q w → ¬ P w → length (filter P? xs) < length (filter Q? xs) filter-length-strict (x ∷ xs) (here refl) qw ¬pw with P? x | Q? x ... | yes pw | _ = ⊥-elim (¬pw pw) ... | no _ | yes _ = s≤s (filter-length-mono xs) ... | no _ | no ¬qw = ⊥-elim (¬qw qw) filter-length-strict (x ∷ xs) (there w∈xs) qw ¬pw with P? x | Q? x ... | yes _ | yes _ = s≤s (filter-length-strict xs w∈xs qw ¬pw) ... | yes px | no ¬qx = ⊥-elim (¬qx (sub px)) ... | no _ | yes _ = <-trans (filter-length-strict xs w∈xs qw ¬pw) (n<1+n _) ... | no _ | no _ = filter-length-strict xs w∈xs qw ¬pw -- From a decidable P and a refutation of (P → Q), recover P and ¬ Q. ¬→-split : {P : Type ℓ₁}{Q : Type ℓ₂} → Dec P → ¬ (P → Q) → P × ¬ Q ¬→-split (yes p) ¬pq = p , λ q → ¬pq (λ _ → q) ¬→-split (no ¬p) ¬pq = ⊥-elim (¬pq (λ p → ⊥-elim (¬p p)))
The construction¶
Fix an algebra 𝑨 equipped with both finiteness witnesses. We abbreviate the
working congruence level as ℓ = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ — the absorbing level of
Setoid.Congruences.Finite, at which the generated (principal) congruences used
for the monolith stay put — and pairs is the list of all index pairs of the
carrier enumeration.
module _ {𝓞 𝓥 : Level}{𝑆 : Signature 𝓞 𝓥}{𝑨 : Algebra {𝑆 = 𝑆} α ρ} (𝑭 : FiniteAlgebra 𝑨) (𝑪 : FiniteCongruences 𝑨) where open FiniteAlgebra 𝑭 open FiniteCongruences 𝑪 open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( Carrier to A ; sym to ≈sym ) ℓ : Level ℓ = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ pairs : List (Fin card × Fin card) pairs = cartesianProduct (allFin card) (allFin card) -- The decision procedure that a decidable congruence relates the i-th and j-th -- enumerated carrier elements, and the count of all such related index pairs. _∈?_ : ((i , j) : Fin card × Fin card)(d : DecCon 𝑨 ℓ) → Dec (ConRel d (enum i) (enum j)) (i , j) ∈? d = proj₂ d (enum i) (enum j) count : DecCon 𝑨 ℓ → ℕ count d = length (filter (_∈? d) pairs) -- Containment *on the enumerated carrier*, and its decision procedure. Naming -- the predicate lets the maximality proof below take the decision as an -- ordinary argument instead of splitting on it with `with`. _⊆ᶜ_ : DecCon 𝑨 ℓ → DecCon 𝑨 ℓ → Type ℓ d ⊆ᶜ e = ∀ i j → ConRel d (enum i) (enum j) → ConRel e (enum i) (enum j) _⊆ᶜ?_ : (d e : DecCon 𝑨 ℓ) → Dec (d ⊆ᶜ e) d ⊆ᶜ? e = all? (λ i → all? (λ j → ((i , j) ∈? d) →-dec ((i , j) ∈? e)))
A congruence contained in another relates no more pairs (count-mono); if the
containment is proper on the enumerated carrier it relates strictly fewer
(count-strict). Both are instances of the generic list lemmas.
count-mono : (d e : DecCon 𝑨 ℓ) → proj₁ d ⊆ proj₁ e → count d ≤ count e count-mono d e d⊆e = filter-length-mono (_∈? d) (_∈? e) (λ {p} → d⊆e) pairs count-strict : (d e : DecCon 𝑨 ℓ)(i j : Fin card) → proj₁ d ⊆ proj₁ e → ConRel e (enum i) (enum j) → ¬ ConRel d (enum i) (enum j) → count d < count e count-strict d e i j d⊆e eij ¬dij = filter-length-strict (_∈? d) (_∈? e) (λ {p} → d⊆e) pairs (∈-cartesianProduct⁺ (∈-allFin i) (∈-allFin j)) eij ¬dij
A relation that holds on every enumerated pair holds everywhere, because the
enumeration is surjective and congruences respect ≈. This lifts a carrier-level
containment to a genuine containment of congruences.
carrier-lift : (R S : Con 𝑨 ℓ) → (∀ i j → proj₁ R (enum i) (enum j) → proj₁ S (enum i) (enum j)) → R ⊆ S carrier-lift (R , pr) (S , ps) h {x} {y} Rxy = Strans (Srefl (≈sym ei≈x)) (Strans Sij (Srefl ej≈y)) where open IsEquivalence (is-equivalence pr) using () renaming (trans to Rtrans) open IsEquivalence (is-equivalence ps) using () renaming (trans to Strans) Rrefl = reflexive pr Srefl = reflexive ps i j : Fin card i = proj₁ (enum-sur x) j = proj₁ (enum-sur y) ei≈x : enum i ≈ x ei≈x = proj₂ (enum-sur x) ej≈y : enum j ≈ y ej≈y = proj₂ (enum-sur y) Rij : R (enum i) (enum j) Rij = Rtrans (Rrefl ei≈x) (Rtrans Rxy (Rrefl (≈sym ej≈y))) Sij : S (enum i) (enum j) Sij = h i j Rij
Now fix a pair a ≢ b. Among the congruences not relating a and b (a finite,
non-empty sublist of cons, non-empty because the diagonal is one) we pick one of
maximum count; count-maximality is ⊆-maximality, by count-mono/count-strict.
-- The diagonal (least) congruence at level ℓ, from Setoid.Congruences.Basic; -- its representative in `cons` witnesses the non-emptiness of `filtered` below. Δ : Con 𝑨 ℓ Δ = 𝟘[ 𝑨 ] {ℓ} module _ (a b : A) (a≢b : ¬ (a ≈ b)) where -- The congruences of `cons` that do not relate a and b. notRel? : (d : DecCon 𝑨 ℓ) → Dec (¬ ConRel d a b) notRel? d = ¬? (proj₂ d a b) a≢bCons : List (DecCon 𝑨 ℓ) a≢bCons = filter notRel? cons -- Of course the diagonal does not relate a and b, so it's in a≢bCons. ¬Δab : ¬ ConRel (witness Δ) a b ¬Δab Δab = a≢b (lower (proj₂ (witness≑ Δ) Δab)) Δ∈a≢bCons : witness Δ ∈ a≢bCons Δ∈a≢bCons = ∈-filter⁺ notRel? (witness∈ Δ) ¬Δab -- The chosen congruence: a maximum-count member of `a≢bCons`. Θ-dec : DecCon 𝑨 ℓ Θ-dec = argmax count (witness Δ) a≢bCons Θ-dec∈filtered : Θ-dec ∈ a≢bCons Θ-dec∈filtered = [ (λ eq → subst (_∈ a≢bCons) (sym eq) Δ∈a≢bCons) , (λ ∈f → ∈f) ]′ (argmax-sel count (witness Δ) a≢bCons) Θ : Con 𝑨 ℓ Θ = proj₁ Θ-dec ¬Θab : ¬ proj₁ Θ a b ¬Θab = proj₂ (∈-filter⁻ notRel? {xs = cons} Θ-dec∈filtered) -- count d ≤ count Θ for every member of `a≢bCons`: Θ has maximum count. Θ-max-count : (d : DecCon 𝑨 ℓ) → d ∈ a≢bCons → count d ≤ count Θ-dec Θ-max-count d d∈f = lookup (f[xs]≤f[argmax] {f = count} (witness Δ) a≢bCons) d∈f
Maximality. If d ∈ a≢bCons contains Θ, then d ⊆ Θ: were the containment
proper on the enumerated carrier, d would out-count Θ, contradicting maximum
count. The witness of properness is extracted from the decidable failure of
carrier-containment.
Θ-max-of : ((δ , δcon) : DecCon 𝑨 ℓ) → (δ , δcon) ∈ a≢bCons → Θ ⊆ δ → Dec ((δ , δcon) ⊆ᶜ Θ-dec) → δ ⊆ Θ Θ-max-of (δ , _) d∈f Θ⊆d (yes h) = carrier-lift δ Θ h Θ-max-of d d∈f Θ⊆d (no ¬h) = ⊥-elim (n≮n (count d) (≤-<-trans (Θ-max-count d d∈f) cΘ<cd)) where -- The two existential witnesses, each extracted once and shared. exi : ∃[ i ] ¬ (∀ j → ConRel d (enum i) (enum j) → ConRel Θ-dec (enum i) (enum j)) exi = ¬∀⟶∃¬ card _ (λ i → all? (λ j → (i , j) ∈? d →-dec (i , j) ∈? Θ-dec)) ¬h i₀ : Fin card i₀ = exi .proj₁ exj : ∃[ j ] ¬ (ConRel d (enum i₀) (enum j) → ConRel Θ-dec (enum i₀) (enum j)) exj = ¬∀⟶∃¬ card _ (λ j → (i₀ , j) ∈? d →-dec (i₀ , j) ∈? Θ-dec) (proj₂ exi) j₀ : Fin card j₀ = exj .proj₁ split : ConRel d (enum i₀) (enum j₀) × ¬ ConRel Θ-dec (enum i₀) (enum j₀) split = ¬→-split ((i₀ , j₀) ∈? d) (exj .proj₂) cΘ<cd : count Θ-dec < count d cΘ<cd = count-strict Θ-dec d i₀ j₀ Θ⊆d (split .proj₁) (split .proj₂) Θ-max : ((δ , δcon) : DecCon 𝑨 ℓ) → (δ , δcon) ∈ a≢bCons → Θ ⊆ δ → δ ⊆ Θ Θ-max d d∈f Θ⊆d = Θ-max-of d d∈f Θ⊆d (d ⊆ᶜ? Θ-dec)
Subdirect irreducibility of the maximal quotient¶
Let Q = 𝑨 ╱ Θ. A congruence of Q is a congruence of 𝑨 containing Θ:
the underlying relation, equivalence proof, and compatibility carry over verbatim
(the quotient's operations are 𝑨's), and a Q-congruence's reflexivity over the
quotient equality Θ is exactly the containment Θ ⊆ ·. Q→A records this.
Q : Algebra α ℓ Q = 𝑨 ╱ Θ Q→A : Con Q ℓ → Con 𝑨 ℓ Q→A (ψ , ψcon) = ψ , mkcon r (is-equivalence ψcon) (is-compatible ψcon) where r : ∀ {x y} → x ≈ y → ψ x y r = reflexive ψcon ∘ reflexive (Θ .proj₂)
The monolith of Q is the principal congruence generated by the single pair
(a , b). It is nonzero (it relates a , b, which are Q-distinct), and it is
the least nonzero congruence: any nonzero ψ of Q corresponds to a congruence
φ ⊇ Θ of 𝑨; choosing its representative d ∈ cons, if d did not relate
a , b then maximality would force φ ⊆ Θ, making ψ zero — so d, hence φ,
hence ψ, relates a , b, i.e. contains the principal congruence.
Rₐᵦ : A → A → Type α Rₐᵦ x y = (x ≡ a) × (y ≡ b) μ : Con Q ℓ μ = Cg {𝑨 = Q} Rₐᵦ μ-nonzero : Nonzero Q μ μ-nonzero below = ¬Θab (below (base (refl , refl))) μ-least : (ψ : Con Q ℓ) → Nonzero Q ψ → μ ⊆ ψ μ-least Ψ@(ψ , ψcon) nz = Cg-least Ψ R⊆ψ where φ : Con 𝑨 ℓ φ = Q→A Ψ Θ⊆φ : Θ ⊆ φ Θ⊆φ = reflexive ψcon -- The representative of φ in `cons`, and its three certificates. rep : ∃[ d ∈ DecCon 𝑨 _ ] (d ∈ cons × φ ≑ d .proj₁) rep = complete φ -- Does d relate a and b? If not, maximality of Θ collapses ψ to zero. ψab-of : ((p , _) : ∃[ (δ , δdec) ∈ DecCon 𝑨 _ ] ((δ , δdec) ∈ cons × φ ≑ δ) ) → Dec (ConRel p a b) → ψ a b ψab-of (_ , _ , _ , d⊆φ ) (yes dab) = d⊆φ dab ψab-of ((δ , δdec) , d∈cons , φ⊆d , d⊆φ ) (no ¬dab) = ⊥-elim (nz (⊆-trans {θ = φ}{φ = δ}{ψ = Θ} φ⊆d (δ⊆Θ Θ⊆δ))) where Θ⊆δ : Θ ⊆ δ Θ⊆δ = ⊆-trans {θ = Θ}{φ = φ}{ψ = δ} Θ⊆φ φ⊆d δ⊆Θ : Θ ⊆ δ → δ ⊆ Θ δ⊆Θ = Θ-max (δ , δdec) (∈-filter⁺ notRel? d∈cons ¬dab) R⊆ψ : ∀ {x y} → Rₐᵦ x y → ψ x y R⊆ψ (refl , refl) = ψab-of rep (proj₂ (proj₁ rep) a b) SI-Q : IsSubdirectlyIrreducible Q SI-Q = (a , b , ¬Θab) , μ , record { mono-nonzero = μ-nonzero ; mono-least = μ-least }
Assembling the representation and the theorem¶
The index is the type of distinct pairs. For each, Θ is the chosen maximal
congruence; the family separates points because, given any pair x , y not
already ≈-equal (decidable!), Θ for (x , y) keeps them apart — so if every
member related them, they would be equal. This is where decidable ≈ closes the
¬¬-gap the design note flags: the meet is exactly the diagonal.
finiteSubdirectSIRep : SubdirectSIRep 𝑨 ℓ (α ⊔ ρ) finiteSubdirectSIRep = I , Θfam , separates , si where I : Type (α ⊔ ρ) I = ∃[ a ] ∃[ b ] ¬ a ≈ b Θfam : I → Con 𝑨 ℓ Θfam (a , b , a≢b) = Θ a b a≢b separates-of : (x y : A) → ((i : I) → proj₁ (Θfam i) x y) → Dec (x ≈ y) → x ≈ y separates-of x y h (yes x≈y) = x≈y separates-of x y h (no x≢y) = ⊥-elim (¬Θab x y x≢y (h (x , y , x≢y))) separates : Separates Θfam separates {x} {y} h = separates-of x y h (x ≟ y) si : (i : I) → IsSubdirectlyIrreducible (𝑨 ╱ Θfam i) si (a , b , a≢b) = SI-Q a b a≢b
Birkhoff's subdirect representation theorem for finite algebras, unconditionally: every finite algebra (with the decidable, complete congruence data above) is a subdirect product of subdirectly irreducible algebras.
finite-Birkhoff : SubdirectlyRepresentable 𝑨 ℓ (α ⊔ ρ) finite-Birkhoff = SIRep→Representable finiteSubdirectSIRep
Non-vacuity: the theorem fires¶
The finiteness interfaces are genuine, computational data — not disguised choice
principles — so they must be exhibited, not merely assumed. The one-element
algebra 𝟏 satisfies both: its bare witness
𝟏-FiniteAlgebra is exhibited in Setoid.Algebras.Finite, and
its congruence-side witness 𝟏-FiniteCongruences (a singleton
complete list) in Setoid.Congruences.Finite. Feeding them to finite-Birkhoff
confirms the theorem fires (here on a degenerate input: the family of distinct
pairs is empty, so the trivial algebra is the subdirect product of the empty
family). A genuinely subdirectly irreducible worked example — one that exercises
the maximal-congruence search — is the natural next addition.
-- The theorem applied: the one-element algebra is subdirectly representable. 𝟏-SubdirectlyRepresentable : {𝓞 𝓥 : Level}{𝑆 : Signature 𝓞 𝓥} → SubdirectlyRepresentable (𝟏 {𝑆 = 𝑆}) (𝓞 ⊔ 𝓥) 0ℓ 𝟏-SubdirectlyRepresentable = finite-Birkhoff 𝟏-FiniteAlgebra 𝟏-FiniteCongruences
-
This is option (b) of the design note
docs/notes/m6-2-subdirect.md, § The three options for a choice-dependent theorem: discharging M6-2's choice parameter by search, where≈is decidable, instead of assuming it. ↩