Reindexing a square matrix: multiplicativity and the trace

Category: 1-Mathlib (CSD-free).

Matrix.reindex e e relabels a square matrix along e : m ≃ n. Mathlib has it as a linear equivalence (Matrix.reindexLinearEquiv) and as an algebra equivalence (Matrix.reindexAlgEquiv), but the two facts a reindexing argument actually reaches for are awkward to get out of those packages: that it is multiplicative on the nose, and that it leaves the trace alone.

• Matrix.reindex_mul — reindex e e M * reindex e e N = reindex e e (M * N), from Matrix.submatrix_mul_equiv. The algebra equivalence gives this too, but only after unfolding its coercion, which is the step every call site was repeating.
• Matrix.trace_reindex — the trace is unchanged, by Equiv.sum_comp on the diagonal.

Both are stated for reindex e e with a single equivalence on both indices, which is the only case a square matrix admits.

Rule of two. CV/CompositeArena.lean's trace_compositeReindex is the first occurrence of the trace fact and is now a one-line consequence of trace_reindex; CV/ArenaIndexBridge.lean's transport lemmas are the second, and are what prompted the extraction.

References

Mathlib/LinearAlgebra/Matrix/Reindex.lean (reindexAlgEquiv, reindex_apply); Mathlib/Data/Matrix/Mul.lean (submatrix_mul_equiv); specs/future-work.md; specs/BACKLOG.md #133.

theorem Matrix.reindex_mul {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring R] (e : m ≃ n) (M N : Matrix m m R) : (reindex e e) M * (reindex e e) N = (reindex e e) (M * N)

Reindexing is multiplicative.

theorem Matrix.trace_reindex {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [AddCommMonoid R] (e : m ≃ n) (M : Matrix m m R) : ((reindex e e) M).trace = M.trace

Reindexing preserves the trace: the diagonal is permuted, not changed.