# mathlibdocumentation

data.matrix.pequiv

# partial equivalences for matrices #

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.

def pequiv.to_matrix {m : Type u_3} {n : Type u_4} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) :
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
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 : n α) (i : l) (j : n) :
f.to_matrix.mul M i j = (f i).cases_on 0 (λ (fi : m), M fi j)
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) :
@[simp]
theorem pequiv.to_matrix_refl {n : Type u_4} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
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 : 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)
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 : n α) :
= λ (i : m), M (f i)
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) :
@[simp]
theorem pequiv.to_matrix_bot {m : Type u_3} {n : Type u_4} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
theorem pequiv.to_matrix_injective {m : Type u_3} {n : Type u_4} {α : Type v} [decidable_eq n] [nontrivial α] :
theorem pequiv.to_matrix_swap {n : Type u_4} {α : Type v} [decidable_eq n] [ring α] (i j : n) :
@[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) :
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) :
b₁).to_matrix.mul c).to_matrix = 0
@[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 : l α) :

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

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) :
j = 1 (σ i) j

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