linear_map.cppm File Reference

Finite-dim linear maps with algebraic witnesses. More...

#include <array>
#include <concepts>
#include <cstddef>
#include <initializer_list>
#include <utility>
import dedekind.geometry:affine;
import dedekind.category;
import dedekind.algebra;

Include dependency graph for linear_map.cppm:

Classes
class	dedekind::geometry::LinearMap< F, Rows, Cols >
	A dense compile-time-sized linear map F^Cols -> F^Rows. More...
class	dedekind::geometry::DifferentiableMap< F, DomainDim, CodomainDim, ValueFn, JacobianFn >
	A finite-dimensional map paired with a user-supplied Jacobian witness. More...
struct	dedekind::geometry::TangentBundlePoint< F, N >
	A point in the tangent bundle T(F^N) = F^N × F^N. More...
struct	dedekind::geometry::CotangentBundlePoint< F, N >
	A point in the cotangent bundle T*(F^N) = F^N × (F^N)*. More...

Concepts
concept	dedekind::geometry::IsMatrixScalar
	A scalar type that can serve as coefficients in a LinearMap.
concept	dedekind::geometry::HasMatrixScalarEmbedding
	Floating carrier that is admissible as a matrix scalar by policy.
concept	dedekind::geometry::HasJacobianAt
	Map-like object exposing a finite-dimensional LinearMap Jacobian.
concept	dedekind::geometry::IsLinearMapModule
	Verify that LinearMap<F, R, C> behaves as a module over scalar F.

Macros
#define	DEDEKIND_ENABLE_DOUBLE_REAL_PROXY   0

Typedefs
template<IsMatrixScalar F, std::size_t Rows, std::size_t Cols>
using	dedekind::geometry::Matrix = LinearMap<F, Rows, Cols>
template<IsMatrixScalar F, std::size_t N>
using	dedekind::geometry::Covector = LinearMap<F, 1, N>
	Covector: a linear functional F^N -> F, represented as a row vector.
template<std::size_t Rows, std::size_t Cols>
using	dedekind::geometry::RealMatrix = LinearMap<double, Rows, Cols>
	RealMatrix: machine-real matrix alias behind explicit opt-in.
template<IsMatrixScalar F, std::size_t N>
using	dedekind::geometry::TangentVector = Vector<F, N>
	TangentVector at a point in F^N.
template<IsMatrixScalar F, std::size_t N>
using	dedekind::geometry::CotangentVector = Covector<F, N>
	CotangentVector at a point in F^N.

Functions
template<typename F> requires std::floating_point<F> && IsMatrixScalar<F>
constexpr F	dedekind::geometry::embed_matrix_scalar (F value) noexcept
	Explicit embedding witness from floating carriers into matrix scalars.
template<IsMatrixScalar F, std::size_t Rows, std::size_t Cols>
constexpr LinearMap< F, Rows, Cols >	dedekind::geometry::operator+ (const LinearMap< F, Rows, Cols > &a, const LinearMap< F, Rows, Cols > &b)
template<IsMatrixScalar F, std::size_t Rows, std::size_t Cols>
constexpr LinearMap< F, Rows, Cols >	dedekind::geometry::operator- (const LinearMap< F, Rows, Cols > &a, const LinearMap< F, Rows, Cols > &b)
template<IsMatrixScalar F, std::size_t Rows, std::size_t Cols>
constexpr LinearMap< F, Rows, Cols >	dedekind::geometry::operator- (const LinearMap< F, Rows, Cols > &a)
template<IsMatrixScalar F, std::size_t Rows, std::size_t Cols>
constexpr LinearMap< F, Rows, Cols >	dedekind::geometry::operator* (const F &scalar, const LinearMap< F, Rows, Cols > &a)
template<IsMatrixScalar F, std::size_t Rows, std::size_t Cols>
constexpr LinearMap< F, Rows, Cols >	dedekind::geometry::operator* (const LinearMap< F, Rows, Cols > &a, const F &scalar)
template<IsMatrixScalar F, std::size_t Rows, std::size_t Cols>
constexpr Vector< F, Rows >	dedekind::geometry::operator* (const LinearMap< F, Rows, Cols > &a, const Vector< F, Cols > &v)
template<IsMatrixScalar F, std::size_t Rows, std::size_t Inner, std::size_t Cols>
constexpr LinearMap< F, Rows, Cols >	dedekind::geometry::operator* (const LinearMap< F, Rows, Inner > &a, const LinearMap< F, Inner, Cols > &b)
template<IsMatrixScalar F, std::size_t N>
constexpr LinearMap< F, N, N >	dedekind::geometry::identity_linear_map ()
template<IsMatrixScalar F, std::size_t Rows, std::size_t Cols>
constexpr LinearMap< F, Rows, Cols >	dedekind::geometry::zero_linear_map ()
template<IsMatrixScalar F, std::size_t DomainDim, std::size_t CodomainDim, typename ValueFn, typename JacobianFn>
constexpr auto	dedekind::geometry::make_differentiable_map (ValueFn value, JacobianFn jacobian)
	Construct a finite-dimensional differentiable map from primal and Jacobian callables.
