mathlib3 documentation

data.matrix.pequiv

partial equivalences for matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Using partial equivalences to represent matrices. This file introduces the function pequiv.to_matrix, which returns a matrix containing ones and zeros. For any partial equivalence f, f.to_matrix i j = 1 ↔ f i = some j.

The following important properties of this function are proved to_matrix_trans : (f.trans g).to_matrix = f.to_matrix ⬝ g.to_matrix to_matrix_symm : f.symm.to_matrix = f.to_matrixᵀ to_matrix_refl : (pequiv.refl n).to_matrix = 1 to_matrix_bot : ⊥.to_matrix = 0

This theory gives the matrix representation of projection linear maps, and their right inverses. For example, the matrix (single (0 : fin 1) (i : fin n)).to_matrix corresponds to the ith projection map from R^n to R.

Any injective function fin m → fin n gives rise to a pequiv, whose matrix is the projection map from R^m → R^n represented by the same function. The transpose of this matrix is the right inverse of this map, sending anything not in the image to zero.

notations #

This file uses the notation ⬝ for matrix.mul and ᵀ for matrix.transpose.

source
def pequiv.to_matrix {m : Type u_3} {n : Type u_4} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) :
matrix m n α

to_matrix returns a matrix containing ones and zeros. f.to_matrix i j is 1 if f i = some j and 0 otherwise

Equations
source
@[simp]
theorem pequiv.to_matrix_apply {m : Type u_3} {n : Type u_4} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) (i : m) (j : n) :
f.to_matrix i j = ite (j ∈ ⇑f i) 1 0
source
theorem pequiv.mul_matrix_apply {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type v} [fintype m] [decidable_eq m] [semiring α] (f : l ≃. m) (M : matrix m n α) (i : l) (j : n) :
f.to_matrix.mul M i j = (⇑f i).cases_on 0 (λ (fi : m), M fi j)
source
theorem pequiv.to_matrix_symm {m : Type u_3} {n : Type u_4} {α : Type v} [decidable_eq m] [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) :
f.symm.to_matrix = f.to_matrix.transpose
source
@[simp]
theorem pequiv.to_matrix_refl {n : Type u_4} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
(pequiv.refl n).to_matrix = 1
source
theorem pequiv.matrix_mul_apply {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type v} [fintype m] [semiring α] [decidable_eq n] (M : matrix l m α) (f : m ≃. n) (i : l) (j : n) :
M.mul f.to_matrix i j = (⇑(f.symm) j).cases_on 0 (λ (fj : m), M i fj)
source
theorem pequiv.to_pequiv_mul_matrix {m : Type u_3} {n : Type u_4} {α : Type v} [fintype m] [decidable_eq m] [semiring α] (f : m ≃ m) (M : matrix m n α) :
f.to_pequiv.to_matrix.mul M = λ (i : m), M (⇑f i)
source
theorem pequiv.mul_to_pequiv_to_matrix {m : Type u_1} {n : Type u_2} {α : Type u_3} [fintype n] [decidable_eq n] [semiring α] (f : n ≃ n) (M : matrix m n α) :
M.mul f.to_pequiv.to_matrix = M.submatrix id ⇑(f.symm)
source
theorem pequiv.to_matrix_trans {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type v} [fintype m] [decidable_eq m] [decidable_eq n] [semiring α] (f : l ≃. m) (g : m ≃. n) :
(f.trans g).to_matrix = f.to_matrix.mul g.to_matrix
source
@[simp]
theorem pequiv.to_matrix_bot {m : Type u_3} {n : Type u_4} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
⊥.to_matrix = 0
source
theorem pequiv.to_matrix_injective {m : Type u_3} {n : Type u_4} {α : Type v} [decidable_eq n] [monoid_with_zero α] [nontrivial α] :
function.injective pequiv.to_matrix
source
theorem pequiv.to_matrix_swap {n : Type u_4} {α : Type v} [decidable_eq n] [ring α] (i j : n) :
(equiv.to_pequiv (equiv.swap i j)).to_matrix = 1 - (pequiv.single i i).to_matrix - (pequiv.single j j).to_matrix + (pequiv.single i j).to_matrix + (pequiv.single j i).to_matrix
source
@[simp]
theorem pequiv.single_mul_single {k : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type v} [fintype n] [decidable_eq k] [decidable_eq m] [decidable_eq n] [semiring α] (a : m) (b : n) (c : k) :
(pequiv.single a b).to_matrix.mul (pequiv.single b c).to_matrix = (pequiv.single a c).to_matrix
source
theorem pequiv.single_mul_single_of_ne {k : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type v} [fintype n] [decidable_eq n] [decidable_eq k] [decidable_eq m] [semiring α] {b₁ b₂ : n} (hb : b₁ ≠ b₂) (a : m) (c : k) :
(pequiv.single a b₁).to_matrix.mul (pequiv.single b₂ c).to_matrix = 0
source
@[simp]
theorem pequiv.single_mul_single_right {k : Type u_1} {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type v} [fintype n] [fintype k] [decidable_eq n] [decidable_eq k] [decidable_eq m] [semiring α] (a : m) (b : n) (c : k) (M : matrix k l α) :
(pequiv.single a b).to_matrix.mul ((pequiv.single b c).to_matrix.mul M) = (pequiv.single a c).to_matrix.mul M

Restatement of single_mul_single, which will simplify expressions in simp normal form, when associativity may otherwise need to be carefully applied.

source
theorem pequiv.equiv_to_pequiv_to_matrix {n : Type u_4} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] (σ : n ≃ n) (i j : n) :
σ.to_pequiv.to_matrix i j = 1 (⇑σ i) j

We can also define permutation matrices by permuting the rows of the identity matrix.