Monomial Matrices Preserve Diagonality

Abstract

Monomial matrices admit a diagonal-times-permutation form and preserve diagonality under the stated transpose sandwich.

Definition 1.1 (Monomial matrix).

$$\begin{array}{c}\forall n:Type,[\mathrm{DecidableEq}\left(n\right)],[\mathrm{Fintype}\left(n\right)],\\ \forall R:Type,[\mathrm{CommRing}\left(R\right)],\\ \forall sigma:\mathrm{Equiv}.\mathrm{Perm}\left(n\right),c:n\to R,\\ \mathrm{monomial}\left(sigma,c\right)=\mathrm{Matrix}.\mathrm{of}\left(i,j\mapsto \{\begin{array}{ll}c\left(i\right),& j=sigma\left(i\right)\\ 0,& \text{otherwise}\end{array}\right).\end{array}$$

Formalization. D5/S3/Quantum/Matrix/MonomialDiagonalPreserving.monomial (✓ std3).

Source. Repository-derived.

Commentary.

The monomial matrix attached to sigma and c places c(i) in row i at column sigma(i), and places zero at every other entry.

This is the generalized permutation matrix pattern with row scalars. When every scalar is nonzero, every row and column has one nonzero entry.

Lemma 1.2 (Diagonal-times-permutation form).

$$\begin{array}{c}\forall n:Type,[\mathrm{DecidableEq}\left(n\right)],[\mathrm{Fintype}\left(n\right)],\\ \forall R:Type,[\mathrm{CommRing}\left(R\right)],\\ \forall sigma:\mathrm{Equiv}.\mathrm{Perm}\left(n\right),c:n\to R,\\ \mathrm{monomial}\left(sigma,c\right)=\mathrm{Matrix}.\mathrm{diagonal}\left(c\right)\cdot \mathrm{PEquiv}.\mathrm{toMatrix}\left(\mathrm{Equiv}.\mathrm{toPEquiv}\left(sigma\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/MonomialDiagonalPreserving.monomial_eq_diagonal_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

A monomial matrix is the permutation matrix of sigma multiplied on the left by the diagonal matrix of row scalars c.

Theorem 1.3 (Diagonality after the transpose sandwich).

$$\begin{array}{c}\forall n:Type,[\mathrm{DecidableEq}\left(n\right)],[\mathrm{Fintype}\left(n\right)],\\ \forall R:Type,[\mathrm{CommRing}\left(R\right)],\\ \forall sigma:\mathrm{Equiv}.\mathrm{Perm}\left(n\right),c,d:n\to R,\\ \mathrm{monomial}\left(sigma,c\right)\cdot \mathrm{Matrix}.\mathrm{diagonal}\left(d\right)\cdot \mathrm{Matrix}.\mathrm{transpose}\left(\mathrm{monomial}\left(sigma,c\right)\right).\mathrm{IsDiag}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/MonomialDiagonalPreserving.isDiag_monomial_mul_diagonal_mul_transpose (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplying a diagonal matrix on the left by a monomial matrix and on the right by its transpose permutes and rescales diagonal entries, so the resulting matrix remains diagonal.

No converse is proved or claimed: the theorem does not say that every matrix preserving diagonality must be monomial.

References

• Truth anchor: D5/S3/Quantum/Matrix/MonomialDiagonalPreserving.isDiag_monomial_mul_diagonal_mul_transpose
• Truth anchor: D5/S3/Quantum/Matrix/MonomialDiagonalPreserving.monomial
• Truth anchor: D5/S3/Quantum/Matrix/MonomialDiagonalPreserving.monomial_eq_diagonal_mul