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 })