dedekind::category::IsCoequalizer Concept Reference

The categorical dual of IsEqualizer — a Quotient of Cod<F> equating two parallel arrows F, G. More...

Concept definition

template<typename Q, typename F, typename G>
concept dedekind::category::IsCoequalizer =  IsParallelPair<F, G> && IsQuotient<Q, Cod<F>>

Detailed Description

The categorical dual of IsEqualizer — a Quotient of Cod<F> equating two parallel arrows F, G.

For a parallel pair F, G : A → B, the coequalizer is the smallest quotient Q of B together with a regular epi q : B → Q satisfying the equalising condition

q ∘ F = q ∘ G (equalising)

universal among such: any other arrow B → X equating F and G factors uniquely through q. In a topos the coequalizer is the regular-epi onto the quotient by the smallest equivalence relation containing the image of the parallel pair.

Where IsEqualizer pins the structural shape via IsSubobject<E, Dom<F>>, the dual IsCoequalizer pins it via IsQuotient<Q, Cod<F>> (in :topoi as the dual to IsSubobject). The universal property's $\forall$ — existence and uniqueness of the unique factoring map for any arrow that equates the kernel relation, plus the equalising condition q∘F = q∘G — is the engineer's honesty obligation, as for IsNNO.

image__Image_as_coequalizer

For a single arrow F : A → B with kernel pair π_1, π_2 : P ⇒ A (P satisfying IsKernelPair<P, F> in :pullback), the image of F is the coequalizer of (π_1, π_2) — the canonical epi-mono factorisation

A → Im(F) → B

read off as "collapse the equivalence relation 'same F-image'". The mono side Im(F) ↪ B is what IsImageOf above pins; the quotient side A ↠ A/~ is what IsCoequalizer here pins (with F = π_1, G = π_2 over the kernel pair).

Template Parameters

Q	The candidate coequalizer species (a Quotient of Cod<F>).
F	The first parallel arrow F : A → B.
G	The second parallel arrow G : A → B.