(Regular epi, mono) factorisation system theory — the categorical context for the image-as-coequalizer-of-kernel-pair theorem narrated in :image (#718 Slice 1).
More...
Classes | |
| struct | dedekind::category::_factorisation_upgrade_witnesses::exact_category_witness |
| Category-shape-tagged toy carrier for upgrade-chain witnesses. More... | |
Namespaces | |
| namespace | dedekind::category |
Concepts | |
| concept | dedekind::category::IsRegularEpi |
An arrow E is a regular epi when it is an epi and registered as the coequalizer of some parallel pair. | |
| concept | dedekind::category::IsRegularMono |
Dual of IsRegularEpi: an arrow M is a regular mono when it is a mono and the equalizer of some parallel pair. | |
| concept | dedekind::category::IsFactorisationSystem |
Category C admits the canonical (regular epi, mono) factorisation system. Form-chain row 6 (#718). | |
| concept | dedekind::category::IsRegularCategory |
Category C satisfies the regular-category axioms. Pinned for Set and (transitively) every topos. | |
| concept | dedekind::category::IsExactCategory |
Category C satisfies the exact-category axioms. Sollbruchstelle landing site. | |
Variables | |
| template<typename E> | |
| constexpr bool | dedekind::category::is_regular_epi_v = false |
User-declared witness: E is a regular epi (the coequalizer of some parallel pair). | |
| template<typename M> | |
| constexpr bool | dedekind::category::is_regular_mono_v = false |
User-declared witness: M is a regular mono (the equalizer of some parallel pair). Dual to is_regular_epi_v. | |
| template<typename C> | |
| constexpr bool | dedekind::category::is_factorisation_system_v = false |
User-declared witness: category C admits a (regular epi, mono) factorisation system — every arrow f of C factors as f = m ∘ e with e a regular epi and m a mono, uniquely up to iso. | |
| template<typename C> | |
| constexpr bool | dedekind::category::is_regular_category_v = false |
User-declared witness: C is a regular category — has finite limits, kernel pairs and coequalizers of kernel pairs, and regular epis are stable under pullback. | |
| template<typename C> | |
| constexpr bool | dedekind::category::is_factorisation_system_v< C > = true |
Every regular category admits the (regular epi, mono) factorisation system (Wikipedia: regular category). The upgrade fires automatically; downstream callers need only register is_regular_category_v. | |
| template<typename C> | |
| constexpr bool | dedekind::category::is_exact_category_v = false |
User-declared witness: C is an exact category — a regular category in which every equivalence relation is the kernel pair of some arrow (every equivalence relation is effective). | |
| template<typename C> | |
| constexpr bool | dedekind::category::is_regular_category_v< C > = true |
| Every exact category is a regular category (Borceux vol 2 §2.6); the upgrade fires automatically. | |
| template<typename T> | |
| constexpr bool | dedekind::category::is_regular_epi_v< Identity< T > > = true |
| template<typename T> | |
| constexpr bool | dedekind::category::is_regular_mono_v< Identity< T > > = true |
| template<typename E> | |
| constexpr bool | dedekind::category::is_epic_arrow_v< E > = true |
| template<typename M> | |
| constexpr bool | dedekind::category::is_monic_arrow_v< M > = true |
| template<> | |
| constexpr bool | dedekind::category::is_exact_category_v< _factorisation_upgrade_witnesses::exact_category_witness > = true |
Detailed Description
(Regular epi, mono) factorisation system theory — the categorical context for the image-as-coequalizer-of-kernel-pair theorem narrated in :image (#718 Slice 1).
@partition :factorisation
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
factorisation__Motivation
In a category C with finite limits, an arrow e is a regular epi when it is the coequalizer of some parallel pair; dually, m is a regular mono when it is the equalizer of some parallel pair. When every arrow of C factors uniquely (up to iso) as m ∘ e with e a regular epi and m a mono, the pair (regular epis, monos) constitutes a factorisation system on C, and C is called a regular category. When in addition every equivalence relation is the kernel pair of some arrow (i.e. every equivalence relation is effective), C is called exact.
Set is exact, and every (elementary) topos is exact, so every topos is regular and admits the canonical (regular epi, mono) factorisation — this is the categorical context that makes the image-as-coequalizer-of-kernel-pair theorem (narrated in :image) the right structural payoff for the quotient categorification.
factorisation__Form_chain_position
Row 4–8 of the quotient Form-chain (#718):
IsKernelPair (row 3, in :pullback) ↓ + coequalizer-of-parallel-pair role IsRegularEpi (row 4) ↓ + dual on the mono side IsRegularMono (row 5) ↓ + paired into a factorisation IsFactorisationSystem (row 6) ↓ + universally in a category IsRegularCategory (row 7 — Set, every topos) ↓ + every equivalence relation is effective IsExactCategory (row 8 — Set is exact; every topos is exact)
factorisation__Structural_vs_Universal
The concepts here pin the operational shape (an arrow is a regular epi when it is the coequalizer of some parallel pair) but not the universal property's $\forall $ — existence and uniqueness of the factorisation map. C++ concepts cannot quantify over the universal property; downstream witnesses opt-in via the variable-trait registry to record the intent that their carrier realises the structural role. This is the IsNNO honesty pattern the project uses for every universal-property concept.
factorisation__Layering
Upstream-of-everything-numeric. Lives in :category alongside :image and :pullback. Carrier witnesses register downstream where the carriers are available. Sister to :morphism (which already names IsEpicArrow / IsMonicArrow at the structural-shape level); :factorisation refines those by naming the regular variants (coequalizer / equalizer of a parallel pair, not just any epi / mono).
- Note
- "In a regular category, the regular-epimorphisms and the monomorphisms form a factorization system." — Borceux, Handbook of Categorical Algebra, vol 2, §2.1. (See also Mac Lane, CWM, Ex §IV.6; the (regular epi, mono) factorisation is the canonical factorisation system in Set and in any topos.)
