Permutation matrices

This file defines the matrix associated with a permutation

Main definitions

• Equiv.Perm.permMatrix: the permutation matrix associated with an Equiv.Perm

Main results

• Matrix.det_permutation: the determinant is the sign of the permutation
• Matrix.trace_permutation: the trace is the number of fixed points of the permutation

@[reducible, inline]

abbrev Equiv.Perm.permMatrix {n : Type u_1} (R : Type u_2) [DecidableEq n] (σ : Perm n) [Zero R] [One R] : Matrix n n R

the permutation matrix associated with an Equiv.Perm

@[simp]

theorem Matrix.permMatrix_refl {n : Type u_1} {R : Type u_2} [DecidableEq n] [Zero R] [One R] : Equiv.Perm.permMatrix R (Equiv.refl n) = 1

@[simp]

theorem Matrix.permMatrix_one {n : Type u_1} {R : Type u_2} [DecidableEq n] [Zero R] [One R] : Equiv.Perm.permMatrix R 1 = 1

@[simp]

theorem Matrix.transpose_permMatrix {n : Type u_1} {R : Type u_2} [DecidableEq n] (σ : Equiv.Perm n) [Zero R] [One R] : (Equiv.Perm.permMatrix R σ).transpose = Equiv.Perm.permMatrix R σ⁻¹

@[simp]

theorem Matrix.conjTranspose_permMatrix {n : Type u_1} {R : Type u_2} [DecidableEq n] (σ : Equiv.Perm n) [NonAssocSemiring R] [StarRing R] : (Equiv.Perm.permMatrix R σ).conjTranspose = Equiv.Perm.permMatrix R σ⁻¹

@[simp]

theorem Matrix.det_permutation {n : Type u_1} {R : Type u_2} [DecidableEq n] (σ : Equiv.Perm n) [Fintype n] [CommRing R] : (Equiv.Perm.permMatrix R σ).det = ↑↑(Equiv.Perm.sign σ)

The determinant of a permutation matrix equals its sign.

theorem Matrix.trace_permutation {n : Type u_1} {R : Type u_2} [DecidableEq n] (σ : Equiv.Perm n) [Fintype n] [AddCommMonoidWithOne R] : (Equiv.Perm.permMatrix R σ).trace = ↑(Function.fixedPoints ⇑σ).ncard

The trace of a permutation matrix equals the number of fixed points.

theorem Matrix.permMatrix_mulVec {n : Type u_1} {R : Type u_2} [DecidableEq n] (σ : Equiv.Perm n) [Fintype n] {v : n → R} [CommRing R] : (Equiv.Perm.permMatrix R σ).mulVec v = v ∘ ⇑σ

theorem Matrix.vecMul_permMatrix {n : Type u_1} {R : Type u_2} [DecidableEq n] (σ : Equiv.Perm n) [Fintype n] {v : n → R} [CommRing R] : vecMul v (Equiv.Perm.permMatrix R σ) = v ∘ ⇑(Equiv.symm σ)

@[simp]

theorem Matrix.permMatrix_mul {n : Type u_1} {R : Type u_2} [DecidableEq n] (σ τ : Equiv.Perm n) [Fintype n] [NonAssocSemiring R] : Equiv.Perm.permMatrix R (σ * τ) = Equiv.Perm.permMatrix R τ * Equiv.Perm.permMatrix R σ

def Matrix.permMatrixHom {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [NonAssocSemiring R] : Equiv.Perm n →* Matrix n n R

permMatrix as a homomorphism.

@[simp]

theorem Matrix.permMatrixHom_apply {n : Type u_1} {R : Type u_2} [DecidableEq n] [Fintype n] [NonAssocSemiring R] (σ : Equiv.Perm n) : permMatrixHom σ = Equiv.Perm.permMatrix R σ⁻¹

theorem Matrix.permMatrix_l2_opNorm_le {n : Type u_1} [DecidableEq n] (σ : Equiv.Perm n) [Fintype n] {𝕜 : Type u_3} [RCLike 𝕜] : ‖Equiv.Perm.permMatrix 𝕜 σ‖ ≤ 1

The l2-operator norm of a permutation matrix is bounded above by 1. See Matrix.permMatrix_l2_opNorm_eq for the equality statement assuming the matrix is nonempty.

theorem Matrix.permMatrix_l2_opNorm_eq {n : Type u_1} [DecidableEq n] (σ : Equiv.Perm n) [Fintype n] {𝕜 : Type u_3} [RCLike 𝕜] [Nonempty n] : ‖Equiv.Perm.permMatrix 𝕜 σ‖ = 1

The l2-operator norm of a nonempty permutation matrix is equal to 1. Note that this is not true for the empty case, since the empty matrix has l2-operator norm 0. See Matrix.permMatrix_l2_opNorm_le for the inequality version of the empty case.