Papers With

← All papers
First page of Transpose Symmetry of Injectivity over Commutative Semirings

Transpose Symmetry of Injectivity over Commutative Semirings

Sixuan Gu, Wei Qi, Yaoyu Cheng

math.RA Aug 17, 2026 · v1
formalization mathlib algebra
Read PDF arXiv abstract Code
TL;DR
The main transpose-injectivity theorem over commutative semirings is formalized in Lean 4 with Mathlib, with a public GitHub repository.
Abstract
Let R be a commutative semiring, not necessarily with a multiplicative identity, and let A be an element of Mn(R). We prove that the map x to Ax on Rn is injective if and only if x to AT x is injective. Equivalently, the left- and right-cancellative elements of the multiplicative semigroup Mn(R) coincide. The proof splits formal determinant expansions into their even and odd halves; it uses no subtraction, additive cancellation, group completion, inverse, or multiplicative identity. As consequences we recover the stable-finiteness theorem for matrices over unital commutative semirings. We also prove that surjectivity is invariant under transpose. In fact, the existence of a surjective square matrix of positive size forces R to have a multiplicative identity.
Problem

For a commutative semiring R, possibly without a multiplicative identity, the question is whether injectivity of the map x ↦ Ax on R^n is equivalent to injectivity of x ↦ A^T x. Determinant arguments that rely on subtraction or group completion do not apply in this setting.

Approach

Signed determinants are replaced by the even and odd halves of the formal determinant expansion, which obey parity identities for column swaps, repeated columns and Laplace expansion. A summand-separation lemma, proved by downward induction on minor size, shows that a_{pq}x_q = a_{pq}y_q. A one-column separation lemma, proved by descending balanced-minor relations, then concludes that x_q = y_q. No step uses cancellation, inverses or a unit, and the results are formalized in Lean 4 with Mathlib.

Results

Injectivity is transpose-invariant over every commutative semiring, so the left- and right-cancellative elements of M_n(R) coincide. Consequences include the Reutenauer–Straubing stable-finiteness theorem and the transpose-invariance of surjectivity. A surjective square matrix of positive size forces R to have a multiplicative identity.