Examples.Setoid.FiniteQuotient¶
Worked example: a finite quotient of (ℕ, +, 0)¶
This is the Examples.Setoid.FiniteQuotient module of the Agda Universal Algebra Library.
The quotient of an algebra by a congruence is one of the central constructions of
universal algebra; in the Setoid development it is the operation _╱_
of Setoid.Congruences. This module takes the quotient of the commutative monoid
(ℕ, +, 0) modulo the parity congruence a ∼ b ⟺ a % 2 ≡ b % 2.
The result is a genuinely finite quotient: it has exactly two congruence classes,
even and odd, and its induced operation is addition modulo 2 — i.e. the two-element
group ℤ/2ℤ.
(Incidentally, the monoid (ℕ, +, 0) that we use here is the same one that appears in
Examples.Classical.CommutativeMonoid; it is rebuilt here directly over
Sig-Monoid.)
The monoid (ℕ, +, 0) over Sig-Monoid¶
We author this algebra by hand, matching the ⟨ Sig-Monoid ⟩ carrier as (o , args) in
the Interp field. The pair constructor _,_ now comes straight from the
Setoid.Algebras barrel (re-exported via Setoid.Algebras.Basic), so no separate
Data.Product import is needed — and the (∙-Op , args) match no longer trips the
misleading "∙-Op is not a constructor of the datatype … Σ" error.
ℕ+-monoid : Algebra 0ℓ 0ℓ ℕ+-monoid = record { Domain = setoid ℕ ; Interp = interp } where interp : ⟨ Sig-Monoid ⟩ (setoid ℕ) ⟶ setoid ℕ interp ⟨$⟩ (∙-Op , args) = args 0F + args 1F interp ⟨$⟩ (ε-Op , _) = 0 interp .≈cong {∙-Op , _} {.∙-Op , _} (refl , args≈) = cong₂ _+_ (args≈ 0F) (args≈ 1F) interp .≈cong {ε-Op , _} {.ε-Op , _} (refl , _) = refl
Alternatively, we can use the mkAlgebraₚ smart constructor to make
the definition slightly less tedious.
First define interpretations of the operations and the congruence proof that the operations respect equality.
-- the operations of the monoid (ℕ, +, 0), shared by the smart-constructor -- build below and by the isomorphism proof f : ∀ o → Op (ArityOf Sig-Monoid o) ℕ f ∙-Op args = args 0F + args 1F f ε-Op _ = 0 cong-f : ∀ o → {u v : ArityOf Sig-Monoid o → ℕ} → (∀ i → u i ≡ v i) → f o u ≡ f o v cong-f ∙-Op ui≡vi = cong₂ _+_ (ui≡vi 0F) (ui≡vi 1F) cong-f ε-Op _ = refl
Constructing the algebra with mkAlgebraₚ results in an algebra that is isomorphic
to the algebra ℕ+-monoid defined above.
ℕ+-monoid-≅ : ℕ+-monoid ≅ mkAlgebraₚ ℕ f cong-f ℕ+-monoid-≅ = ≅-mkAlgebra f cong-f λ { ∙-Op _ → refl ; ε-Op _ → refl }
Both algebras carry (ℕ, ≡) and interpret each operation symbol identically,
so the identity map is a homomorphism in each direction and the two round
trips hold on the nose.
The parity congruence¶
Two naturals are related when they have the same remainder modulo 2. This is the
kernel of _% 2, hence an equivalence; compatibility with + is the standard fact
that remainder distributes over addition (%-distribˡ-+), and
compatibility with the nullary 0 is immediate.
θ : ℕ → ℕ → Type θ a b = a % 2 ≡ b % 2 θ-isEquiv : IsEquivalence θ θ-isEquiv = record { refl = refl ; sym = sym ; trans = trans } -- + preserves parity: (u₀ + u₁) % 2 ≡ (v₀ + v₁) % 2 from uᵢ % 2 ≡ vᵢ % 2. θ-compatible : ℕ+-monoid ∣≈ θ θ-compatible ∙-Op {u} {v} h = trans (%-distribˡ-+ (u 0F) (u 1F) 2) (trans (cong₂ (λ r s → (r + s) % 2) (h 0F) (h 1F)) (sym (%-distribˡ-+ (v 0F) (v 1F) 2))) θ-compatible ε-Op _ = refl parity : Con ℕ+-monoid 0ℓ parity = θ , record { reflexive = cong (_% 2) ; is-equivalence = θ-isEquiv ; is-compatible = θ-compatible }
The quotient (ℕ, +, 0) ╱ parity ≅ ℤ/2ℤ¶
The carrier of the quotient is still ℕ, but its equality is parity,
so distinct naturals of the same parity become equal. We exhibit the two classes,
the failure of cross-class identification, and the modular addition 1 + 1 ≈ 0.
ℤ/2 : Algebra 0ℓ 0ℓ ℤ/2 = ℕ+-monoid ╱ parity open Setoid 𝔻[ ℤ/2 ] using ( _≈_ ) -- every even number collapses to 0, every odd number to 1 2≈0 : 2 ≈ 0 2≈0 = refl 4≈0 : 4 ≈ 0 4≈0 = refl 3≈1 : 3 ≈ 1 3≈1 = refl -- the two classes are genuinely distinct 0≉1 : ¬ (0 ≈ 1) 0≉1 () -- the induced operation is addition modulo 2: 1 + 1 ≈ 0 1+1≈0 : (1 + 1) ≈ 0 1+1≈0 = refl