vectorspace.cppm File Reference

vector-space concepts + concrete witnesses. More...

#include <cstdint>
#include <functional>
import dedekind.algebra:modules;
import dedekind.category;

Include dependency graph for vectorspace.cppm:

Classes
struct	dedekind::algebra::Bit2U64Action
	Scalar action \(\mathbb{F}_2 \times \mathbb{F}_2^{64} \to \mathbb{F}_2^{64}\) on (bool, uint64_t). More...
struct	dedekind::category::is_linear_action< dedekind::algebra::𝔽64, bool, std::plus< dedekind::algebra::𝔽64 >, std::bit_xor< bool >, std::bit_and< bool >, std::multiplies<> >
struct	dedekind::category::is_linear_action< std::uint64_t, bool, std::bit_xor< std::uint64_t >, std::bit_xor< bool >, std::bit_and< bool >, dedekind::algebra::Bit2U64Action >

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::algebra::IsVectorSpace
	The Gold Standard: A Module where the Scalar is a Field.
concept	dedekind::algebra::IsFieldElement
	A bona fide element of a field is a 1D vector space over itself.
concept	dedekind::algebra::HasVectorSpaceOperators
	Pragmatic vector-space check used by first reified vector carriers.
concept	dedekind::algebra::SatisfiesVectorSpaceAxioms
	Operational witness of the core vector-space axiom signatures.

Variables
template<typename V, typename F>
constexpr bool	dedekind::algebra::is_vector_space_v = IsVectorSpace<V, F>
	is_vector_space_v<V, F>: V is an F-vector-space. Concept-based dispatch — fires automatically when IsVectorSpace<V, F> holds (which composes IsModule<V, F> + IsField<F>). Companion to is_module_v in :modules. (#498/#499 trait registry.)

Detailed Description

vector-space concepts + concrete witnesses.

@partition :vectorspace

Copyright

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

vectorspace__Scope

A vector space is a module whose scalar ring is additionally a field. This partition hosts the concepts and the concrete vector-space witnesses at that strictly higher layer:

• IsVectorSpace<V, F> — strict axiomatic witness, uses the axiomatic dedekind::category::IsField.
• HasVectorSpaceOperators<V, F> — operational counterpart.
• IsFieldElement<F> — slogan: "a field element is a 1D vector space over itself." Its operational counterpart is the canonical HasFieldOperators<F> from :field.
• SatisfiesVectorSpaceAxioms — structural axiom-shape battery.

Witnesses:

• RealLine as HasVectorSpaceOperators (operational);
• 𝔽64 (from :galois) as IsVectorSpace<𝔽64, bool> — a 6-D vector space over the prime subfield \(\mathbb{F}_2\);
• uint64_t as IsVectorSpace<uint64_t, bool, ...> — \(\mathbb{F}_2^{64}\), the 64-D vector space over \(\mathbb{F}_2\). Not a field: has zero divisors. Adds no struct: uint64_t already \emph{is} the carrier; XOR is addition; a Bit2U64Action functor is the scalar action.

The module-level concepts (semimodule, module, 1D OneDimensionalVector, integral-scalar detectors) remain in :modules; the operational field-shape witness HasFieldOperators is canonical in :field; Galois-field concepts and carriers (bool-as-𝔽2, struct 𝔽64) live in :galois. :vectorspace imports all three.

Note

"Die Geometrie ist nicht die Wissenschaft von den Größen, sondern von der Art und Weise, wie sie zusammenhängen." [Trans: "Geometry is not the science of magnitudes, but of the way they hang together."] — Hermann Graßmann, Die lineale Ausdehnungslehre, ein neuer Zweig der Mathematik (Leipzig, 1844), Einleitung. The founding text of vector-space theory; Graßmann's relational framing prefigures the modern axiomatic definition.

Variable Documentation

is_vector_space_v

template<typename V, typename F>

bool dedekind::algebra::is_vector_space_v = IsVectorSpace<V, F>

inlineconstexprexport

is_vector_space_v<V, F>: V is an F-vector-space. Concept-based dispatch — fires automatically when IsVectorSpace<V, F> holds (which composes IsModule<V, F> + IsField<F>). Companion to is_module_v in :modules. (#498/#499 trait registry.)

vectorspace__Formal_Verification