An algebraic set: a Tarski set whose carrier is closed under a family of operations. This is the Ddk = Trsk ∩ Alg layer, spelt out as its two conjuncts. More...

Concept definition

template<typename X, typename... Ops>
concept dedekind::algebra::IsAlgebraOnSet =  dedekind::category::IsLSet<X> &&
                         IsClosedAlgebra<typename X::Domain, Ops...>

Detailed Description

An algebraic set: a Tarski set whose carrier is closed under a family of operations. This is the Ddk = Trsk ∩ Alg layer, spelt out as its two conjuncts.

The parameters name the three pieces of an (A, F) algebra carried on a set object:

X — the set object (HAS-A its carrier via X::Domain).
X::Domain — the carrier element type (the A in BS §I.1's (A, F)).
Ops... — element-level operations on the carrier (the F). Set-level ops (complement, |, &) live on X itself, not in Ops, so they are never confused with F.

The definition factors as Ddk = Trsk ∩ Alg:

IsLSet<X> is the Trsk (set) half: X is a Goguen L-set (a subobject of a regular carrier with χ into a named chain), not merely an IsArrow — Kleene-valued sets qualify; the ETCS specialisation IsSet is not required — and, since Trsk = Jlt ∩ Set, IsLSet roots std::semiregular on X::Domain (the Jlt value-semantics half).
IsClosedAlgebra is the Alg half: the operations close on the carrier. No value constraint is re-pinned here (std::semiregular comes from IsLSet), so it is asserted exactly once. IsClosedUnderEither admits exactly the two operation shapes the carrier uses: a unary Op is already an endomap A → A, and a binary Op A×A → A corresponds to endomorphisms once one argument is fixed (currying). Neither shape is an arbitrary n-ary API.

Template Parameters

X	The set object (`IsLSet`).
Ops	The family of operations on `X::Domain`.