2×2 matrices — as linear maps between 2-tuples (the worked first-class instance; n>2 lives behind the structure-preserving combinators of #368). More...

#include <concepts>
#include <cstddef>
#include <functional>
#include <type_traits>
#include <utility>
import dedekind.linear_algebra:vec2;
import dedekind.sets;
import dedekind.order;
import dedekind.category;
import dedekind.numbers;
import dedekind.algebra;

Include dependency graph for mat2x2.cppm:

Classes
struct	dedekind::linear_algebra::Invertible2x2< T, a, b, c, d >
	Full-rank 2×2 matrix with entries as non-type template parameters. More...
struct	dedekind::linear_algebra::Matrix2x2< T, a, b, c, d >
	General (possibly-singular) 2×2 matrix with NTTP entries. More...
struct	dedekind::linear_algebra::DirectSum< A, B >
	Direct sum of two invertibles — the trivial compositional preserver. More...
struct	dedekind::linear_algebra::BlockUpperTriangular< A, B, D >
	Block-upper-triangular matrix — Tier 2 of #366, the degenerate-Schur case where the lower-left block is zero. More...
struct	dedekind::linear_algebra::Matrix2x2V< T >
	Value-level 2×2 matrix — the runtime companion to NTTP Matrix2x2. More...
struct	dedekind::linear_algebra::Matrix2x2Map< T, F >
	`f` on every entry: the matrix2x2_functor's action on an arrow, an endomap of the entries applied entrywise. More...
struct	dedekind::linear_algebra::matrix2x2_functor< T >
struct	dedekind::category::is_functorial< dedekind::linear_algebra::matrix2x2_functor< T > >
	Elementwise lifts: the functor laws hold by construction. More...
struct	dedekind::category::unit_witness< dedekind::linear_algebra::matrix2x2_functor< T >, T >
struct	dedekind::category::counit_witness< dedekind::linear_algebra::matrix2x2_functor< T >, T >
	Counit / extract for `Matrix2x2V<T>`: top-left corner. Matches the `m11` = (1, 1) entry — the canonical projection from the matrix algebra to the underlying scalar ring. More...
struct	dedekind::category::unit_trait< dedekind::linear_algebra::Matrix2x2V< T >, std::plus< dedekind::linear_algebra::Matrix2x2V< T > > >
	The units of `M₂(T)`, built from the scalars' own: the zero matrix for `+`, the identity for `×`, what a ring homomorphism into it carries `0` and `1` to. More...
struct	dedekind::category::unit_trait< dedekind::linear_algebra::Matrix2x2V< T >, std::multiplies< dedekind::linear_algebra::Matrix2x2V< T > > >
struct	dedekind::category::is_associative< dedekind::linear_algebra::Matrix2x2V< T >, std::plus< dedekind::linear_algebra::Matrix2x2V< T > > >
struct	dedekind::category::is_associative< dedekind::linear_algebra::Matrix2x2V< T >, std::multiplies< dedekind::linear_algebra::Matrix2x2V< T > > >
struct	dedekind::category::is_commutative< dedekind::linear_algebra::Matrix2x2V< T >, std::plus< dedekind::linear_algebra::Matrix2x2V< T > > >
struct	dedekind::category::is_total_by_construction< dedekind::linear_algebra::Matrix2x2V< T >, std::plus< dedekind::linear_algebra::Matrix2x2V< T > > >
struct	dedekind::category::is_total_by_construction< dedekind::linear_algebra::Matrix2x2V< T >, std::multiplies< dedekind::linear_algebra::Matrix2x2V< T > > >

Namespaces
namespace	dedekind::category
namespace	dedekind::linear_algebra::detail

Concepts
concept	dedekind::category::detail_mat2x2::HasRingEntries
	The entries form a ring under the `+` and `×` the matrices are computed with: then `M₂(T)` is a ring (Lang, Algebra, §XIII.1), each law below inherited from it, and not otherwise.

Typedefs
template<typename T = int>
using	dedekind::linear_algebra::Identity2x2 = Invertible2x2<T, T{1}, T{0}, T{0}, T{1}>
	The 2×2 identity matrix over T: [[1, 0], [0, 1]].
template<typename T = int>
using	dedekind::linear_algebra::Zero2x2 = Matrix2x2<T, T{0}, T{0}, T{0}, T{0}>
	The 2×2 zero matrix — the additive identity in the ring of matrices.
using	dedekind::linear_algebra::_newb_compositional_pin::Q = dedekind::numbers::Rational<dedekind::numbers::default_integer>
using	dedekind::linear_algebra::_newb_compositional_pin::Vec2_Q = dedekind::linear_algebra::Vec2V<Q>
using	dedekind::linear_algebra::_newb_compositional_pin::Mat2_Q = dedekind::linear_algebra::Matrix2x2V<Q>

Functions
template<typename T, T a, T b, T c, T d, T a2, T b2, T c2, T d2>
constexpr auto	dedekind::linear_algebra::operator* (Invertible2x2< T, a, b, c, d >, Matrix2x2< T, a2, b2, c2, d2 >)
	Mixed composition: Invertible2x2 · Matrix2x2 → Matrix2x2.
template<typename T> requires std::semiregular<T> && dedekind::algebra::HasRingOperators<T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::inverse (const Matrix2x2V< T > &a, std::plus< Matrix2x2V< T > >)
	The additive inverse, \(-A\) entry by entry: the hook `category::inverse_v` reads, found by argument-dependent lookup.
template<typename T>
constexpr Vec2V< T >	dedekind::linear_algebra::operator* (const Matrix2x2V< T > &A, const Vec2V< T > &v)
	Matrix-column-vector product: (2×2) · (2×1) → (2×1).
template<typename T>
constexpr Covec2V< T >	dedekind::linear_algebra::operator* (const Covec2V< T > &v, const Matrix2x2V< T > &A)
	Row-vector-matrix product: (1×2) · (2×2) → (1×2).
template<typename T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::operator\| (const Vec2V< T > &a, const Vec2V< T > &b)
	Horizontal concatenation of two column vectors into a 2×2 matrix.
template<typename T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::operator/ (const Covec2V< T > &a, const Covec2V< T > &b)
	Vertical concatenation of two row vectors into a 2×2 matrix.

Variables
template<typename T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::identity_matrix2x2_v {T{1}, T{0}, T{0}, T{1}}
	Value-level identity: [[1, 0], [0, 1]].
template<typename T>
constexpr Matrix2x2V< T >	dedekind::linear_algebra::zero_matrix2x2_v {T{0}, T{0}, T{0}, T{0}}
	Value-level zero: [[0, 0], [0, 0]].
template<detail_mat2x2::HasRingEntries T>
constexpr bool	dedekind::category::is_distributive_v< dedekind::linear_algebra::Matrix2x2V< T >, std::multiplies< dedekind::linear_algebra::Matrix2x2V< T > >, std::plus< dedekind::linear_algebra::Matrix2x2V< T > > >
template<typename T>
constexpr bool	dedekind::linear_algebra::is_endomorphism_ring_v< Matrix2x2V< T >, Vec2V< T > > = true
constexpr Matrix2x2V< Rat >	dedekind::linear_algebra::detail::nc_a {Rat{0L}, Rat{1L}, Rat{0L}, Rat{0L}}
constexpr Matrix2x2V< Rat >	dedekind::linear_algebra::detail::nc_b {Rat{0L}, Rat{0L}, Rat{1L}, Rat{0L}}
constexpr Matrix2x2V< Rat >	dedekind::linear_algebra::detail::decomp_probe
constexpr Vec2V< Rat >	dedekind::linear_algebra::detail::tr_vec {Rat{7L}, Rat{-3L}}
constexpr Covec2V< Rat >	dedekind::linear_algebra::detail::tr_covec {Rat{2L}, Rat{5L}}
constexpr Matrix2x2V< Rat >	dedekind::linear_algebra::detail::orth_I = identity_matrix2x2_v<Rat>
constexpr Matrix2x2V< Rat >	dedekind::linear_algebra::detail::orth_R90 {Rat{0L}, Rat{-1L}, Rat{1L}, Rat{0L}}
constexpr Matrix2x2V< Rat >	dedekind::linear_algebra::detail::orth_Rx {Rat{1L}, Rat{0L}, Rat{0L}, Rat{-1L}}
constexpr Matrix2x2V< Rat >	dedekind::linear_algebra::detail::orth_R180 = orth_R90 * orth_R90
constexpr Vec2V< Rat >	dedekind::linear_algebra::detail::col_e1 {Rat{1L}, Rat{0L}}
constexpr Vec2V< Rat >	dedekind::linear_algebra::detail::col_e2 {Rat{0L}, Rat{1L}}
template<typename T, typename Idx>
constexpr bool	dedekind::category::is_eval_arrow_v< dedekind::linear_algebra::Matrix2x2V< T >, Idx > = true
template<typename T, std::integral U, U I>
constexpr bool	dedekind::category::is_eval_arrow_v< dedekind::linear_algebra::Matrix2x2V< T >, std::integral_constant< U, I > > = true
constexpr Matrix2x2V< unsigned int >	dedekind::linear_algebra::detail_op::opm {1u, 2u, 3u, 4u}

Detailed Description

2×2 matrices — as linear maps between 2-tuples (the worked first-class instance; n>2 lives behind the structure-preserving combinators of #368).

@partition :mat2x2

Following Stammbach's "Lineare Algebra", matrices are interpreted as linear maps on the 2-vector carriers from :vec2. This partition carries two parallel families:

NTTP family: Invertible2x2, Matrix2x2, Identity2x2, Zero2x2, DirectSum, BlockUpperTriangular. Entries live in the type, so algebraic identities like M * M.inverse() == Identity2x2<T>{} reduce to type equalities and are decidable as static_asserts.
Value family: Matrix2x2V<T> with identity / zero constants plus shape-conforming linear actions Matrix2x2V × Vec2V → Vec2V and Covec2V × Matrix2x2V → Covec2V. This is the carrier the ℂ/𝔻 → M₂ regular representations in :embeddings target.

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

matrix__Tier0_Existential_Proof

Tier 0 of issue #366 — the block-Schur invertibility recursion program. This partition establishes the base case that higher tiers compose: Invertible2x2<T, a, b, c, d> is an NTTP-parameterised 2×2 matrix with the full-rank witness a*d - b*c ≠ 0 enforced by static_assert at instantiation, and with inverse_type given by the closed-form Cramer expression (1/det) · [[d, -b], [-c, a]].

The carrier T is expected to be a structural (C++20 NTTP-compatible) type with ring-like arithmetic; the paper-facing existential proof uses Rational<long> (ℚ as a proxy for ℝ per the #364 / #366 narrowing), since exact rational arithmetic sidesteps the rounding / structurality questions that double would raise today.

matrix__Module_Action_Alignment

Vec2<T, x, y> is a structural 2-vector carrying its coordinates as NTTPs. Invertible2x2 carries a left action on Vec2 via operator*(Vec2), which is the compile-time analogue of the linear action GL_2(T) × T² → T² that underlies dedekind.algebra:modules / :action conceptually. Because entries live in the type, each matrix-vector product is a type-level rewrite, observable via static_assert.

matrix__DSL_Surface

using Q = dedekind::numbers::Rational<long>;
// M = [[1, 2], [3, 4]],  det = -2
constexpr Invertible2x2<Q, Q{1L}, Q{2L}, Q{3L}, Q{4L}> M{};
static_assert(M * M.inverse() == Identity2x2<Q>{});

Wikipedia: Invertible matrix, Cramer's rule, General linear group, Group action

Note: "The notion of a matrix ... appears to me to be one of considerable importance: it includes that of an ordinary algebraic quantity, and also that of a quaternion." — Arthur Cayley, A Memoir on the Theory of Matrices, Philosophical Transactions of the Royal Society of London 148 (1858), Article 14.

See also: #297 undergraduate linear algebra (work in progress): n×n determinants, adjugates and inverses.

Typedef Documentation

◆ Identity2x2

template<typename T = int>

using dedekind::linear_algebra::Identity2x2 = Invertible2x2<T, T{1}, T{0}, T{0}, T{1}>

export

The 2×2 identity matrix over T: [[1, 0], [0, 1]].

Parameter-free reveal tag; mirrors the Ø{} / Singleton<V>{} convention from dedekind.order:halfspace. Callers write static_assert(M * M.inverse() == Identity2x2<T>{}) without having to spell the entries. T defaults to int for simple integer-matrix tests; paper-facing ℚ proofs pass T = Rational<Z> explicitly.

Function Documentation

◆ inverse()

template<typename T>
requires std::semiregular<T> && dedekind::algebra::HasRingOperators<T>

Matrix2x2V< T > dedekind::linear_algebra::inverse	(	const Matrix2x2V< T > &	a,
		std::plus< Matrix2x2V< T > >	)

constexprexport

The additive inverse, \(-A\) entry by entry: the hook category::inverse_v reads, found by argument-dependent lookup.

Parameters

a	the matrix.

Returns: \(-A\).

◆ operator*() [1/2]

template<typename T>

Vec2V< T > dedekind::linear_algebra::operator*	(	const Matrix2x2V< T > &	A,
		const Vec2V< T > &	v )

constexprexport

Matrix-column-vector product: (2×2) · (2×1) → (2×1).

matrix__Bifunctorial_And_Concept_Witnessed_Shapes

Higher matrix shapes do not fit the unary IsShapedFunctor mould as cleanly as the (1×1, 2×1, 1×2, 2×2) family above:

DirectSum<A, B> and BlockUpperTriangular<A, B, D> are naturally bifunctors / trifunctors Mat × Mat → Mat: block-diagonal / block-UT composition is functorial in each argument separately but not unary. Witnessing them via the unary IsShapedFunctor concept would require either a partial application trick (functor for fixed B / fixed D) or an IsBifunctor extension to the category partition;
Orthogonality, rotation, diagonality etc. live as concept-level invariants on Matrix2x2V <·> (e.g. IsOrthogonalMatrixCarrier in :contracts), not as separate carrier types. Until #368 introduces dedicated carriers Orthogonal2x2<T>, Rotation2x2<T>, etc., there is no type for a functor to map into;

Both directions are real upgrades but require either bifunctor concept work or new concrete carrier types from #368. Tracked separately rather than folded in here.

matrix__Shape_Conforming_Linear_Actions

Matrix2x2V × Vec2V → Vec2V (left action on column vectors, 2×2 · 2×1) and Covec2V × Matrix2x2V → Covec2V (right action on row vectors, 1×2 · 2×2). The inner dimension 2 = column_count(M) = row_count(v) lines up; the outer shape of the result is determined by the outer dimensions. Mismatched shapes would be structurally ill-typed — no overload exists for Matrix2x2V × Covec2V or Vec2V × Matrix2x2V.

◆ operator*() [2/2]

template<typename T, T a, T b, T c, T d, T a2, T b2, T c2, T d2>

auto dedekind::linear_algebra::operator*	(	Invertible2x2< T, a, b, c, d >	,
		Matrix2x2< T, a2, b2, c2, d2 >	)

constexprexport

Mixed composition: Invertible2x2 · Matrix2x2 → Matrix2x2.

Product of an invertible matrix with a possibly-singular one is in general singular, so the result is typed as Matrix2x2. Defined as a free function since it can't live as an Invertible2x2 member — that member already specialises to Invertible2x2 return type.

◆ operator/()

template<typename T>

Matrix2x2V< T > dedekind::linear_algebra::operator/	(	const Covec2V< T > &	a,
		const Covec2V< T > &	b )

constexprexport

Vertical concatenation of two row vectors into a 2×2 matrix.

(a.x, a.y) / (b.x, b.y) = [[a.x, a.y],
                           [b.x, b.y]]

Inverse of Matrix2x2V::row: (M.row(0) / M.row(1)) == M.

◆ operator|()

template<typename T>

Matrix2x2V< T > dedekind::linear_algebra::operator\|	(	const Vec2V< T > &	a,
		const Vec2V< T > &	b )

constexprexport

Horizontal concatenation of two column vectors into a 2×2 matrix.

— tuples into matrices.

Concatenation is the inverse of decomposition: the column view of a matrix M.column(0) and M.column(1) reassembles to M under |; similarly the row view reassembles under /. This makes the slogan "a matrix is both a horizontal concatenation of its columns and a vertical concatenation of its rows" operationally meaningful — the decomposition and the concatenation are mutual inverses at the value level, witnessed by static_assert below.

Operator_choice

| echoes the classical augmented-matrix notation [A | B] and is read as horizontal concatenation (append columns).
/ mirrors the LaTeX vertical-split convention [A / B]; reads as vertical concatenation (stack rows).
>> was deliberately avoided: it is already wired throughout dedekind.category as categorical composition / Kleisli bind, and reusing it for the coproduct-side concatenation operation would overload the symbol across two distinct categorical ideas.

Scalar_→_tuple concatenation is already handled by aggregate initialisation: Vec2V<T>{a, b} and Covec2V<T>{a, b} literally concatenate two scalars into the respective 2×1 / 1×2 tuple.

(a.x, a.y)ᵀ | (b.x, b.y)ᵀ = [[a.x, b.x],
                             [a.y, b.y]]

Inverse of Matrix2x2V::column: (M.column(0) | M.column(1)) == M.

Classes

Namespaces

Concepts

Typedefs

Functions

Variables

Detailed Description

matrix__Tier0_Existential_Proof

matrix__Module_Action_Alignment

matrix__DSL_Surface

Typedef Documentation

◆ Identity2x2

Function Documentation

◆ inverse()

◆ operator*() [1/2]

matrix__Bifunctorial_And_Concept_Witnessed_Shapes

matrix__Shape_Conforming_Linear_Actions

◆ operator*() [2/2]

◆ operator/()

◆ operator|()

— tuples into matrices.