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.

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

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 ⬝ 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)ᵀ

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 ⬝ 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 ⬝ M = λ (i : m), M (⇑f i)

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 ⬝ 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 ⬝ (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 ⬝ (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 ⬝ ((pequiv.single b c).to_matrix ⬝ M) = (pequiv.single a c).to_matrix ⬝ 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.