The Linear Synthesis (Modules and Vector Spaces). More...
#include <compare>#include <concepts>#include <cstddef>#include <functional>#include <limits>import dedekind.algebra:ring;import dedekind.ieee;import dedekind.category;
Classes | |
| struct | dedekind::algebra::OneDimensionalVector< S, Tag > |
| Reified carrier for a 1D module/vector-space coordinate. More... | |
| struct | dedekind::algebra::BoolLineJoin |
| Additive join on 1D Boolean vectors (OR). More... | |
| struct | dedekind::algebra::BoolLineMeetAction |
| Scalar action on 1D Boolean vectors via meet (AND). More... | |
| struct | dedekind::category::SpeciesTraits< dedekind::algebra::OneDimensionalVector< S, Tag > > |
Namespaces | |
| namespace | dedekind::category |
Concepts | |
| concept | dedekind::algebra::IsIntegralScalar |
| Internal bridge for std::integral scalar carriers. | |
| concept | dedekind::algebra::IsUnsignedIntegralScalar |
| Internal bridge for std::unsigned_integral scalar carriers. | |
| concept | dedekind::algebra::IsFloatingScalar |
| Internal bridge for std::floating_point scalar carriers. | |
| concept | dedekind::algebra::IsModule |
| An Abelian Group participating in a Linear Action by a Ring. | |
| concept | dedekind::algebra::IsScalar |
| A bona fide scalar is a 1D semi-module over itself. | |
| concept | dedekind::algebra::IsSemimodule |
A commutative additive monoid participating in a Linear Action: dedekind::category::IsSemimodule, whose laws are the trait is_linear_action_v there. | |
Typedefs | |
| using | dedekind::algebra::RealLine = OneDimensionalVector<dedekind::ieee::IEEE<double>> |
| Alias: reals seen as a canonical 1D vector carrier. | |
| using | dedekind::algebra::UnsignedLine = OneDimensionalVector<unsigned int> |
| using | dedekind::algebra::BoolLine = OneDimensionalVector<bool> |
| using | dedekind::algebra::RealLineScalar = decltype(RealLine{}.coordinate()) |
Functions | |
| template<IsUnsignedIntegralScalar S, typename Tag> | |
| constexpr OneDimensionalVector< S, Tag > | dedekind::algebra::scale_strength_reduced (const OneDimensionalVector< S, Tag > &v, S factor) |
| Strength-reduced scaling for unsigned 1D vectors. | |
|
template<typename S, typename Tag> requires requires(S s) { { -s } -> std::same_as<S>; } | |
| constexpr dedekind::algebra::OneDimensionalVector< S, Tag > | dedekind::category::inverse (dedekind::algebra::OneDimensionalVector< S, Tag > v, std::plus< dedekind::algebra::OneDimensionalVector< S, Tag > >) |
Variables | |
| template<typename M, typename R> | |
| constexpr bool | dedekind::algebra::is_module_v = IsModule<M, R> |
is_module_v<M, R>: M is an R-module. Concept-based dispatch — fires automatically when IsModule<M, R> holds. | |
Detailed Description
The Linear Synthesis (Modules and Vector Spaces).
@partition :modules
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
modules__Taxonomy_of_Influence
A Module is the reification of 'Structural Action'. It defines how a Ring (the Scalar) acts upon an Additive Group (the Vector), creating the 'Linear Action' that serves as the engine for all Vector Spaces and Metric Geometry in the Dedekind topos.
- Note
- „Die Arithmetik, Algebra und Analysis sind nur eine einzige Wissenschaft, die Wissenschaft der Zahlen.“ (Arithmetic, algebra, and analysis are but a single science, the science of numbers.) — Emmy Noether
Function Documentation
◆ scale_strength_reduced()
|
constexprexport |
Strength-reduced scaling for unsigned 1D vectors.
Multiplication by powers of two is lowered to left-shift when safe.
Variable Documentation
◆ is_module_v
|
inlineconstexprexport |
is_module_v<M, R>: M is an R-module. Concept-based dispatch — fires automatically when IsModule<M, R> holds.
(NEW-A, #498/#499)
The recursive enrichment relations Figure~1 of the paper depicts (ℚ as ℤ-module, 𝔻 as ℝ-module, ℂ as ℝ-module, …) are pinned mechanically as a single concept-based trait variable. Unlike a per-carrier opt-in pattern, the trait fires automatically for any carrier (M, R) whose operators satisfy IsModule<M, R> — no consumer-side registration is required. The strict gating (Module ⟹ Ring) is honoured because IsModule itself composes IsRing; carriers whose scalar fails IsRing won't fire the trait, which is the correct algebraic statement.
Sister traits with structural-metadata payload (rank, endomorphism identity) — is_free_module_v and is_endomorphism_ring_v — live in dedekind.linear_algebra:basis where the metadata is at home.
(NEW-A pilot inventory)
The carriers that currently fire the trait registry across the codebase, with the static_assert witness site for each:
is_module_v witnesses:
is_module_v<Rational<default_integer>, default_integer> — numbers/rational.cppm: ℚ is a ℤ-module via the Frac construction (the localisation S^{-1}ℤ at S=ℤ_≠0).
is_module_v<Complex<Rational<default_integer>>, Rational<default_integer>> — numbers/complex.cppm: ℂ over ℚ is a ℚ-module via the quotient ring ℚ[i]/(i²+1) carrying the canonical componentwise ℚ-action on the (real, imag) pair.
is_module_v<Dual<Rational<default_integer>>, Rational<default_integer>> — analysis/dual.cppm: Dual<ℚ> is a ℚ-module via the quotient-algebra propagation in algebra:quotient (the exact-arithmetic AD instance).
is_module_v<Vec2V<unsigned int>, unsigned int> — linear_algebra/vec2.cppm: the rank-2 free module over the unsigned-integer modular ring.
is_module_v<Vec2V<Rational<default_integer>>, Rational<default_integer>> — linear_algebra/mat2x2.cppm: Vec2 over ℚ as a ℚ-module (the rank-2 vector space over the field ℚ, witnessed at the module tier; under epic #374's HasFieldOperators-to- IsField retargeting, the IsField<Rational> certification in numbers/rational.cppm closes the upgrade to is_vector_space_v automatically via the concept composition).
is_free_module_v specialisations (rank-bearing):
is_free_module_v<Vec2V<unsigned int>, unsigned int, 2> and is_free_module_v<Covec2V<unsigned int>, unsigned int, 2> — linear_algebra/vec2.cppm: the rank-2 free modules and their dual rank-2 free modules over the unsigned-integer modular ring.
is_free_module_v<Vec2V<Rational<default_integer>>, Rational<default_integer>, 2> — linear_algebra/mat2x2.cppm: Vec2 over ℚ as a rank-2 free ℚ-module.
is_endomorphism_ring_v specialisations (internal-hom):
is_endomorphism_ring_v<Matrix2x2V<unsigned int>, Vec2V<unsigned int>> and is_endomorphism_ring_v<Matrix2x2V<Rational<default_integer>>, Vec2V<Rational<default_integer>>> — linear_algebra/mat2x2.cppm: 2×2 matrices as the endomorphism ring of the rank-2 free module, on both the unsigned-integer and ℚ scalar carriers.
Recursive enrichment status:
is_vector_space_v<V, F> automatic upgrade — the trait fires when IsField<F> holds in addition to IsModule<V, F>. Under epic #374's HasFieldOperators-to-, the strict IsField retargetingcategory::IsField closes on Rational<default_integer> via the multiplicative-inverse trait registration in numbers/rational.cppm (zero excluded by the is_invertible_v convention pinned in total.cppm). So every is_module_v witness above whose scalar is ℚ auto-upgrades to is_vector_space_v (ℚ is IsTotal on the exact path, is_exact_total).
The recursive enrichment Figure~1 of the paper depicts (ℚ as ℤ-module, 𝔻 as ℝ-module, ℂ as ℝ-module, …) is structurally in place at the is_module_v / is_free_module_v / is_endomorphism_ring_v tier — with ℚ now also at the is_vector_space_v tier. This inventory is the running snapshot.
