dedekind::algebra::EmbedsAsSubalgebra Concept Reference

The Birkhoff S leg as an arrow: a monic homomorphism, i.e. a structure-preserving embedding whose image is a subalgebra. More...

Concept definition

template<typename Arrow, typename S typename detail_universal::default_signatures<Arrow>::source, typename T typename detail_universal::default_signatures<Arrow>::target>
concept dedekind::algebra::EmbedsAsSubalgebra = 
    IsHomomorphism<Arrow, S, T> && dedekind::category::IsMonicArrow<Arrow> &&
    std::semiregular<typename std::remove_cvref_t<Arrow>::Domain> &&
    std::semiregular<typename std::remove_cvref_t<Arrow>::Codomain>

Detailed Description

The Birkhoff S leg as an arrow: a monic homomorphism, i.e. a structure-preserving embedding whose image is a subalgebra.

The monic dual of IsQuotientMorphism (the H leg): where a quotient morphism is a surjective homomorphism, a subalgebra embedding is an injective one. Together they are the two directions of the HSP legs on arrows — EmbedsAsSubalgebra for \(\mathbb{Q}\hookrightarrow\mathbb{R}\) and \(\mathbb{R}\hookrightarrow\mathbb{C}\), IsQuotientMorphism for \(\mathbb{R}\twoheadrightarrow\mathbb{C} = \mathbb{R}[i]/(i^2+1)\).

The property is a conjunction of exactly two legs plus a carrier shape:

• IsHomomorphism — structure-preserving (preserves the F of an \((A,F)\) algebra: \(+,\cdot,0,1\)). This already implies IsArrow, so the \(\text{Domain}\to\text{Codomain}\) shape is not restated.
• IsMonicArrow — injective, so the image is a genuine subalgebra (Domain = the subalgebra carrier, Codomain = the ambient algebra).
• Domain / Codomain are std::semiregular. The embedding is the pointwise arrow (f(q) takes a carrier element and embed(a+b)==embed(a)+embed(b) is an element-level law), so the carriers are values (Rule 1) — the Jlt value-semantics half that IsLSet roots on a carrier — not IsAlgebraOnSet, which would make the arrow a \(\text{Set}\to\text{Set}\) map and break the hom law. The ambient algebra structure (IsAlgebraOnSet on 𝔸<Domain>) is witnessed at the declaration site, where the operations are in scope.

Note

This concept classifies the arrow (the inclusion mono itself). Its graph \(\Gamma = \operatorname{graph}(\text{embed}) \subseteq A \times B\) is a separate object: a functional, monic IsRelation on the product that reifies the arrow relationally — not the inclusion subobject of the codomain, and not an IsShapedFunctor (a field homomorphism preserves operations, not composition of arrows between categories; \(\mathbb{Q},\mathbb{R}\) are objects, not categories).

Like both HSP siblings the monic/hom legs are opt-in (is_monic_arrow_v / category::is_homomorphism declarations); the honest discipline is to pin them with computed witnesses at the declaration site (the embedding of a genuine carrier can be run: embed(a+b)==embed(a)+embed(b), embed injective).