Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::algebra::IsMonoid Concept Referenceexport
module dedekind.algebra

Proposition: a set object X whose carrier X::Domain forms a monoid — the set-indexed lift of category::IsMonoid. More...

Concept definition

template<typename X, typename Op std::plus<typename X::Domain>>
concept dedekind::algebra::IsMonoid = IsAlgebraOnSet<X, Op> &&
dedekind::category::IsMonoid<typename X::Domain, Op>
dedekind::algebra::IsAlgebraOnSet
An algebraic set: a Tarski set whose carrier is closed under a family of operations....
Definition universal.cppm:187
dedekind::algebra::IsMonoid
Proposition: a set object X whose carrier X::Domain forms a monoid — the set-indexed lift of category...
Definition monoid.cppm:51
dedekind::category::IsMonoid
A Semigroup with a two-sided Identity element.
Definition total.cppm:584

Detailed Description

Proposition: a set object X whose carrier X::Domain forms a monoid — the set-indexed lift of category::IsMonoid.

X is an ETCS set, its carrier X::Domain satisfies the axiomatic category::IsMonoid<X::Domain, Op>, and IsAlgebraOnSet supplies the carrier discipline (IsLSet roots std::semiregular on X::Domain, IsClosedAlgebra pins strict closure). The Op-defaulted IsAdditiveMonoid / IsMultiplicativeMonoid siblings name the canonical additive / multiplicative witnesses.

Template Parameters
XThe set object (category::IsSet).
OpThe binary operation on X::Domain (defaults to std::plus).