S realises the image of arrow F as a Subobject of Cod<F> — the mono side of the (regular epi, mono) factorisation system pinned in :factorisation. More...

Concept definition

template<typename S, typename F>

concept dedekind::category::IsImageOf = IsArrow<F> && IsSubobject<S, Cod<F>>

dedekind::category::IsArrow

A type that knows its own Domain (A) and Codomain (B), objects it maps between: called at the domain'...

Definition morphism.cppm:168

dedekind::category::IsImageOf

S realises the image of arrow F as a Subobject of Cod<F> — the mono side of the (regular epi,...

Definition image.cppm:153

dedekind::category::IsSubobject

The categorical witness of a monomorphism ι: S ↣ A — a characteristic morphism χ: A → Ω together with...

Definition topoi.cppm:367

Detailed Description

S realises the image of arrow F as a Subobject of Cod<F> — the mono side of the (regular epi, mono) factorisation system pinned in :factorisation.

Structurally, IsImageOf<S, F> is exactly IsArrow<F> && IsSubobject<S, Cod<F>>. The added value over the bare conjunction is the naming: a downstream witness declaring this concept records the intent that its subobject is the image of F (the smallest subobject of Cod<F> through which F factors), not just any subobject of Cod<F>.

The universality (smallest such subobject; canonical epi-mono factorisation F = m ∘ e) is the engineer's honesty obligation, as for IsNNO. C++ concepts cannot quantify over the universal property; they pin the operational signature only.

Categorical context (#718 Slice 2): IsImageOf is the mono leg of the IsFactorisationSystem<C> pair in :factorisation. In a regular category (IsRegularCategory<C>), every arrow's image is a regular subobject and the factorisation is unique up to iso; in Set and every topos this is the canonical (regular epi, mono) factorisation.

Template Parameters

S	The candidate image species (a Subobject of `Cod<F>`).
F	The arrow whose image `S` claims to realise.