HSP structure-preserving operations on algebras — H (quotient, with a relational congruence reading) + P (direct product) + S (subalgebra) carrier-side concepts; their laws and totality are read off the construction in category:total.
More...
Classes | |
| struct | dedekind::category::quotient_algebra_base< Q > |
quotient_algebra_base<Q>: carrier-side declaration that Q is a quotient of some base algebra. Specialise the ::type member at the carrier-defining partition (e.g.\ Complex<R> in numbers:complex records quotient_algebra_base<Complex<R>>::type = R). More... | |
| struct | dedekind::category::construction_base< Q > |
| struct | dedekind::category::quotient_congruence< Q > |
quotient_congruence<Q>: carrier-side declaration of the congruence witnessing Q = V/R. ::type is the relation R, ::carrier is the carrier V that R lives on (R is a homogeneous relation on V). Mirrors the S-leg's subalgebra_base. More... | |
| struct | dedekind::category::detail_quotient::IntByEquality |
| struct | dedekind::category::quotient_congruence< detail_quotient::IntByEquality > |
| struct | dedekind::category::product_algebra_base< Q > |
product_algebra_base<Q>: carrier-side declaration that Q is a finite direct product of some base algebra (the P operation in Birkhoff HSP). Specialise the ::type member at the carrier-defining partition (e.g.\ Vec2V<T> in linear_algebra:vec2 records product_algebra_base<Vec2V<T>>::type = T). More... | |
| struct | dedekind::category::is_linear_action< Q, product_algebra_base_t< Q >, std::plus< Q >, std::plus< product_algebra_base_t< Q > >, std::multiplies< product_algebra_base_t< Q > >, std::multiplies<> > |
| struct | dedekind::category::subalgebra_base< S > |
subalgebra_base: carrier-side declaration that S is a subalgebra of some base algebra (the S operation in Birkhoff HSP). Specialise the ::type member at the carrier-defining partition; the propagation specs below then lift the species-trait pins from base to S. More... | |
| struct | dedekind::category::construction_base< S > |
Namespaces | |
| namespace | dedekind::category |
Concepts | |
| concept | dedekind::category::IsQuotientAlgebra |
Q is declared as a quotient of some base algebra. | |
| concept | dedekind::category::IsCongruenceQuotient |
Q is a quotient of a carrier V by a declared congruence R for Op and reduces from V — the relational reading of the H leg. | |
| concept | dedekind::category::IsProductAlgebra |
Q is declared as a finite direct product of some base algebra. | |
| concept | dedekind::category::IsSubalgebra |
Subobject S of A is a subalgebra under operation Op when it is closed under Op. | |
| concept | dedekind::category::IsSubalgebraOf |
S is declared as a subalgebra of some base algebra. | |
Typedefs | |
| template<typename Q> | |
| using | dedekind::category::quotient_algebra_base_t = typename quotient_algebra_base<Q>::type |
Convenience alias for quotient_algebra_base<Q>::type. | |
| template<typename Q> | |
| using | dedekind::category::quotient_congruence_t = typename quotient_congruence<Q>::type |
Convenience alias for quotient_congruence<Q>::type (the congruence relation R). | |
| template<typename Q> | |
| using | dedekind::category::quotient_congruence_carrier_t = typename quotient_congruence<Q>::carrier |
Convenience alias for quotient_congruence<Q>::carrier (the carrier V that the congruence lives on). | |
| template<typename Q> | |
| using | dedekind::category::product_algebra_base_t = typename product_algebra_base<Q>::type |
Convenience alias for product_algebra_base<Q>::type. | |
| template<typename S> | |
| using | dedekind::category::subalgebra_base_t = typename subalgebra_base<S>::type |
Convenience alias for subalgebra_base<S>::type. | |
Variables | |
| template<typename S, typename A, typename Op> | |
| constexpr bool | dedekind::category::is_closed_under_v = false |
User-declared closure witness: subobject S of A is closed under operation Op. | |
Detailed Description
HSP structure-preserving operations on algebras — H (quotient, with a relational congruence reading) + P (direct product) + S (subalgebra) carrier-side concepts; their laws and totality are read off the construction in category:total.
@partition :quotient
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
- Note
- "A class @c K of algebras is closed under the formation of subalgebras, homomorphic images, and direct products if and only if @c K is the class of all algebras satisfying some set of identities." — Garrett Birkhoff, On the structure of abstract algebras, Proc. Cambridge Phil. Soc. 31 (1935), Theorem 1; the modern formulation is in Burris–Sankappanavar~[§II.11] (Theorem 11.9, the HSP theorem).
quotient__The_Meta_Symmetry
A "quotient over a bona fide algebra is itself a bona fide algebra". Categorically: a structure-preserving functor F: C → C (e.g. complex extension Cplx, dual extension Dual) preserves the algebraic surface — associativity, commutativity, distributivity — of its input, and totality is read off the construction (:total, Path E). This partition reifies that meta- symmetry at the type level: the carrier-side declaration quotient_algebra_base<Q>::type = Base records the functorial relation, and :total reads Q's laws and totality off that declaration.
The arrow-side cousin is IsQuotientMorphism in :universal — a declared homomorphism + declared surjectivity, naming the canonical projection π: Base → Base/~ = Q. The two together formalise the quotient construction at both ends:
IsQuotientAlgebra<Q>(this partition; carrier side)IsQuotientMorphism<Arrow>(:universal; morphism side)
Two concrete instantiations ship today (#498/#499 NEW-A):
Complex<R>=R[i]/(i²+1) (numbers:complex)Dual<F>=F[ε]/(ε²) (analysis:dual)
Rational = Frac(I) is not one: the field of fractions is a localization (ℤ ↪ ℚ embeds, nothing is collapsed; fields are not a variety), so Birkhoff's H leg does not apply and ℚ registers its laws directly (numbers:rational).
Each carrier site declares the quotient relation once via a single quotient_algebra_base<Q> specialisation; category:total reads the laws and totality off it without per-trait enumeration. Carrier- specific bits (additive identity values, additive inverse via -q) remain at the carrier site as unit_trait / inverse_trait specialisations because their construction depends on the carrier's internal layout.
quotient__Categorical_Reading
In the :morphism vocabulary, the quotient construction is a a functor between categories and its image is an object of the target category. The construction rules in category:total express functoriality at the trait level: the laws and totality of Q are read off those of Base under std::plus / std::multiplies, exactly as a structure-preserving functor does on objects in CRing or Mod_R.
Issues #498 (Algebraic Tower) / #499 (NEW-A trait registry).