template<HasJacobianAt Map>
constexpr auto	dedekind::geometry::jacobian_at (const Map &map, const typename Map::Domain &x) -> typename Map::Jacobian
	Return the Jacobian of a finite-dimensional differentiable map.
template<HasJacobianAt Map>
constexpr auto	dedekind::geometry::frechet_derivative_at (const Map &map, const typename Map::Domain &x) -> typename Map::Jacobian
	Return the Fr\'echet derivative of a finite-dimensional map.
template<HasJacobianAt Map> requires (Map::codomain_dimension == 1) && std::same_as< typename Map::Jacobian, Covector<typename Map::scalar_type, Map::domain_dimension>>
constexpr Covector< typename Map::scalar_type, Map::domain_dimension >	dedekind::geometry::differential_at (const Map &map, const typename Map::Domain &x)
	Return the scalar-valued differential as a covector.
template<IsMatrixScalar F, std::size_t M, std::size_t N>
constexpr LinearMap< F, M, N >	dedekind::geometry::outer (const Vector< F, M > &u, const Vector< F, N > &v)
	Outer product u ⊗ v : F^N -> F^M.

Detailed Description

Finite-dim linear maps with algebraic witnesses.

@partition :linear_map

linear_map__Algebraic_Structure

LinearMap<F, R, C> represents a finite-dimensional linear map F^C -> F^R and serves as an algebraic carrier for the theory of modules and vector spaces.

Algebraic Status:

• When F is a Semiring: LinearMap forms a Semimodule over F (additive monoid + external linear action by semiring scalars)
• When F is a Ring: LinearMap forms a Module over F (additive group + external linear action by ring scalars)
• When F is a Field: LinearMap forms a Vector Space over F (additive group + external linear action by field scalars)

The structure ensures that both external operations (scalar action) and internal operations (matrix addition) satisfy the Linear Action Axioms:

1. Vector Additivity: s * (m1 + m2) = s*m1 + s*m2
2. Scalar Additivity: (s1 + s2) * m = s1*m + s2*m

Note

Matrix multiplication (composition) is non-commutative, so the ring of square matrices does NOT form a commutative ring, only a ring.

linear_map__Design_and_Extensibility

The current LinearMap<F, R, C> is a dense matrix implementation with compile-time fixed dimensions. This design is appropriate for:

• Small to medium matrices (dense, static dimensions)
• Static dimension requirements (no runtime resizing)

For other use cases, the architecture supports extensions:

• Sparse matrices: Can be implemented as a separate type (e.g., COO, CSR) with the same algebraic interface (semimodule laws are preserved).
• Infinite/functional matrices: Represented functionally (e.g., Hilbert matrix accessed via coefficient(i,j) = 1/(i+j+1)) or as lazy evaluation.
• Diagonal matrices: Specialized implementation storing only O(n) coefficients while preserving the LinearMap interface.

The semimodule axioms are independent of storage representation, so any alternative matrix type implementing the same arithmetic operations will automatically satisfy the same algebraic structure (if F is a semiring).

Copyright

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

Note

