universal.cppm File Reference

The universal-algebra (A, F) meta-pattern: carrier + finitary operations. More...

#include <concepts>
#include <functional>
#include <type_traits>
import dedekind.category;

Include dependency graph for universal.cppm:

Classes
struct	dedekind::algebra::_has_carrier_witness::algebra_view< T >
	Thin algebra-view wrapper used as the pilot for the HasCarrier concept (#573) on a primitive carrier. More...
struct	dedekind::algebra::semiring_ops< S >
	Canonical semiring operations of a carrier, so combinators can default their Add / Mult without a call site spelling them. The default (this primary) is the ordinary ring (+, ×), which is correct for any carrier whose native operators are its semiring ops; carriers whose ops differ specialize (the burden of proof sits at the implementation site): Tropical → (⊕ = TropicalPlus, ⊗ = +), bool → (∨, ∧) — bool must NOT take the default (bool bool promotes to int). This single defaulted seam replaces the old detection(empty-primary)/resolution(semiring_ops_of) split. More...
struct	dedekind::algebra::semiring_ops< bool >
	The Boolean semiring's operations, (∨, ∧). More...
struct	dedekind::algebra::Signature< Ops >
	A signature, the \(F\) of an \((A, F)\) algebra named as one type: the Ops... of IsAlgebra, IsAlgebraOnSet and HasCarrier, which a concept can then take as a parameter and default. More...
struct	dedekind::algebra::detail_universal::homomorphism_of< Arrow, S, T >
	Arrow is an arrow between two algebras, IsAlgebra of S on its domain and of T on its codomain, that carries each operation of S to the one in the same place of T, a monoid homomorphism for each: false unless both are signatures of one nonzero length. A struct, so its partial specialisation fires across module boundaries. More...
struct	dedekind::algebra::detail_universal::preserves< Arrow, Op, Op2 >
	Arrow carries Op to Op2, of any arity, by the declared certificate, and the unit to the unit where Op has one, computed: a unary or non-unital operation asks the law alone. More...
struct	dedekind::algebra::detail_universal::homomorphism_of< Arrow, Signature< Ss... >, Signature< Ts... > >
struct	dedekind::algebra::detail_universal::default_signatures< Arrow >
	The signatures a homomorphism defaults to: the semiring each end of an arrow registers, and the empty signature, which claims nothing, for a type that is no arrow. More...
struct	dedekind::algebra::detail_universal::default_signatures< Arrow >

Concepts
concept	dedekind::algebra::IsClosedAlgebra
	The closure-only tier of an (A, F) algebra: each Op closes on T, without the value-semantics requirement.
concept	dedekind::algebra::IsAlgebra
	The universal-algebra (A, F) pattern at the closure tier.
concept	dedekind::algebra::IsAlgebraOnSet
	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.
concept	dedekind::algebra::IsTotalAlgebra
	The universal-algebra (A, F) pattern at the totality tier — every operation closes on the carrier and is total under the carrier's chosen totality path (Periodic / Idempotent / Saturating).
concept	dedekind::algebra::HasCarrier
	The HAS-A posture in code: an Algebra HAS-A Carrier (under operations Ops) iff the carrier closes the operations (IsAlgebra), the carrier is mereologically a part of the algebra, and the algebra exposes the part via the arrow_drill_down projector.
concept	dedekind::algebra::AlgebraAsProduct
	Set-level sibling of HasCarrier: an algebra is a product of (set object, operations on the underlying type).
concept	dedekind::algebra::IsHomomorphism
	An arrow \(f : A \to B\) between two algebras that carries each operation of the signature S on \(A\) to the one in the same place of T on \(B\): \(f(x \odot y) = f(x) \circledast f(y)\) and \(f(e) = e'\) for each (Burris and Sankappanavar, A Course in Universal Algebra, §II.6).
concept	dedekind::algebra::IsQuotientMorphism
	An arrow that is both a homomorphism of the signatures and surjective (via category::is_epic_arrow_v).
concept	dedekind::algebra::EmbedsAsSubalgebra
	The Birkhoff S leg as an arrow: a monic homomorphism, i.e. a structure-preserving embedding whose image is a subalgebra.

Typedefs
template<typename S>
using	dedekind::algebra::semiring_signature
	The semiring signature a carrier registers, (⊕, ⊗) off semiring_ops: the default family of a homomorphism.

Detailed Description

The universal-algebra (A, F) meta-pattern: carrier + finitary operations.

@partition :universal

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

Wikipedia: Universal algebra, Algebraic structure, Free object.

universal__Why_this_partition

Each specific concept in this module's algebraic hierarchy (IsRing<T, Add, Mult>, IsField<T, Add, Mult>, IsAbelianGroup<T, Op>, IsMonoid<T, Op>, ...) is an instance of the universal-algebra (A, F) pattern of Burris–Sankappanavar 1981 §I.1: a carrier set A with a family F of finitary operations satisfying axioms.

This partition names that pattern explicitly at the closure tier — IsAlgebra<T, Ops...> requires only that each Op closes on T, with axioms living in the specific refinements (IsMonoid, IsAbelianGroup, IsRing, IsField, ...). The relationship between this partition and the others mirrors the relationship between HasRingOperators (closure tier) and IsRing (axiom tier) within the ring partition.

universal__Use_cases

• Documentation anchor: the (A, F) vocabulary is named here, with one citation, and downstream concepts inherit by reference.
• IsHomomorphism<Arrow, Ops...>: an arrow between two algebras that respects each operation of the family, per operation the category's monoid homomorphism.
• IsQuotientMorphism: IsHomomorphism + IsSurjective, exhibiting a quotient as a surjective homomorphism between algebras.
• Generic dispatch for code that handles any algebra without pinning a specific algebraic theory.

Note

"Algebra in the Dedekind topos is the study of operations that preserve structural symmetry." (Per algebra.) Identifying the universal pattern first lets specific symmetries (Ring, Field, AbelianGroup) refine it; the more symmetries we identify mechanically, the lower the per-functor implementation effort downstream.

universal__Naming

The partition is named :universal (universal algebra), not the shorter :algebra, because the umbrella module is itself named dedekind.algebra and a same-named partition would collide.

See also

Burris & Sankappanavar 1981, A Course in Universal Algebra (Springer GTM 78), §I.1.

dedekind.category:functor (IsFAlgebra<Carrier, Structure, Functor>) and dedekind.category:f_algebra (initial-F-algebra / terminal-F-coalgebra universal properties) for the categorical reading of the same notion. Per the textbook isomorphism Alg(Σ) ≅ F_Σ-Alg (Pierce 1991, Basic Category Theory for Computer Scientists §2.2), every IsAlgebra<T, Ops...> instance here corresponds to an F-algebra for the polynomial endofunctor F_Σ generated by the signature Σ = (Ops...). The universal-algebra side (this partition) names the (A, F) carrier-plus-operations pattern; the F-algebra side (category:functor / category:f_algebra) names the same fragment as a category whose objects are structure maps F → A.

Note

"L'algèbre est généreuse: elle donne souvent plus qu'on ne lui demande." [Trans: "Algebra is generous; she often gives more than is asked of her."] — Jean le Rond d'Alembert, attributed (cf. Œuvres, ed.\ Belin 1821, Vol. 1).

Typedef Documentation

semiring_signature

template<typename S>

using dedekind::algebra::semiring_signature

export

Initial value:

 
    Signature<typename semiring_ops<S>::add, typename semiring_ops<S>::mult>

The semiring signature a carrier registers, (⊕, ⊗) off semiring_ops: the default family of a homomorphism.

Template Parameters

S	the carrier.