Setoid.Congruences.Generation¶
The Congruence Generated by a Relation¶
This is the Setoid.Congruences.Generation module of the Agda Universal Algebra Library.
The Setoid.Congruences.Lattice module made Con 𝑨 a meet-semilattice
under containment, with meet given by intersection (the tractable half of the
congruence lattice). The join requires more work; it is the least congruence
containing the union; that is, the congruence generated by the union. This
module supplies the subsidiary result on which the join rests: for any binary
relation R on the carrier of 𝑨 there is a least congruence Cg R containing R.
We build Cg R as the inductively-defined closure Gen R of R under the
congruence-forming rules: it contains R (base), it contains the setoid equality
_≈_ (rfl), and it is closed under symmetry, transitivity, and the basic
operations (symmetric, transitive, compatible). The following two facts make this the
generated congruence and constitute the Congruence Generation Theorem:
Cg Ris a congruence containingR(so it is an upper bound ofR); and- every congruence
ψcontainingRcontainsCg R(so it is the least upper bound) — this isCg-least, proved by induction onGen.
From Cg we obtain the join θ ∨ φ = Cg(θ ∪ φ) and prove it is the least
upper bound of θ and φ in the containment order. Because the closure quantifies
over the operations and the carrier, Gen R lands at level 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ
(not ℓ); assembling this into a single-level Lattice/CompleteLattice bundle —
where that level is absorbed — is the remaining step of the congruence-lattice work
and is deferred to a follow-up.
Inductive Generation of a Congruence¶
Fix an algebra 𝑨 and a binary relation R on its carrier. Gen R is the
smallest relation containing R that is reflexive over _≈_, symmetric,
transitive, and compatible with every basic operation. The closure quantifies over
the operation symbols (𝓞), their arities (𝓥), and the carrier (α, ρ), so it
inhabits BinaryRel 𝕌[ 𝑨 ] (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ), one level above its input R.
module _ {𝑆 : Signature 𝓞 𝓥} {𝑨 : Algebra α ρ} where open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( refl to ≈refl ) data Gen (R : BinaryRel 𝕌[ 𝑨 ] ℓ) : BinaryRel 𝕌[ 𝑨 ] (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ) where base : R ⊆ Gen R rfl : {x y : 𝕌[ 𝑨 ]} → x ≈ y → Gen R x y symmetric : {x y : 𝕌[ 𝑨 ]} → Gen R x y → Gen R y x transitive : {x y z : 𝕌[ 𝑨 ]} → Gen R x y → Gen R y z → Gen R x z compatible : (f : OperationSymbolsOf 𝑆) {u v : ArityOf 𝑆 f → 𝕌[ 𝑨 ]} → (∀ i → Gen R (u i) (v i)) → Gen R ((f ^ 𝑨) u) ((f ^ 𝑨) v) Cg : (R : BinaryRel 𝕌[ 𝑨 ] ℓ) → Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ) Cg R = Gen R , mkcon rfl g-isEquivalence compatible where open IsEquivalence using (refl ; sym ; trans ) g-isEquivalence : IsEquivalence (Gen R) g-isEquivalence .refl = rfl ≈refl g-isEquivalence .sym = symmetric g-isEquivalence .trans = transitive
The Congruence Generation Theorem¶
R is contained in Cg R (the base constructor), and Cg R is the least
congruence with that property: any congruence ψ containing R already contains
Gen R. The latter is proved by induction on the derivation of Gen R x y,
turning each closure rule into the corresponding congruence law of ψ. Note ψ may
live at any relation level ℓ′, so this is a genuinely heterogeneous statement.
Cg-incl : (R : BinaryRel 𝕌[ 𝑨 ] ℓ) → R ⊆ Gen R Cg-incl R = base Cg-least : {R : BinaryRel 𝕌[ 𝑨 ] ℓ} (ψ : Con 𝑨 ℓ′) → R ⊆ proj₁ ψ → Gen R ⊆ proj₁ ψ Cg-least ψ R⊆ψ (base r) = R⊆ψ r Cg-least (_ , ψcon) R⊆ψ (rfl e) = reflexive ψcon e Cg-least ψ R⊆ψ (symmetric p) = IsEquivalence.sym (is-equivalence (ψ .proj₂)) (Cg-least ψ R⊆ψ p) Cg-least ψ R⊆ψ (transitive p q) = IsEquivalence.trans (is-equivalence (proj₂ ψ)) (Cg-least ψ R⊆ψ p) (Cg-least ψ R⊆ψ q) Cg-least ψ R⊆ψ (compatible f h) = is-compatible (proj₂ ψ) f (λ i → Cg-least ψ R⊆ψ (h i))
Monotonicity follows immediately: if R is contained in S then Cg R is
contained in Cg S (take ψ = Cg S, which contains S hence R).
Cg-mono : {R : BinaryRel 𝕌[ 𝑨 ] ℓ} {S : BinaryRel 𝕌[ 𝑨 ] ℓ′} → R ⊆ S → Gen R ⊆ Gen S Cg-mono {S = S} R⊆S = Cg-least (Cg S) (λ r → base (R⊆S r))
The Join of Two Congruences¶
For congruences θ φ : Con 𝑨 the union θ ∪ φ of their underlying relations need
not be transitive, so we take the join to be the congruence it generates,
θ ∨ φ = Cg(θ ∪ φ). We record the order facts using a heterogeneous containment
_⊑_ (which coincides definitionally with the homogeneous _≤_ of
Setoid.Congruences.Lattice when the two levels agree), because the
join sits at the higher level 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ.
-- Heterogeneous containment of congruences. _⊑_ : Con 𝑨 ℓ → Con 𝑨 ℓ′ → Type (α ⊔ ℓ ⊔ ℓ′) θ ⊑ φ = proj₁ θ ⊆ proj₁ φ infix 4 _⊑_ -- The union of the underlying relations of two congruences. _∪ᵣ_ : Con 𝑨 ℓ → Con 𝑨 ℓ → BinaryRel 𝕌[ 𝑨 ] ℓ (θ ∪ᵣ φ) x y = proj₁ θ x y ⊎ proj₁ φ x y infixr 6 _∪ᵣ_ _∨_ : Con 𝑨 ℓ → Con 𝑨 ℓ → Con 𝑨 (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ) θ ∨ φ = Cg (θ ∪ᵣ φ) infixr 6 _∨_
The join is the least upper bound of its arguments: each argument is below it
(base ∘ inj₁, base ∘ inj₂), and it is below any common upper bound (by
Cg-least, since the union is below any congruence above both arguments).
∨-upperˡ : (θ φ : Con 𝑨 ℓ) → θ ⊑ (θ ∨ φ) ∨-upperˡ _ _ p = base (inj₁ p) ∨-upperʳ : (θ φ : Con 𝑨 ℓ) → φ ⊑ (θ ∨ φ) ∨-upperʳ _ _ q = base (inj₂ q) ∨-least : (θ φ : Con 𝑨 ℓ) (ψ : Con 𝑨 ℓ′) → θ ⊑ ψ → φ ⊑ ψ → (θ ∨ φ) ⊑ ψ ∨-least _ _ ψ θ⊑ψ φ⊑ψ = Cg-least ψ (λ {x y} → [ θ⊑ψ , φ⊑ψ ])
The principal (single-pair) relation¶
For two carrier elements a, b of an algebra, ❴ a , b ❵ is the
relation that relates exactly a to b. Its generated congruence Cg ❴ a , b ❵ is
the principal congruence collapsing the one pair.
module principal {𝑆 : Signature 𝓞 𝓥} (𝑨 : Algebra {𝑆 = 𝑆} α ρ) where data ❴_,_❵ (a b : 𝕌[ 𝑨 ]) : BinaryRel 𝕌[ 𝑨 ] α where pᵣ : ❴ a , b ❵ a b open ❴_,_❵