Detailed Description

Matrix-shape carriers — generic n×m matrix aggregator.

@partition :matrix

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

matrix__Scope

Aggregates the n×m matrix carrier family. Today it re-exports the worked first-class instance :mat2x2 (Matrix2x2V<T>, Invertible2x2, Identity2x2, Zero2x2, the 2×2 NTTP family); higher-rank specialisations (Mat3x3V<T>, Mat4x4V<T>, … MatNxMV<T>) slot in here as siblings when they ship. Consumers can either import :matrix for the whole family, or import :mat2x2 directly when they only need the 2×2 case.

The internal-hom End_R(V) = M_n(R) is reified for the worked n=2 case via is_endomorphism_ring_v<Matrix2x2V<T>, Vec2V<T>> in :basis; higher-rank witnesses follow the same shape.

matrix__CT_Framing

In CT lingo a matrix is the homogeneous specialisation of a categorical table:

Table (heterogeneous): a dependent product Π_{(r,c) ∈ R×C} T_{r,c} — entries indexed by row×column positions, with possibly distinct entry-types per position.
Matrix (homogeneous): the exponential / power object T^(R×C) when every entry-type collapses to a single carrier T.

This places matrices in Pierce-land's CCC primitives (dedekind.category:cartesian: products, exponentials), with the homogeneous-entry constraint as the algebraic refinement. The heterogeneous-block-decomposition view (BlockUpperTriangular etc.) is the dependent-product reading; today's family stays homogeneous by convention.