Free-algebra constructions — the textbook companion to HSP. More...
Classes | |
| struct | dedekind::category::free_algebra_base< F > |
free_algebra_base<F>: carrier-side declaration that F is the free algebra over some base R (the textbook companion to HSP; cf. Burris–Sankappanavar §II.11). Specialise the ::type member at the carrier-defining partition (e.g. Polynomial<R, M> in algebra:polynomial records free_algebra_base<Polynomial<R, M>>::type = R). More... | |
| struct | dedekind::category::construction_base< F > |
Namespaces | |
| namespace | dedekind::category |
Concepts | |
| concept | dedekind::category::IsFreeAlgebra |
F is declared as the free algebra over some base R. | |
Typedefs | |
| template<typename F> | |
| using | dedekind::category::free_algebra_base_t = typename free_algebra_base<F>::type |
Convenience alias for free_algebra_base<F>::type. | |
Detailed Description
Free-algebra constructions — the textbook companion to HSP.
@partition :free
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
- Note
- "Given a class @c K of algebras of type @c F and a set @c X
of variables, the @b free @b algebra @c F_K(X) over @c K
with @c X as its set of free generators is uniquely
determined (up to isomorphism) by the property that for
every algebra @c A in @c K and every map @c X @c → @c A
there is a unique homomorphism @c F_K(X) @c → @c A
extending the map." — Stanley Burris and H. P. Sankappanavar, A Course in Universal Algebra [§II.10–11] (paraphrased; the universal property is the textbook definition of
F_K(X)).
free__The_Free_Algebra_Functor
For a variety V of algebras, the free V-algebra on a set X is the universal object F_V(X) admitting a unique homomorphism to any other algebra in V that interprets each generator x ∈ X. Burris–Sankappanavar~[§II.11] gives the construction (term-algebra modulo the variety's laws); the free-algebra functor is the left adjoint to the forgetful functor V → Set. Free algebras are the textbook companion to the HSP variety closure (:quotient): every variety is generated by its free algebra on a sufficiently large set.
Concrete shipping instance: Polynomial<R, M> = R[M], the monoid algebra, is the free commutative R-algebra on the monomials' generators (Lang [§II.3], §IV.1). Other classical free constructions fit the same pattern and would slot in here when carriers ship: the free monoid, the free group, the free vector space.
free__Trait_Propagation
Like H and P, the free-algebra construction is structure-preserving: the laws of + are the base's (coefficientwise), the laws of × rest on the base's commutative-ring laws (the Cauchy product), and totality follows the same reading. A single free_algebra_base<F>::type = R declaration at the carrier site declares the construction; category:total reads the laws and totality off it. Carrier-specific identity / inverse values remain at the carrier site (the construction of zero polynomial / unit polynomial depends on the carrier's internal layout).
Issues #498 (Algebraic Tower) / #499 (NEW-A trait registry).
