dedekind::category::IsKernelPair Concept Reference

The pullback of an arrow F against itself — the equivalence relation "have the same F-image" on Dom<F>. More...

Concept definition

template<typename P, typename F>
concept dedekind::category::IsKernelPair =  IsPullback<P, F, F>

Detailed Description

The pullback of an arrow F against itself — the equivalence relation "have the same F-image" on Dom<F>.

For an arrow F : A → B, the kernel pair is the pullback A ×_B A: pairs (x, x') ∈ A × A such that F(x) = F(x'). Categorically this is the kernel (in the equivalence-relation sense) of F, treated as an equivalence-relation object via the pullback.

Structurally, IsKernelPair<P, F> is exactly IsPullback<P, F, F>; the alias gives the kernel-pair role its textbook name at the concept level so downstream witnesses can refer to it by intent.

The image of an arrow F is the coequalizer of F's kernel pair (the canonical epi-mono factorisation of F), which is the structural payoff this naming sets up. The kernel pair's projections π_1, π_2 form an IsParallelPair (below) on Dom<F>; the coequalizer-of-parallel-pair half awaits an IsQuotient surface (see the partition header).

Template Parameters

P	The candidate kernel-pair species (a Subobject of Dom<F> × Dom<F>).
F	The arrow whose kernel pair is being named.