basis.cppm File Reference

Free-module / basis / endomorphism-ring trait registry. More...

#include <cstddef>
import dedekind.algebra;

Include dependency graph for basis.cppm:

Variables
template<typename M, typename R, std::size_t N>
constexpr bool	dedekind::linear_algebra::is_free_module_v = false
	is_free_module_v<M, R, N>: declare that M is a free module of rank N over R.
template<typename A, typename V>
constexpr bool	dedekind::linear_algebra::is_endomorphism_ring_v = false
	is_endomorphism_ring_v<A, V>: declare that A is the endomorphism ring of the module V, i.e.\ A = End_R(V) for the appropriate scalar R.

Detailed Description

Free-module / basis / endomorphism-ring trait registry.

@partition :basis

Copyright

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

basis__Scope

The "rank + basis" structural metadata that distinguishes free modules from arbitrary modules — and the endomorphism-ring identity End_R(V) = M_n(R) on rank-n free modules — lives here. These claims carry structural payload (a rank N, an identity between two named carriers) that no concept on its own derives from the operator surface, so they remain opt-in trait variables rather than concept-based defaults.

Sister anchor in algebra:modules: is_module_v<M, R>, which is concept-based (it fires whenever IsModule<M, R> holds, no carrier-side opt-in needed). The split is the right one because

• "M is a module over R" is purely an algebraic-axioms claim;
• "M is a free module of rank N over R" pins a specific N as metadata, and "A is the endomorphism ring of V" pins a specific (A, V) pair as a structural identity — neither is recoverable from the operator surface alone.

Issues #498 (Algebraic Tower) / #499 (NEW-A trait registry).

Variable Documentation

is_endomorphism_ring_v

template<typename A, typename V>

bool dedekind::linear_algebra::is_endomorphism_ring_v = false

inlineconstexprexport

is_endomorphism_ring_v<A, V>: declare that A is the endomorphism ring of the module V, i.e.\ A = End_R(V) for the appropriate scalar R.

Default false; specialised by carrier sites that own the ring–module pair (e.g. Matrix2x2V<T> over Vec2V<T> in :mat2x2). Pins the internal-hom of the module category mechanically; downstream Figure~1 invariant tests can read this trait rather than reconstructing the equality.

is_free_module_v

template<typename M, typename R, std::size_t N>

bool dedekind::linear_algebra::is_free_module_v = false

inlineconstexprexport

is_free_module_v<M, R, N>: declare that M is a free module of rank N over R.

Default false; specialised by carrier sites at the rank payload they own (e.g. Vec2V<T> over T at rank 2 in :vec2). Specialisations are gated on dedekind::algebra::IsModule<M, R> so the algebraic precondition (R is a ring, M is a module over R) holds before the rank claim is recorded — a free module is a module with a chosen basis, and the module structure must already be present.