Matrices with a single non-zero element. #
This file provides Matrix.stdBasisMatrix. The matrix Matrix.stdBasisMatrix i j c has c
at position (i, j), and zeroes elsewhere.
def
Matrix.stdBasisMatrix
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
(a : α)
:
Matrix m n α
stdBasisMatrix i j a is the matrix with a in the i-th row, j-th column,
and zeroes elsewhere.
Equations
- Matrix.stdBasisMatrix i j a i' j' = if i = i' ∧ j = j' then a else 0
Instances For
@[simp]
theorem
Matrix.smul_stdBasisMatrix
{m : Type u_2}
{n : Type u_3}
{R : Type u_4}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
[SMulZeroClass R α]
(r : R)
(i : m)
(j : n)
(a : α)
:
r • Matrix.stdBasisMatrix i j a = Matrix.stdBasisMatrix i j (r • a)
@[simp]
theorem
Matrix.stdBasisMatrix_zero
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
:
Matrix.stdBasisMatrix i j 0 = 0
theorem
Matrix.stdBasisMatrix_add
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
(a : α)
(b : α)
:
Matrix.stdBasisMatrix i j (a + b) = Matrix.stdBasisMatrix i j a + Matrix.stdBasisMatrix i j b
theorem
Matrix.mulVec_stdBasisMatrix
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
[Fintype m]
(i : n)
(j : m)
(c : α)
(x : m → α)
:
Matrix.mulVec (Matrix.stdBasisMatrix i j c) x = Function.update 0 i (c * x j)
theorem
Matrix.matrix_eq_sum_std_basis
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
[Fintype m]
[Fintype n]
(x : Matrix m n α)
:
x = Finset.sum Finset.univ fun (i : m) => Finset.sum Finset.univ fun (j : n) => Matrix.stdBasisMatrix i j (x i j)
theorem
Matrix.std_basis_eq_basis_mul_basis
{m : Type u_2}
{n : Type u_3}
[DecidableEq m]
[DecidableEq n]
(i : m)
(j : n)
:
Matrix.stdBasisMatrix i j 1 = Matrix.vecMulVec (fun (i' : m) => if i = i' then 1 else 0) fun (j' : n) => if j = j' then 1 else 0
theorem
Matrix.induction_on'
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
[Finite m]
[Finite n]
{P : Matrix m n α → Prop}
(M : Matrix m n α)
(h_zero : P 0)
(h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q))
(h_std_basis : ∀ (i : m) (j : n) (x : α), P (Matrix.stdBasisMatrix i j x))
:
P M
theorem
Matrix.induction_on
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
[Finite m]
[Finite n]
[Nonempty m]
[Nonempty n]
{P : Matrix m n α → Prop}
(M : Matrix m n α)
(h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q))
(h_std_basis : ∀ (i : m) (j : n) (x : α), P (Matrix.stdBasisMatrix i j x))
:
P M
@[simp]
theorem
Matrix.StdBasisMatrix.apply_same
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
(c : α)
:
Matrix.stdBasisMatrix i j c i j = c
@[simp]
theorem
Matrix.StdBasisMatrix.apply_of_ne
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(j : n)
(c : α)
(i' : m)
(j' : n)
(h : ¬(i = i' ∧ j = j'))
:
Matrix.stdBasisMatrix i j c i' j' = 0
@[simp]
theorem
Matrix.StdBasisMatrix.apply_of_row_ne
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
{i : m}
{i' : m}
(hi : i ≠ i')
(j : n)
(j' : n)
(a : α)
:
Matrix.stdBasisMatrix i j a i' j' = 0
@[simp]
theorem
Matrix.StdBasisMatrix.apply_of_col_ne
{m : Type u_2}
{n : Type u_3}
{α : Type u_5}
[DecidableEq m]
[DecidableEq n]
[Semiring α]
(i : m)
(i' : m)
{j : n}
{j' : n}
(hj : j ≠ j')
(a : α)
:
Matrix.stdBasisMatrix i j a i' j' = 0
@[simp]
theorem
Matrix.StdBasisMatrix.diag_zero
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
(h : j ≠ i)
:
Matrix.diag (Matrix.stdBasisMatrix i j c) = 0
@[simp]
theorem
Matrix.StdBasisMatrix.diag_same
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(c : α)
:
Matrix.diag (Matrix.stdBasisMatrix i i c) = Pi.single i c
@[simp]
theorem
Matrix.StdBasisMatrix.trace_zero
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(h : j ≠ i)
:
Matrix.trace (Matrix.stdBasisMatrix i j c) = 0
@[simp]
theorem
Matrix.StdBasisMatrix.trace_eq
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(c : α)
[Fintype n]
:
Matrix.trace (Matrix.stdBasisMatrix i i c) = c
@[simp]
theorem
Matrix.StdBasisMatrix.mul_left_apply_same
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(b : n)
(M : Matrix n n α)
:
(Matrix.stdBasisMatrix i j c * M) i b = c * M j b
@[simp]
theorem
Matrix.StdBasisMatrix.mul_right_apply_same
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(a : n)
(M : Matrix n n α)
:
(M * Matrix.stdBasisMatrix i j c) a j = M a i * c
@[simp]
theorem
Matrix.StdBasisMatrix.mul_left_apply_of_ne
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(a : n)
(b : n)
(h : a ≠ i)
(M : Matrix n n α)
:
(Matrix.stdBasisMatrix i j c * M) a b = 0
@[simp]
theorem
Matrix.StdBasisMatrix.mul_right_apply_of_ne
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(a : n)
(b : n)
(hbj : b ≠ j)
(M : Matrix n n α)
:
(M * Matrix.stdBasisMatrix i j c) a b = 0
@[simp]
theorem
Matrix.StdBasisMatrix.mul_same
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
(k : n)
(d : α)
:
Matrix.stdBasisMatrix i j c * Matrix.stdBasisMatrix j k d = Matrix.stdBasisMatrix i k (c * d)
@[simp]
theorem
Matrix.StdBasisMatrix.mul_of_ne
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
(i : n)
(j : n)
(c : α)
[Fintype n]
{k : n}
{l : n}
(h : j ≠ k)
(d : α)
:
Matrix.stdBasisMatrix i j c * Matrix.stdBasisMatrix k l d = 0
theorem
Matrix.row_eq_zero_of_commute_stdBasisMatrix
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
[Fintype n]
{i : n}
{j : n}
{k : n}
{M : Matrix n n α}
(hM : Commute (Matrix.stdBasisMatrix i j 1) M)
(hkj : k ≠ j)
:
M j k = 0
theorem
Matrix.col_eq_zero_of_commute_stdBasisMatrix
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
[Fintype n]
{i : n}
{j : n}
{k : n}
{M : Matrix n n α}
(hM : Commute (Matrix.stdBasisMatrix i j 1) M)
(hki : k ≠ i)
:
M k i = 0
theorem
Matrix.diag_eq_of_commute_stdBasisMatrix
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
[Fintype n]
{i : n}
{j : n}
{M : Matrix n n α}
(hM : Commute (Matrix.stdBasisMatrix i j 1) M)
:
M i i = M j j
theorem
Matrix.mem_range_scalar_of_commute_stdBasisMatrix
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
[Fintype n]
{M : Matrix n n α}
(hM : Pairwise fun (i j : n) => Commute (Matrix.stdBasisMatrix i j 1) M)
:
M ∈ Set.range ⇑(Matrix.scalar n)
M is a scalar matrix if it commutes with every non-diagonal stdBasisMatrix.
theorem
Matrix.mem_range_scalar_iff_commute_stdBasisMatrix
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
[Fintype n]
{M : Matrix n n α}
:
M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (Matrix.stdBasisMatrix i j 1) M
theorem
Matrix.mem_range_scalar_iff_commute_stdBasisMatrix'
{n : Type u_3}
{α : Type u_5}
[DecidableEq n]
[Semiring α]
[Fintype n]
{M : Matrix n n α}
:
M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (i j : n), Commute (Matrix.stdBasisMatrix i j 1) M
M is a scalar matrix if and only if it commutes with every stdBasisMatrix.