Quotient Set

definition

Given a Set $A$ and an Equivalence Relation $\sim$ on $A$, the quotient $A/\sim$ of $A$ under $\sim$ is the set of parts of the corresponding Partition (see Partitions Correspond to Equivalence Relations).

Sources: 7 Sketches Definition 1.21; Kittenlab Lecture 9, 11; CTfS Definition 2.6.1.1, Examples 2.6.1.2, 3.1.2.3

There is a canonical Surjection $q:A\twoheadrightarrow A/\sim$ sending each element to its class. Categorically, $A/\sim$ is the Coequalizer of the two projections $R\rightrightarrows A$ from the relation $R\subseteq A\times A$: it is the universal way of “squishing” $\sim$-related elements together (Kittenlab Lecture 11: angles $\theta \sim \theta +2\pi$ give $[0,2\pi )$ or the circle $S^1$). Examples (CTfS): $\mathbb{Z}$ modulo “differ by a multiple of 7” has 7 elements; the clock face $\{0,\dots ,11\}$ is $\mathbb{N}$ (or $\mathbb{Z}$) modulo 12, on which the monoid of elapsed hours acts (Monoid Action). Pushouts in $\mathbf{Set}$ are quotients of disjoint unions.

JuliaLeanHaskell

Docs: FinSets · Limits & colimits — Kittenlab Lecture 9, Lecture 11

# Catlab: quotient of a FinSet by the equivalence generated by pairs = coequalizer
using Catlab
A = FinSet(6)
f = FinFunction([1,2,5], A)    # pairs (1,2),(2,4),(5,6) generate the relation
g = FinFunction([2,4,6], A)
q = coequalizer(f, g)
proj(q)                        # the surjection A → A/∼

-- Mathlib: `Quotient r` for a setoid r, with `Quotient.mk` the canonical surjection
example (α : Type) (r : Setoid α) : Type := Quotient r
#check @Quotient.mk            -- (s : Setoid α) → α → Quotient s
#check @Quotient.sound         -- a ≈ b → ⟦a⟧ = ⟦b⟧
#check @Quotient.lift          -- universal property (maps out of the quotient)

-- Haskell has no quotient types; represent A/∼ by a choice of representatives
import Data.List (nubBy)
quotient :: (a -> a -> Bool) -> [a] -> [a]
quotient eq = nubBy eq
-- the canonical surjection picks the first representative
classOf :: (a -> a -> Bool) -> [a] -> a -> a
classOf eq reps a = head [r | r <- reps, eq r a]