Documentation

Mathlib.LinearAlgebra.Matrix.Permutation

Permutation matrices #

This file defines the matrix associated with a permutation

Main definitions #

Main results #

source
@[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

Equations
Instances For
    source
    @[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 σ⁻¹
    source
    @[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 σ⁻¹
    source
    @[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.

    source
    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.

    source
    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 ∘ ⇑σ
    source
    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 σ)
    source
    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.

    source
    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.