Image classifier for a retractable arrow: y is in the image iff the retract fires at y.
More...
Public Types | |
| using | Domain = Cod<F> |
| using | Codomain = bool |
| using | Domain = Cod<F> |
| using | Codomain = bool |
Public Member Functions | |
| constexpr bool | operator() (const Cod< F > &y) const |
| constexpr bool | operator() (const Cod< F > &) const |
Public Attributes | |
| F | f |
Detailed Description
requires IsRetractableArrow<F> && (!IsIsomorphism<F>) && requires(const std::remove_cvref_t<F>& cf, const Cod<F>& y) { { retract(cf)(y) } -> std::same_as<std::optional<Dom<F>>>; }
struct dedekind::category::ImageChi< F >
Image classifier for a retractable arrow: y is in the image iff the retract fires at y.
Image classifier for an isomorphism: the image is the whole codomain, so membership is decidably true.
The decidability seam. Where the primary ImageChi answers Ternary::Unknown (the \(\exists x. F(x)=y\) is Rice-undecidable on a general arrow), a IsRetractableArrow F discharges the existential as a lookup: \(y \in \mathrm{im}(F) \iff \mathrm{retract}(F)(y)\) has a value. The Codomain is therefore bool (not Ternary), so Subobject<Cod<F>, ImageChi<F>>::logic_species is Boole and the image is HasDecidableMembership — the arrow's factorization class (retractable vs. merely an arrow) becomes the relation's decidability class, read off at compile time. Isos route to their own (tighter) spec below, excluded here by !IsIsomorphism so dispatch stays unambiguous; a general monic-but-not-retractable arrow keeps the primary Ternary classifier.
An iso \(f:A\to B\) is surjective, so every y in B is in im(f) (equivalently retract(f)(y) is always Some for the total inverse). Codomain is bool, hence Boole / HasDecidableMembership. This is the branch-on-iso the arrow hierarchy takes so that an iso never routes through the monic/retract path (which is excluded here by !IsIsomorphism above): IsIsomorphism ⟹ IsRetractableArrow via the blanket IsoRetract, but the iso gets its own tighter, always-true classifier rather than the has_value lookup.
The documentation for this struct was generated from the following file:
- src/main/modules/dedekind/category/image.cppm
