dedekind::algebra::IsGrothendieckGroup Concept Reference

G is the Grothendieck group of the commutative monoid M — the free abelian group on M, equivalently the left adjoint of the forgetful functor Ab → CMon applied at M. More...

Concept definition

template<typename G, typename M>
concept dedekind::algebra::IsGrothendieckGroup = 
    dedekind::category::IsAbelianGroup<G, std::plus<G>> &&
    dedekind::category::IsCommutativeMonoid<M, std::plus<M>> &&
    is_grothendieck_group_v<G, M>

Detailed Description

G is the Grothendieck group of the commutative monoid M — the free abelian group on M, equivalently the left adjoint of the forgetful functor Ab → CMon applied at M.

Composes:

• The structural abelian-group claim ( IsAbelianGroup<G, std::plus<G>>): G must actually be an abelian group.
• The structural commutative-monoid claim ( IsCommutativeMonoid<M, std::plus<M>>): M must actually be a commutative monoid.
• The opt-in trait is_grothendieck_group_v<G, M>: the engineer's claim that this specific pair forms a Grothendieck- completion adjunction at the monoid M.

Universal-property content (existence + uniqueness of the extension φ̂) is the engineer's honesty obligation. Operational realisation: the closure-forcing operator M - M → G implements the Grothendieck construction at the operator level; the project's Cardinality - Cardinality → SignedCardinality is the canonical instance.

Template Parameters

G	The carrier type claimed to be the Grothendieck group.
M	The commutative monoid being completed.