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.proj i ∘ₗ toLin' (diagonal w) = w i • LinearMap.proj i

theorem Matrix.diagonal_comp_single {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type v} [CommSemiring R] (w : n → R) (i : n) : toLin' (diagonal w) ∘ₗ LinearMap.single R (fun (x : n) => R) i = w i • LinearMap.single R (fun (x : n) => R) i

@[deprecated Matrix.diagonal_comp_single (since := "2024-08-09")]

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

theorem Matrix.diagonal_toLin' {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type v} [CommSemiring R] (w : n → R) : toLin' (diagonal w) = LinearMap.pi fun (i : n) => 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 (toLin' (diagonal w)) = ⨆ i ∈ {i : m | w i = 0}, LinearMap.range (LinearMap.single K (fun (x : m) => K) i)

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

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