The N×N matrix over a semiring — Mat(S), the higher-rank, semiring-generic generalisation of :mat2x2's Matrix2x2V<T>.
More...
#include <array>#include <concepts>#include <cstddef>#include <functional>#include <type_traits>import dedekind.linear_algebra:contracts;import dedekind.sets;import dedekind.category;import dedekind.algebra;
Classes | |
| struct | dedekind::linear_algebra::SemimoduleVec< S, N, Orientation > |
An N-entry semimodule vector over the semiring S, read as an index→scalar arrow. IsColumnVector / IsCovector by the default (semimodule) contract: ⊕ and the two-sided scalar ⊗ action, but no negation (a dioid has none). Ket (ColumnOrientation, |v⟩) and Bra (RowOrientation, ⟨w|) are its two orientations — the bra·ket language of | |
| struct | dedekind::linear_algebra::MatNxNV< S, N > |
Mat(S): the N×N matrix over a semiring S. Entries are stored row-major; ⊕ / ⊗ are S's semiring operations, read off dedekind::algebra::semiring_ops (never native operator+/ which the tropical carriers skew). More... | |
| struct | dedekind::linear_algebra::MatPlus< S, N > |
Mat(S)'s additive monoid ⊕: elementwise base-⊕. More... | |
| struct | dedekind::linear_algebra::MatTimes< S, N > |
Mat(S)'s multiplicative monoid ⊗: the ⊕- c_{ij} = ⊕_k a_{ik} ⊗ b_{kj} (matrix multiply). More... | |
| struct | dedekind::linear_algebra::TransposeF< S, N > |
The transpose reified as a dagger functor: TransposeF{}(A) = Aᵀ. A value/type (not a free call), so the point-free dedekind::category dagger predicates and concepts (is_unitary, IsDagger, IsUnitary) can take it as their Dagger argument. On Mat(S) the dagger is the transpose; on Rel it is converse; on a Hilbert space the adjoint — | |
| struct | dedekind::category::unit_trait< dedekind::linear_algebra::MatNxNV< S, N >, dedekind::linear_algebra::MatPlus< S, N > > |
⊕-identity of Mat(S) is the zero matrix. Registered on the exported unit_trait extension point (the internal unit_registry box is not reachable across modules), exactly as dedekind::algebra::Tropical registers its own ∞ / 0. More... | |
| struct | dedekind::category::unit_trait< dedekind::linear_algebra::MatNxNV< S, N >, dedekind::linear_algebra::MatTimes< S, N > > |
⊗-identity of Mat(S) is the identity matrix. More... | |
| struct | dedekind::category::is_involutive< dedekind::linear_algebra::TransposeF< S, N >, dedekind::linear_algebra::MatNxNV< S, N > > |
The transpose is an involution (Aᵀᵀ = A) for any S, so TransposeF is a certified IsInvolution on Mat(S) — the involutive core of the dagger the predicates (is_unitary) read. A structural fact about the operation, not a per-arrow unitarity claim (unitarity is a value property; see | |
| struct | dedekind::category::is_homomorphism< dedekind::linear_algebra::TransposeF< S, N >, dedekind::linear_algebra::MatNxNV< S, N >, dedekind::linear_algebra::MatTimes< S, N >, Opposite< dedekind::linear_algebra::MatTimes< S, N > > > |
Over a commutative scalar ⊗ the transpose reverses matrix multiplication, \((A B)^{\top} = B^{\top} A^{\top}\): a homomorphism into the opposite product, so, with \(A^{\top\top} = A\), a dagger on Mat(S). Witnessed by contravariance_over_commutative_semiring below; over a noncommutative ⊗ the transpose stays an involution and is no dagger. More... | |
| struct | dedekind::category::is_linear_action< dedekind::linear_algebra::SemimoduleVec< S, N, O >, S, std::plus< dedekind::linear_algebra::SemimoduleVec< S, N, O > >, typename dedekind::algebra::semiring_ops< S >::add, typename dedekind::algebra::semiring_ops< S >::mult, std::multiplies<> > |
\(S^N\), entrywise, is a semimodule over any semiring S: the free semimodule of rank N, its laws the semiring's, entry by entry. One certificate for both orientations. More... | |
| struct | dedekind::category::unit_trait< dedekind::linear_algebra::SemimoduleVec< S, N, O >, std::plus< dedekind::linear_algebra::SemimoduleVec< S, N, O > > > |
The ⊕-identity of a dedekind::linear_algebra::SemimoduleVec (a Ket or Bra) is the zero vector (every entry the base ⊕-identity) — what makes it an IsCommutativeMonoid, hence an IsSemimodule, hence an IsColumnVector / IsCovector. One registration for both orientations. More... | |
| struct | dedekind::category::is_saturating< dedekind::linear_algebra::MatNxNV< S, N >, dedekind::linear_algebra::MatPlus< S, N > > |
Totality of Mat(S)'s monoids is inherited, honestly: matrix ⊕ is total exactly when the base ⊕ is a magma, and matrix ⊗ (built from both base ops) when both are. Same discipline as Tropical's ⊗ saturation — true for a periodic/saturating base such as the necklace's saturating-unsigned dioid, false where the base op is a hazard (e.g. signed +). More... | |
| struct | dedekind::category::is_saturating< dedekind::linear_algebra::MatNxNV< S, N >, dedekind::linear_algebra::MatTimes< S, N > > |
| struct | dedekind::category::is_saturating< dedekind::linear_algebra::SemimoduleVec< S, N, O >, std::plus< dedekind::linear_algebra::SemimoduleVec< S, N, O > > > |
Totality distributes over the vector construction (§4 property distribution): a dedekind::linear_algebra::Ket / dedekind::linear_algebra::Bra is a total magma under its elementwise ⊕ exactly when the scalar ⊕ is. Parametric on S — the decision is settled at the call site by which scalar the exhibit uses (a total field such as Rational<default_integer> or the max-plus dioid: yes; a signed long-backed Rational: no), never asserted near the carrier. More... | |
| struct | dedekind::algebra::semiring_ops< dedekind::linear_algebra::MatNxNV< S, N > > |
Mat(S) is a semiring: register its ⊕ / ⊗ so downstream (e.g. star = the *-closure) reads them generically off semiring_ops, exactly as for the base S. More... | |
Namespaces | |
| namespace | dedekind::category |
Concepts | |
| concept | dedekind::linear_algebra::IsLinearOperator |
A linear operator: a (callable) IsArrow that additionally preserves the semimodule structure (the right-S-semimodule-hom law above — sound over any semiring, no commutativity assumed). | |
Typedefs | |
| template<typename S, std::size_t N> | |
| using | dedekind::linear_algebra::Ket = SemimoduleVec<S, N, ColumnOrientation> |
|v⟩: a column of Mat(S) (a ColumnOrientation vector). | |
| template<typename S, std::size_t N> | |
| using | dedekind::linear_algebra::Bra = SemimoduleVec<S, N, RowOrientation> |
⟨w|: a row of Mat(S) (a RowOrientation covector). | |
| using | dedekind::linear_algebra::MPll = dedekind::algebra::MaxPlus<unsigned long long> |
Mat : Semiring → Semiring is inhabited. With S a semiring, Mat(S) = MatNxNV<S,N> is a semiring under (MatPlus, MatTimes). Witnessed at the max-plus dioid, the carrier the necklace/CPM transfer machinery runs on. | |
Functions | |
| template<typename S, std::size_t N, typename O> requires (IsColumnVector<SemimoduleVec<S, N, O>> || IsCovector<SemimoduleVec<S, N, O>>) | |
| constexpr SemimoduleVec< S, N, dual_orientation_t< O > > | dedekind::linear_algebra::transpose (const SemimoduleVec< S, N, O > &v) |
The dagger of a 1-tensor: transpose flips the orientation (Ket ↔ Bra), keeping the components — so \(\mathrm{dagger}(|v\rangle)=\langle v|\) and \(\mathrm{dagger}(\langle w|)=|w\rangle\) ( \((n\times1)^{\top}=1\times n\)). | |
| template<typename S, std::size_t N> | |
| constexpr MatNxNV< S, N > | dedekind::linear_algebra::zero_matrix () |
The zero matrix — every entry the base ⊕-identity (0̄). | |
| template<typename S, std::size_t N> | |
| constexpr MatNxNV< S, N > | dedekind::linear_algebra::identity_matrix () |
The identity matrix — ⊗-identity (1̄) on the diagonal, 0̄ off it. | |
| constexpr bool | dedekind::linear_algebra::nontrivial_maxplus_matvec () |
| constexpr bool | dedekind::linear_algebra::contravariance_over_commutative_semiring () |
Variables | |
| template<typename F> | |
| constexpr bool | dedekind::linear_algebra::is_linear_operator_v = false |
Opt-in: F is a linear operator — a semimodule homomorphism, additive and scalar-equivariant on the matching side: \(f(x\otimes s \oplus y) = f(x)\otimes s \oplus f(y)\). | |
| template<typename S, std::size_t N> | |
| constexpr bool | dedekind::linear_algebra::is_linear_operator_v< MatNxNV< S, N > > = true |
Mat(S) is a linear operator on \(S^N\) — a semimodule homomorphism over any semiring S (the lower bound; no commutativity required). | |
| template<typename S, std::size_t N> | |
| constexpr bool | dedekind::category::is_distributive_v< dedekind::linear_algebra::MatNxNV< S, N >, dedekind::linear_algebra::MatTimes< S, N >, dedekind::linear_algebra::MatPlus< S, N > > |
⊗ distributes over ⊕ in Mat(S) exactly when it does in S (§4 property distribution) — not unconditionally. | |
Detailed Description
The N×N matrix over a semiring — Mat(S), the higher-rank, semiring-generic generalisation of :mat2x2's Matrix2x2V<T>.
@partition :matnxn
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
matnxn__Scope
Matrix2x2V<T> (:mat2x2) is ring-native: it is fixed at 2×2 and consumes T's own operator+ / operator* as ⊕ / ⊗. That shape does not survive the tropical carriers: in dedekind::algebra::Tropical operator+ is ⊗ (honest addition) and ⊕ is a separate functor (TropicalPlus), so native operators route the wrong monoids. The fix is the same one :transfer already uses — read ⊕ / ⊗ off dedekind::algebra::semiring_ops — lifted to a first-class carrier.
MatNxNV<S,N> is therefore the double generalisation (2×2 → N×N, ring → semiring) that :matrix reserves the slot for: Mat(S), the Kleene-algebra-of-matrices (Conway/Kozen). Its two monoids MatPlus (elementwise ⊕) and MatTimes (the ⊕-⊗ contraction) are registered so that Mat(S) is itself an IsSemiring whenever S is — the existential proof that the functor Mat : Semiring → Semiring is inhabited. :transfer's star is then just this semiring's *-closure.
Typedef Documentation
◆ MPll
| using dedekind::linear_algebra::MPll = dedekind::algebra::MaxPlus<unsigned long long> |
Function Documentation
◆ transpose()
requires (IsColumnVector<SemimoduleVec<S, N, O>> || IsCovector<SemimoduleVec<S, N, O>>)
|
constexprexport |
The dagger of a 1-tensor: transpose flips the orientation (Ket ↔ Bra), keeping the components — so \(\mathrm{dagger}(|v\rangle)=\langle v|\) and \(\mathrm{dagger}(\langle w|)=|w\rangle\) ( \((n\times1)^{\top}=1\times n\)).
The vector face of the one dagger documented on MatNxNV::transpose (see dedekind::category::IsDagger). The orientation-flip itself (Ket ↔ Bra, keeping the components) is unconditional, and it is involutive on any semiring: transpose(transpose(v)) == v.
- Warning
- The adjoint alignment with the matrix transpose, \((M|v\rangle)^{\top}=\langle v|M^{\top}\), is not unconditional: its left side contracts \(M_{ij}\otimes v_j\) while \(\langle v|M^{\top}\) contracts \(v_j\otimes M_{ij}\), so the identity needs the scalar
⊗to be commutative (or a scalar anti-involution). It therefore holds for the registered exhibits — real, Boolean, tropical max-plus are all commutative semirings — but not for a noncommutativeS, where the orientation-flip stays involutive yet is no longer the adjoint. Overℂthe true adjoint additionally conjugates the components (FIXME(#787): aconj-awareDaggerfunctor).
Variable Documentation
◆ is_linear_operator_v
|
inlineconstexprexport |
Opt-in: F is a linear operator — a semimodule homomorphism, additive and scalar-equivariant on the matching side: \(f(x\otimes s \oplus y) = f(x)\otimes s \oplus f(y)\).
The law is stated on the right (the scalar on the side the homomorphism preserves for any semiring, by associativity). The left form \(f(s\otimes x)=s\otimes f(x)\) additionally needs a commutative ⊗ and is not what the opt-in certifies (over a commutative S the two coincide; see the Mat(S) registration below for the worked law). Like is_monic_arrow_v (:morphism), linearity quantifies over all inputs, so it cannot be verified at compile time; the carrier declares it and the public review is the audit trail. Mat(S) is registered below.
◆ is_linear_operator_v< MatNxNV< S, N > >
|
inlineconstexprexport |
Mat(S) is a linear operator on \(S^N\) — a semimodule homomorphism over any semiring S (the lower bound; no commutativity required).
\(|v\rangle \mapsto M|v\rangle\) is additive ( \(M(v\oplus w)=Mv\oplus Mw\), by left-distributivity) and scalar-equivariant for the scalar acting on the matching side: \(M(v\otimes s)=(Mv)\otimes s\) holds for every semiring by associativity + distributivity (a right-S-semimodule endomorphism of \(S^N\)). Only the left form \(M(s\otimes v)=s\otimes(Mv)\) needs \(M_{ij}\otimes s=s\otimes M_{ij}\), i.e. a commutative S — over a commutative semiring the two sides coincide and this is the familiar \(f(s\otimes x)=s\otimes f(x)\). So the certification is sound over any semiring (CP #874): the law is the semimodule-hom law, stated on the consistent side, not the left form that would demand commutativity.
