Documentation

Mathlib.Data.Matrix.Basis

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.

source
def Matrix.stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (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
source
theorem Matrix.stdBasisMatrix_eq_of_single_single {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
stdBasisMatrix i j a = of (Pi.single i (Pi.single j a))
source
@[simp]
theorem Matrix.of_symm_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
of.symm (stdBasisMatrix i j a) = Pi.single i (Pi.single j a)
source
@[simp]
theorem Matrix.smul_stdBasisMatrix {m : Type u_2} {n : Type u_3} {R : Type u_5} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] [SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α) :
r • stdBasisMatrix i j a = stdBasisMatrix i j (r • a)
source
@[simp]
theorem Matrix.stdBasisMatrix_zero {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) :
stdBasisMatrix i j 0 = 0
source
@[simp]
theorem Matrix.transpose_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) :
(stdBasisMatrix i j a).transpose = stdBasisMatrix j i a
source
@[simp]
theorem Matrix.map_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) {β : Type u_8} [Zero β] {F : Type u_9} [FunLike F α β] [ZeroHomClass F α β] (f : F) :
(stdBasisMatrix i j a).map ⇑f = stdBasisMatrix i j (f a)
source
theorem Matrix.stdBasisMatrix_add {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [AddZeroClass α] (i : m) (j : n) (a b : α) :
stdBasisMatrix i j (a + b) = stdBasisMatrix i j a + stdBasisMatrix i j b
source
theorem Matrix.mulVec_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [NonUnitalNonAssocSemiring α] [Fintype m] (i : n) (j : m) (c : α) (x : m → α) :
(stdBasisMatrix i j c).mulVec x = Function.update 0 i (c * x j)
source
theorem Matrix.matrix_eq_sum_stdBasisMatrix {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] [Fintype m] [Fintype n] (x : Matrix m n α) :
x = ∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)
source
theorem Matrix.stdBasisMatrix_eq_single_vecMulVec_single {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [MulZeroOneClass α] (i : m) (j : n) :
stdBasisMatrix i j 1 = vecMulVec (Pi.single i 1) (Pi.single j 1)
source
theorem Matrix.induction_on' {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] [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 (stdBasisMatrix i j x)) :
P M
source
theorem Matrix.induction_on {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] [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 (stdBasisMatrix i j x)) :
P M
source
def Matrix.stdBasisMatrixAddMonoidHom {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] (i : m) (j : n) :
α →+ Matrix m n α

Matrix.stdBasisMatrix as a bundled additive map.

Equations
source
@[simp]
theorem Matrix.stdBasisMatrixAddMonoidHom_apply {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [AddCommMonoid α] (i : m) (j : n) (a : α) :
(stdBasisMatrixAddMonoidHom i j) a = stdBasisMatrix i j a
source
def Matrix.stdBasisMatrixLinearMap {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_6} [DecidableEq m] [DecidableEq n] [Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) :
α →ₗ[R] Matrix m n α

Matrix.stdBasisMatrix as a bundled linear map.

Equations
source
@[simp]
theorem Matrix.stdBasisMatrixLinearMap_apply {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_6} [DecidableEq m] [DecidableEq n] [Semiring R] [AddCommMonoid α] [Module R α] (i : m) (j : n) (a✝ : α) :
(stdBasisMatrixLinearMap R i j) a✝ = stdBasisMatrix i j a✝
source
theorem Matrix.ext_addMonoidHom {m : Type u_2} {n : Type u_3} {α : Type u_6} {β : Type u_7} [DecidableEq m] [DecidableEq n] [Finite m] [Finite n] [AddCommMonoid α] [AddCommMonoid β] ⦃f g : Matrix m n α →+ β⦄ (h : ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)) :
f = g

Additive maps from finite matrices are equal if they agree on the standard basis.

See note [partially-applied ext lemmas].

source
theorem Matrix.ext_addMonoidHom_iff {m : Type u_2} {n : Type u_3} {α : Type u_6} {β : Type u_7} [DecidableEq m] [DecidableEq n] [Finite m] [Finite n] [AddCommMonoid α] [AddCommMonoid β] {f g : Matrix m n α →+ β} :
f = g ↔ ∀ (i : m) (j : n), f.comp (stdBasisMatrixAddMonoidHom i j) = g.comp (stdBasisMatrixAddMonoidHom i j)
source
theorem Matrix.ext_linearMap {m : Type u_2} {n : Type u_3} (R : Type u_5) {α : Type u_6} {β : Type u_7} [DecidableEq m] [DecidableEq n] [Finite m] [Finite n] [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] ⦃f g : Matrix m n α →ₗ[R] β⦄ (h : ∀ (i : m) (j : n), f ∘ₗ stdBasisMatrixLinearMap R i j = g ∘ₗ stdBasisMatrixLinearMap R i j) :
f = g

Linear maps from finite matrices are equal if they agree on the standard basis.

See note [partially-applied ext lemmas].

source
theorem Matrix.ext_linearMap_iff {m : Type u_2} {n : Type u_3} {R : Type u_5} {α : Type u_6} {β : Type u_7} [DecidableEq m] [DecidableEq n] [Finite m] [Finite n] [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] {f g : Matrix m n α →ₗ[R] β} :
f = g ↔ ∀ (i : m) (j : n), f ∘ₗ stdBasisMatrixLinearMap R i j = g ∘ₗ stdBasisMatrixLinearMap R i j
source
@[simp]
theorem Matrix.StdBasisMatrix.apply_same {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (c : α) :
stdBasisMatrix i j c i j = c
source
@[simp]
theorem Matrix.StdBasisMatrix.apply_of_ne {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (c : α) (i' : m) (j' : n) (h : ¬(i = i' ∧ j = j')) :
stdBasisMatrix i j c i' j' = 0
source
@[simp]
theorem Matrix.StdBasisMatrix.apply_of_row_ne {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] {i i' : m} (hi : i ≠ i') (j j' : n) (a : α) :
stdBasisMatrix i j a i' j' = 0
source
@[simp]
theorem Matrix.StdBasisMatrix.apply_of_col_ne {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i i' : m) {j j' : n} (hj : j ≠ j') (a : α) :
stdBasisMatrix i j a i' j' = 0
source
@[simp]
theorem Matrix.StdBasisMatrix.diag_zero {n : Type u_3} {α : Type u_6} [DecidableEq n] [Zero α] (i j : n) (c : α) (h : j ≠ i) :
(stdBasisMatrix i j c).diag = 0
source
@[simp]
theorem Matrix.StdBasisMatrix.diag_same {n : Type u_3} {α : Type u_6} [DecidableEq n] [Zero α] (i : n) (c : α) :
(stdBasisMatrix i i c).diag = Pi.single i c
source
@[simp]
theorem Matrix.StdBasisMatrix.mul_left_apply_same {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq l] [DecidableEq m] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (b : n) (M : Matrix m n α) :
(stdBasisMatrix i j c * M) i b = c * M j b
source
@[simp]
theorem Matrix.StdBasisMatrix.mul_right_apply_same {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : m) (j : n) (a : l) (M : Matrix l m α) :
(M * stdBasisMatrix i j c) a j = M a i * c
source
@[simp]
theorem Matrix.StdBasisMatrix.mul_left_apply_of_ne {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq l] [DecidableEq m] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (a : l) (b : n) (h : a ≠ i) (M : Matrix m n α) :
(stdBasisMatrix i j c * M) a b = 0
source
@[simp]
theorem Matrix.StdBasisMatrix.mul_right_apply_of_ne {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : m) (j : n) (a : l) (b : n) (hbj : b ≠ j) (M : Matrix l m α) :
(M * stdBasisMatrix i j c) a b = 0
source
@[simp]
theorem Matrix.StdBasisMatrix.mul_same {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq l] [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j : m) (k : n) (d : α) :
stdBasisMatrix i j c * stdBasisMatrix j k d = stdBasisMatrix i k (c * d)
source
@[simp]
theorem Matrix.StdBasisMatrix.stdBasisMatrix_mul_mul_stdBasisMatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_6} [DecidableEq l] [DecidableEq m] [DecidableEq n] [DecidableEq o] [Fintype m] [NonUnitalNonAssocSemiring α] [Fintype n] (i : l) (i' : m) (j' : n) (j : o) (a : α) (x : Matrix m n α) (b : α) :
stdBasisMatrix i i' a * x * stdBasisMatrix j' j b = stdBasisMatrix i j (a * x i' j' * b)
source
@[simp]
theorem Matrix.StdBasisMatrix.mul_of_ne {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq l] [DecidableEq m] [DecidableEq n] [Fintype m] [NonUnitalNonAssocSemiring α] (c : α) (i : l) (j k : m) {l✝ : n} (h : j ≠ k) (d : α) :
stdBasisMatrix i j c * stdBasisMatrix k l✝ d = 0
source
theorem Matrix.row_eq_zero_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_6} [DecidableEq n] [Fintype n] [Semiring α] {i j k : n} {M : Matrix n n α} (hM : Commute (stdBasisMatrix i j 1) M) (hkj : k ≠ j) :
M j k = 0
source
theorem Matrix.col_eq_zero_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_6} [DecidableEq n] [Fintype n] [Semiring α] {i j k : n} {M : Matrix n n α} (hM : Commute (stdBasisMatrix i j 1) M) (hki : k ≠ i) :
M k i = 0
source
theorem Matrix.diag_eq_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_6} [DecidableEq n] [Fintype n] [Semiring α] {i j : n} {M : Matrix n n α} (hM : Commute (stdBasisMatrix i j 1) M) :
M i i = M j j
source
theorem Matrix.mem_range_scalar_of_commute_stdBasisMatrix {n : Type u_3} {α : Type u_6} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} (hM : Pairwise fun (i j : n) => Commute (stdBasisMatrix i j 1) M) :
M ∈ Set.range ⇑(scalar n)

M is a scalar matrix if it commutes with every non-diagonal stdBasisMatrix.

source
theorem Matrix.mem_range_scalar_iff_commute_stdBasisMatrix {n : Type u_3} {α : Type u_6} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} :
M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M
source
theorem Matrix.mem_range_scalar_iff_commute_stdBasisMatrix' {n : Type u_3} {α : Type u_6} [DecidableEq n] [Fintype n] [Semiring α] {M : Matrix n n α} :
M ∈ Set.range ⇑(scalar n) ↔ ∀ (i j : n), Commute (stdBasisMatrix i j 1) M

M is a scalar matrix if and only if it commutes with every stdBasisMatrix.