"أشدُّ ما يحتاج إليه من يُعنى بعلم الحساب أن يعرف ما يحتاج الناس إليه في معاملاتهم من المقادير، إذ بذلك يقاس العدل في القضاء." — Muḥammad ibn Mūsā al-Khwārizmī (c. 780–850 CE), mathematician of the Islamic Golden Age, House of Wisdom, Baghdad. Author of Al-Kitāb al-mukhtaṣar fī ḥisāb al-jabr wal-muqābala (Al-Jabr, ~820 CE), the foundational treatise on algebra. The quote is attributed to al-Khwārizmī on Arabic Wikiquote; the specific primary source within his corpus has not been independently verified. [Trans: "What one most needs in the science of computation is to know the quantities people need in their dealings, for by that, justice in judgment is measured."]

See also

#272 Denotational Automatic Differentiation (work in progress): the chain rule for composed DifferentiableMap, the Jacobian from dual propagation.

#286 undergraduate calculus (work in progress): gradient and Hessian.

Typedef Documentation

CotangentVector

template<IsMatrixScalar F, std::size_t N>

using dedekind::geometry::CotangentVector = Covector<F, N>

export

CotangentVector at a point in F^N.

The cotangent space T*_p(F^N) ≅ (F^N)* is the dual of the tangent space. In the finite-dimensional flat case this is canonically represented as a row vector (Covector), i.e. a LinearMap<F, 1, N>.

