dedekind::category::SubobjectInclusion< S > Struct Template Reference

inclusion_arrow(S): the inclusion \(\iota_S : S \hookrightarrow \mathrm{Domain}(S)\) of a subobject as an arrow (Domain = S::Member, Codomain = S::Domain, through S's own ι), so it can be a leg of a cospan. A monomorphism by definition. More...

Collaboration diagram for dedekind::category::SubobjectInclusion< S >:

Public Types
using	Domain = typename S::Member
using	Codomain = typename S::Domain
using	is_monic_arrow_tag = void
	Structural monic opt-in, by tag: a variable-template partial specialisation would not cross the module boundary (cf. is_monic_arrow_v).

Public Member Functions
constexpr Codomain	operator() (const Domain &m) const

Public Attributes
S	subobject

Detailed Description

template<typename S>
requires IsSubobject<S, typename S::Domain>
struct dedekind::category::SubobjectInclusion< S >

inclusion_arrow(S): the inclusion \(\iota_S : S \hookrightarrow \mathrm{Domain}(S)\) of a subobject as an arrow (Domain = S::Member, Codomain = S::Domain, through S's own ι), so it can be a leg of a cospan. A monomorphism by definition.

Meet = pullback, join = pushout in Sub(U)

In the thin category of subobjects of one ambient, the meet A ∧ B is the pullback of the inclusions A ↪ U ↩ B and the join their pushout (#881). The reading needs the apex's member shape and its legs, so it is a view over the apex, owning nothing: it evaluates through the apex's own χ. Any carrier with the subobject surface takes it: the set objects of sets over their meet and join nodes, the run lists of :runs over their reduced intersection and union.

Note

FIXME(#887): every subobject exposes ι as a member function, not as a nameable arrow; this reifies it until the inclusion is intrinsic.

---

The documentation for this struct was generated from the following file:

• src/main/modules/dedekind/category/pullback.cppm