Diagonal matrices

This file contains some results on the linear map corresponding to a diagonal matrix (range, ker and rank).

Tags

matrix, diagonal, linear_map

theorem Matrix.proj_diagonal {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type v} [CommSemiring R] (i : n) (w : n → R) : LinearMap.comp (LinearMap.proj i) (↑Matrix.toLin' (Matrix.diagonal w)) = w i • LinearMap.proj i

theorem Matrix.diagonal_comp_stdBasis {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type v} [CommSemiring R] (w : n → R) (i : n) : LinearMap.comp (↑Matrix.toLin' (Matrix.diagonal w)) (LinearMap.stdBasis R (fun x => R) i) = w i • LinearMap.stdBasis R (fun x => R) i

theorem Matrix.diagonal_toLin' {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type v} [CommSemiring R] (w : n → R) : ↑Matrix.toLin' (Matrix.diagonal w) = LinearMap.pi fun i => w i • LinearMap.proj i

theorem Matrix.ker_diagonal_toLin' {m : Type u_1} [Fintype m] {K : Type u} [Semifield K] [DecidableEq m] (w : m → K) : LinearMap.ker (↑Matrix.toLin' (Matrix.diagonal w)) = ⨆ (i : m) (_ : i ∈ {i | w i = 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)

theorem Matrix.range_diagonal {m : Type u_1} [Fintype m] {K : Type u} [Semifield K] [DecidableEq m] (w : m → K) : LinearMap.range (↑Matrix.toLin' (Matrix.diagonal w)) = ⨆ (i : m) (_ : i ∈ {i | w i ≠ 0}), LinearMap.range (LinearMap.stdBasis K (fun x => K) i)

theorem LinearMap.rank_diagonal {m : Type u_1} [Fintype m] {K : Type u} [Field K] [DecidableEq m] [DecidableEq K] (w : m → K) : LinearMap.rank (↑Matrix.toLin' (Matrix.diagonal w)) = ↑(Fintype.card { i // w i ≠ 0 })