Diagonal matrices: products with matrix units, and commutation

This file records generic identities about diagonal matrices. Multiplying a rectangular matrix unit on both sides by diagonal matrices of the corresponding row and column sizes rescales its one nonzero entry. And a matrix commuting with a diagonal matrix has no entry away from the diagonal wherever that diagonal matrix separates two coordinates, so a matrix commuting with a diagonal matrix of pairwise distinct entries is itself diagonal.

Neither statement needs a unit or an associative multiplication in the entries: the first holds over a NonUnitalNonAssocSemiring, and the second adds commutativity and cancellation by nonzero elements, which is what forces the off-diagonal entries to vanish.

Main results

• TauCeti.diagonal_mul_single_mul_diagonal: multiplying Eᵢⱼ(c) on the left and right by diagonal matrices rescales its entry by the corresponding diagonal coefficients.
• TauCeti.apply_eq_zero_of_commute_diagonal: a matrix commuting with a diagonal matrix has vanishing (i, j) entry wherever that diagonal matrix separates i from j.
• TauCeti.isDiag_of_commute_diagonal: a matrix commuting with a diagonal matrix of pairwise distinct entries is itself diagonal.

@[simp]

theorem TauCeti.diagonal_mul_single_mul_diagonal {m : Type u_1} {n : Type u_2} [DecidableEq m] [Fintype m] [DecidableEq n] [Fintype n] {A : Type u_3} [NonUnitalNonAssocSemiring A] {i : m} {j : n} {v : m → A} {w : n → A} (c : A) : Matrix.diagonal v * Matrix.single i j c * Matrix.diagonal w = Matrix.single i j (v i * c * w j)

Multiplying a matrix unit on the left and right by diagonal matrices rescales its nonzero entry by the corresponding diagonal entries.

theorem TauCeti.apply_eq_zero_of_commute_diagonal {ι : Type u_4} [Fintype ι] [DecidableEq ι] {k : Type u_5} [NonUnitalNonAssocCommSemiring k] [IsLeftCancelMulZero k] {t : ι → k} {g : Matrix ι ι k} (hg : Commute (Matrix.diagonal t) g) {i j : ι} (hij : t i ≠ t j) : g i j = 0

A matrix commuting with a diagonal matrix has vanishing (i, j) entry whenever the diagonal matrix separates the coordinates i and j.

theorem TauCeti.isDiag_of_commute_diagonal {ι : Type u_4} [Fintype ι] [DecidableEq ι] {k : Type u_5} [NonUnitalNonAssocCommSemiring k] [IsLeftCancelMulZero k] {t : ι → k} (ht : Function.Injective t) {g : Matrix ι ι k} (hg : Commute (Matrix.diagonal t) g) : g.IsDiag

A matrix commuting with a diagonal matrix of pairwise distinct entries is diagonal.

theorem Module.Basis.toMatrix_eq_diagonal_of_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (b : Basis ι R M) (f : M →ₗ[R] M) (c : ι → R) (hf : ∀ (i : ι), f (b i) = c i • b i) : (LinearMap.toMatrix b b) f = Matrix.diagonal c

A map diagonal on a basis has that diagonal matrix in the basis coordinates.