FIXME(https://github.com/vincentk/dedekind/issues/185): Replace the extensional dimension parameter with a first-class dimension witness once the flat geometry carrier is widened accordingly.

Covector

template<IsMatrixScalar F, std::size_t N>

using dedekind::geometry::Covector = LinearMap<F, 1, N>

export

Covector: a linear functional F^N -> F, represented as a row vector.

linear_map__Module_Structure_Verification

Core Algebraic Theorem: LinearMap<F, R, C> is always a Semimodule over the scalar semiring F.

This means:

1. (LinearMap^{R×C}, +) is an additive commutative monoid
   • Closure: A + B is a LinearMap<F, R, C>
   • Identity: zero_linear_map<F, R, C>() is the additive identity
   • Associativity: (A+B)+C = A+(B+C)
   • Commutativity: A+B = B+A
2. (F, +, *) is a semiring (the scalar carrier)
   • (F, +) is a commutative monoid
   • (F, *) is a monoid
   • Multiplication distributes over addition
3. External linear action F × LinearMap^{R×C} → LinearMap^{R×C}
   • Vector Additivity: s * (A + B) = s*A + s*B
   • Scalar Additivity: (s1 + s2) * A = s1*A + s2*A
   • Associativity: (s1 * s2) * A = s1 * (s2 * A)
   • Identity: 1_F * A = A

Refinements for Special Scalar Types:

• When F is a ring: LinearMap<F, R, C> is a Module over F (Additionally has scalar negation)
• When F is a field: LinearMap<F, R, C> is a Vector Space over F (Additionally has scalar division)
• When F is a machine floating scalar admitted by IsMatrixScalar: LinearMap<F, R, C> is vector-space-like with practical IEEE semantics

Note on Matrix Multiplication (Non-Commutativity): Square matrices M^{n×n} form a ring under matrix addition and composition, but this ring is NON-COMMUTATIVE. However, the semimodule structure of arbitrary matrices is unaffected by composition, since composition only applies to square matrices and acts as an additional binary operation.

A covector (dual vector / linear functional) is canonically a LinearMap<F, 1, N>: it maps a column vector to a length-1 column vector whose single entry is the inner product of the row with the argument.

Covectors form the dual module Hom_F(V, F), where V = F^N. When F is a field, the dual module is isomorphic to V itself.

FIXME(https://github.com/vincentk/dedekind/issues/185): Generalize this alias from the current extensional finite-dimensional carrier to a first-class dimension/cardinality witness once the geometry layer is lifted beyond LinearMap<F, 1, N>.

RealMatrix

template<std::size_t Rows, std::size_t Cols>

using dedekind::geometry::RealMatrix = LinearMap<double, Rows, Cols>

export

RealMatrix: machine-real matrix alias behind explicit opt-in.

linear_map__Specializations_for_Common_Ring_and_Field_Scalars

The following type aliases provide semantic naming for matrices over specific algebraic structures. Each specialization documents the algebraic guarantees of the linear map as a module/vector space.

Provided Alias:

• RealMatrix<R, C>: machine-real matrix alias (double) with explicit opt-in requirement via DEDEKIND_ENABLE_DOUBLE_REAL_PROXY=1.

All specializations are Semimodules at minimum (over the semiring formed by their scalar type). When the scalar forms a ring or field, the matrix carries the corresponding module or vector space structure.

Additional aliases (for complex/rational carriers) are planned and should be introduced only once their scalar/vector contracts are implemented in this partition.

Policy: This alias is only available when DEDEKIND_ENABLE_DOUBLE_REAL_PROXY=1 is set at build time.

Algebraic Interpretation: treated as vector-space-like under the active numeric policy (not as a strict field proof).

Satisfies the linear action laws operationally:

1. Vector Additivity: s * (m1 + m2) = s*m1 + s*m2
2. Scalar Additivity: (s1 + s2) * m = s1*m + s2*m
3. Associativity: (s1 * s2) * m = s1 * (s2 * m)
4. Identity: 1.0 * m = m

This alias is the explicit machine-real lift into the current finite matrix carrier. It remains intentionally extensional for this PR.

FIXME(https://github.com/vincentk/dedekind/issues/185): Generalize the geometry layer from fixed extensional dimensions to first-class dimension witnesses where the surrounding carrier supports it.

For square matrices (R == C), composition forms a non-commutative ring.

TangentVector

template<IsMatrixScalar F, std::size_t N>

using dedekind::geometry::TangentVector = Vector<F, N>

export

TangentVector at a point in F^N.

For the flat manifold F^N, the tangent space T_p(F^N) ≅ F^N for every base-point p. The alias makes the geometric role explicit without introducing any new data.

Note

A bare TangentVector is the fibre element (a single tangent vector), not a tangent-bundle carrier on its own — the latter is a (point, tangent vector) pair, captured by TangentBundlePoint below at the geometric level and by IsTangentBundle in :tangent at the algebraic-ring level. Dual<F> in dedekind.analysis:dual is the canonical IsTangentBundle witness; forward-mode AD on Dual<F> is arithmetic in the tangent-bundle ring T(Spec F).

Function Documentation

embed_matrix_scalar()

template<typename F>
requires std::floating_point<F> && IsMatrixScalar<F>

F dedekind::geometry::embed_matrix_scalar ( F value )

constexprexportnoexcept

Explicit embedding witness from floating carriers into matrix scalars.

This is the policy gate for admitting machine floating carriers into the matrix layer. In particular, double is only embeddable when DEDEKIND_ENABLE_DOUBLE_REAL_PROXY=1.

frechet_derivative_at()

template<HasJacobianAt Map>

auto dedekind::geometry::frechet_derivative_at ( const Map & map, const typename Map::Domain & x )->typenameMap::Jacobian

constexprexport

Return the Fr\'echet derivative of a finite-dimensional map.

In the current finite-dimensional slice, this coincides with the Jacobian.

outer()

template<IsMatrixScalar F, std::size_t M, std::size_t N>

LinearMap< F, M, N > dedekind::geometry::outer ( const Vector< F, M > & u, const Vector< F, N > & v )

constexprexport

Outer product u ⊗ v : F^N -> F^M.

Constructs the rank-1 linear map whose (i,j) coefficient is u[i]*v[j]. Applied to a vector w, it yields dot(v,w) * u (the dyadic product).

Algebraic Properties:

• Bilinear: (a*u) ⊗ v = a * (u ⊗ v) = u ⊗ (a*v) for all scalar a
• Distributes over addition: (u1+u2) ⊗ v = (u1⊗v) + (u2⊗v) and u ⊗ (v1+v2) = (u⊗v1) + (u⊗v2)
• Rank 1: The image of u ⊗ v is the 1-dimensional subspace span(u)