partial equivalences for matrices

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

The following important properties of this function are proved toMatrix_trans : (f.trans g).toMatrix = f.toMatrix * g.toMatrix toMatrix_symm : f.symm.toMatrix = f.toMatrixᵀ toMatrix_refl : (PEquiv.refl n).toMatrix = 1 toMatrix_bot : ⊥.toMatrix = 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)).toMatrix 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 ᵀ for Matrix.transpose.

def PEquiv.toMatrix {m : Type u_3} {n : Type u_4} {α : Type v} [DecidableEq n] [Zero α] [One α] (f : m ≃. n) : Matrix m n α

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

Equations

• PEquiv.toMatrix f = ↑Matrix.of fun i j => if j ∈ ↑f i then 1 else 0

@[simp]

theorem PEquiv.toMatrix_apply {m : Type u_3} {n : Type u_4} {α : Type v} [DecidableEq n] [Zero α] [One α] (f : m ≃. n) (i : m) (j : n) : PEquiv.toMatrix f i j = if j ∈ ↑f i then 1 else 0

theorem PEquiv.mul_matrix_apply {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type v} [Fintype m] [DecidableEq m] [Semiring α] (f : l ≃. m) (M : Matrix m n α) (i : l) (j : n) : (Matrix l m α * Matrix m n α) (Matrix l n α) Matrix.instHMulMatrixMatrixMatrix (PEquiv.toMatrix f) M i j = Option.casesOn (↑f i) 0 fun fi => M fi j

theorem PEquiv.toMatrix_symm {m : Type u_3} {n : Type u_4} {α : Type v} [DecidableEq m] [DecidableEq n] [Zero α] [One α] (f : m ≃. n) : PEquiv.toMatrix (PEquiv.symm f) = Matrix.transpose (PEquiv.toMatrix f)

@[simp]

theorem PEquiv.toMatrix_refl {n : Type u_4} {α : Type v} [DecidableEq n] [Zero α] [One α] : PEquiv.toMatrix (PEquiv.refl n) = 1

theorem PEquiv.matrix_mul_apply {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type v} [Fintype m] [Semiring α] [DecidableEq n] (M : Matrix l m α) (f : m ≃. n) (i : l) (j : n) : (Matrix l m α * Matrix m n α) (Matrix l n α) Matrix.instHMulMatrixMatrixMatrix M (PEquiv.toMatrix f) i j = Option.casesOn (↑(PEquiv.symm f) j) 0 fun fj => M i fj

theorem PEquiv.toPEquiv_mul_matrix {m : Type u_3} {n : Type u_4} {α : Type v} [Fintype m] [DecidableEq m] [Semiring α] (f : m ≃ m) (M : Matrix m n α) : PEquiv.toMatrix (Equiv.toPEquiv f) * M = fun i => M (↑f i)

theorem PEquiv.mul_toPEquiv_toMatrix {m : Type u_5} {n : Type u_6} {α : Type u_7} [Fintype n] [DecidableEq n] [Semiring α] (f : n ≃ n) (M : Matrix m n α) : M * PEquiv.toMatrix (Equiv.toPEquiv f) = Matrix.submatrix M id ↑f.symm

theorem PEquiv.toMatrix_trans {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type v} [Fintype m] [DecidableEq m] [DecidableEq n] [Semiring α] (f : l ≃. m) (g : m ≃. n) : PEquiv.toMatrix (PEquiv.trans f g) = PEquiv.toMatrix f * PEquiv.toMatrix g

@[simp]

theorem PEquiv.toMatrix_bot {m : Type u_3} {n : Type u_4} {α : Type v} [DecidableEq n] [Zero α] [One α] : PEquiv.toMatrix ⊥ = 0

theorem PEquiv.toMatrix_injective {m : Type u_3} {n : Type u_4} {α : Type v} [DecidableEq n] [MonoidWithZero α] [Nontrivial α] : Function.Injective PEquiv.toMatrix

theorem PEquiv.toMatrix_swap {n : Type u_4} {α : Type v} [DecidableEq n] [Ring α] (i : n) (j : n) : PEquiv.toMatrix (Equiv.toPEquiv (Equiv.swap i j)) = 1 - PEquiv.toMatrix (PEquiv.single i i) - PEquiv.toMatrix (PEquiv.single j j) + PEquiv.toMatrix (PEquiv.single i j) + PEquiv.toMatrix (PEquiv.single j i)

@[simp]

theorem PEquiv.single_mul_single {k : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type v} [Fintype n] [DecidableEq k] [DecidableEq m] [DecidableEq n] [Semiring α] (a : m) (b : n) (c : k) : PEquiv.toMatrix (PEquiv.single a b) * PEquiv.toMatrix (PEquiv.single b c) = PEquiv.toMatrix (PEquiv.single a c)

theorem PEquiv.single_mul_single_of_ne {k : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type v} [Fintype n] [DecidableEq n] [DecidableEq k] [DecidableEq m] [Semiring α] {b₁ : n} {b₂ : n} (hb : b₁ ≠ b₂) (a : m) (c : k) : PEquiv.toMatrix (PEquiv.single a b₁) * PEquiv.toMatrix (PEquiv.single b₂ c) = 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] [DecidableEq n] [DecidableEq k] [DecidableEq m] [Semiring α] (a : m) (b : n) (c : k) (M : Matrix k l α) : PEquiv.toMatrix (PEquiv.single a b) * (PEquiv.toMatrix (PEquiv.single b c) * M) = PEquiv.toMatrix (PEquiv.single a c) * M

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_toPEquiv_toMatrix {n : Type u_4} {α : Type v} [DecidableEq n] [Zero α] [One α] (σ : n ≃ n) (i : n) (j : n) : PEquiv.toMatrix (Equiv.toPEquiv σ) i j = OfNat.ofNat (Matrix n n α) 1 One.toOfNat1 (↑σ i) j

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