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 𝑨 — 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 --safe 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, up to
mutual containment ≑, a listed one.
Crucially, carrier-finiteness along with decidable setoid equality do not, by
themselves, admit such an enumeration constructively. A congruence is a
Type-valued relation 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → Type ℓ; an arbitrary such relation
on a finite carrier need not be decidable: e.g. on a bare set of two elements, the
relation that collapses the two points iff P holds is a congruence for any
proposition P, and it is ≑-equal to a decidable congruence only iff P is
decidable. So a complete enumeration of congruences-up-to-≑ is strictly stronger
than decidable equality on a finite set; it is exactly the classical content of
"finite algebra" for congruence-lattice purposes.
We therefore take that content as the finiteness interface: a FiniteAlgebra bundles
decidable ≈, a finite enumeration of the carrier, and a finite list of decidable
congruences that is complete up to ≑. Everything downstream is then fully
constructive and computes. Classically every finite algebra furnishes these data, so
finite-Birkhoff is Birkhoff's theorem for finite algebras; the FiniteAlgebra
record is precisely the constructive witness that makes the search go through under
--safe.
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)))
Decidable congruences and the finiteness interface¶
A decidable congruence is a congruence whose membership relation is decidable.
The working congruence level is the absorbing level clv α ρ = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ, at
which the generated (principal) congruences used for the monolith stay put — the
same level discipline as Setoid.Congruences.CompleteLattice.
-- The absorbing congruence level at which everything below is carried out. clv : (α ρ : Level) → Level clv α ρ = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ -- A congruence together with a decision procedure for its membership. DecCon : (𝑨 : Algebra α ρ)(ℓ : Level) → Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ lsuc ℓ) DecCon 𝑨 ℓ = Σ[ θ ∈ Con 𝑨 ℓ ] (∀ x y → Dec (proj₁ θ x y)) ConRel : {𝑨 : Algebra α ρ}{ℓ : Level} → DecCon 𝑨 ℓ → BinaryRel 𝕌[ 𝑨 ] ℓ ConRel (θ , _) = proj₁ θ
The finiteness interface bundles: decidable ≈; a surjective enumeration of the
carrier (used to count related pairs); and a finite, complete list of decidable
congruences (the searchable congruence lattice). See the module header for why
the last field cannot be derived from the first two.
record FiniteAlgebra (𝑨 : Algebra α ρ) : Type (lsuc (clv α ρ)) where open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) field _≟_ : (x y : 𝕌[ 𝑨 ]) → Dec (x ≈ y) card : ℕ enum : Fin card → 𝕌[ 𝑨 ] enum-sur : (x : 𝕌[ 𝑨 ]) → Σ[ i ∈ Fin card ] (enum i ≈ x) cons : List (DecCon 𝑨 (clv α ρ)) complete : (φ : Con 𝑨 (clv α ρ)) → Σ[ d ∈ DecCon 𝑨 (clv α ρ) ] (d ∈ cons) × (φ ≑ proj₁ d) witness : (φ : Con 𝑨 (clv α ρ)) → DecCon 𝑨 (clv α ρ) witness = proj₁ ∘ complete witness∈ : (φ : Con 𝑨 (clv α ρ)) → witness φ ∈ cons witness∈ = proj₁ ∘ proj₂ ∘ complete witness≑ : (φ : Con 𝑨 (clv α ρ)) → φ ≑ proj₁ (witness φ) witness≑ = proj₂ ∘ proj₂ ∘ complete
The construction¶
Fix a finite algebra. We abbreviate the working level as ℓ, and pairs is the
list of all index pairs of the carrier enumeration.
module _ {𝑨 : Algebra α ρ} (𝑭 : FiniteAlgebra 𝑨) where open FiniteAlgebra 𝑭 open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( sym to ≈sym ) ℓ : Level ℓ = clv α ρ 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)
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≢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 with argmax-sel count (witness Δ) a≢bCons ... | inj₁ eq = subst (_∈ a≢bCons) (sym eq) Δ∈a≢bCons ... | inj₂ ∈f = ∈f Θ : 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 : ((d , pd) : DecCon 𝑨 ℓ) → (d , pd) ∈ a≢bCons → Θ ⊆ d → d ⊆ Θ Θ-max d d∈f Θ⊆d with all? (λ i → all? (λ j → ((i , j) ∈? d) →-dec ((i , j) ∈? Θ-dec))) ... | yes h = carrier-lift (proj₁ d) Θ h ... | no ¬h = ⊥-elim (n≮n (count d) (≤-<-trans (Θ-max-count d d∈f) cΘ<cd)) where ¬hj = proj₂ (¬∀⟶∃¬ card _ (λ i → all? (λ j → (i , j) ∈? d →-dec (i , j) ∈? Θ-dec )) ¬h) i₀ j₀ : Fin card i₀ = proj₁ (¬∀⟶∃¬ card _ (λ i → all? (λ j → (i , j) ∈? d →-dec (i , j) ∈? Θ-dec)) ¬h) j₀ = proj₁ (¬∀⟶∃¬ card _ (λ j → (i₀ , j) ∈? d →-dec (i₀ , j) ∈? Θ-dec) ¬hj) ¬impl = proj₂ (¬∀⟶∃¬ card _ (λ j → (i₀ , j) ∈? d →-dec (i₀ , j) ∈? Θ-dec) ¬hj) split = ¬→-split ((i₀ , j₀) ∈? d) ¬impl cΘ<cd : count Θ-dec < count d cΘ<cd = count-strict Θ-dec d i₀ j₀ Θ⊆d (proj₁ split) (proj₂ split)
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 ψ = proj₁ ψ , mkcon r (is-equivalence (proj₂ ψ)) (is-compatible (proj₂ ψ)) where r : ∀ {x y} → x ≈ y → proj₁ ψ x y r e = reflexive (proj₂ ψ) (reflexive (proj₂ Θ) e)
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ₐᵦ : 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → Type α Rₐᵦ x y = (x ≡ a) × (y ≡ b) μ : Con Q ℓ μ = Cg {𝑨 = Q} Rₐᵦ μ-nonzero : Nonzero Q μ μ-nonzero below = ¬Θab (below (base {𝑨 = Q} (refl , refl))) μ-least : (ψ : Con Q ℓ) → Nonzero Q ψ → μ ⊆ ψ μ-least ψ nz = Cg-least {𝑨 = Q} {R = Rₐᵦ} ψ R⊆ψ where φ : Con 𝑨 ℓ φ = Q→A ψ Θ⊆φ : Θ ⊆ φ Θ⊆φ = reflexive (proj₂ ψ) ψab : proj₁ ψ a b ψab with complete φ ... | d , d∈cons , φ⊆d , d⊆φ with proj₂ d a b ... | yes dab = d⊆φ dab ... | no ¬dab = ⊥-elim (nz (⊆-trans {θ = φ}{φ = proj₁ d}{ψ = Θ} φ⊆d (Θ-max d (∈-filter⁺ notRel? d∈cons ¬dab) (⊆-trans {θ = Θ}{φ = φ}{ψ = proj₁ d} Θ⊆φ φ⊆d)))) R⊆ψ : ∀ {x y} → Rₐᵦ x y → proj₁ ψ x y R⊆ψ (refl , refl) = ψab 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 : Separates Θfam separates {x}{y} h with x ≟ y ... | yes x≈y = x≈y ... | no x≢y = ⊥-elim (¬Θab x y x≢y (h (x , y , 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 interface is inhabited¶
The FiniteAlgebra record is genuine, computational data — not a disguised choice
principle — so it must be exhibited, not merely assumed. The one-element algebra
over any signature satisfies it: its carrier is ⊤, decidable equality is trivial,
and its only congruence (up to ≑) is the diagonal, so the complete list is a
singleton. This confirms finite-Birkhoff 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 one-element algebra over the signature 𝑆. 𝟏 : Algebra 0ℓ 0ℓ 𝟏 .Domain = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ ; isEquivalence = record { refl = tt ; sym = λ _ → tt ; trans = λ _ _ → tt } } 𝟏 .Interp ⟨$⟩ _ = tt 𝟏 .Interp .cong _ = tt -- Its sole decidable congruence: the all-relation (= the diagonal on a point). 𝟏-Δ : DecCon 𝟏 (clv 0ℓ 0ℓ) 𝟏-Δ = ((λ _ _ → Lift (clv 0ℓ 0ℓ) ⊤) , mkcon (λ _ → lift tt) (record { refl = lift tt ; sym = λ _ → lift tt ; trans = λ _ _ → lift tt }) (λ _ _ → lift tt)) , (λ _ _ → yes (lift tt)) 𝟏-FiniteAlgebra : FiniteAlgebra 𝟏 𝟏-FiniteAlgebra = record { _≟_ = λ _ _ → yes tt ; card = 1 ; enum = λ _ → tt ; enum-sur = λ _ → zero , tt ; cons = 𝟏-Δ ∷ [] ; complete = λ φ → 𝟏-Δ , here refl , (λ _ → lift tt) , (λ _ → reflexive (proj₂ φ) tt) } -- The theorem applied: the one-element algebra is subdirectly representable. 𝟏-SubdirectlyRepresentable : SubdirectlyRepresentable 𝟏 (clv 0ℓ 0ℓ) 0ℓ 𝟏-SubdirectlyRepresentable = finite-Birkhoff 𝟏-FiniteAlgebra
-
This is option (b) of the design note
docs/notes/m6-2-subdirect.md. ↩