Documentation

Mathlib.LinearAlgebra.Matrix.Swap

Swap matrices #

A swap matrix indexed by i and j is the matrix that, when multiplying another matrix on the left (resp. on the right), swaps the i-th row with the j-th row (resp. the i-th column with the j-th column).

Swap matrices are a special case of elementary matrices. For transvections see Mathlib/LinearAlgebra/Matrix/Transvection.lean.

Implementation detail #

This is a thin wrapper around (Equiv.swap i j).permMatrix.

source
🔸 coverage
def Matrix.swap (R : Type u_1) {n : Type u_2} [Zero R] [One R] [DecidableEq n] (i j : n) :
Matrix n n R

The swap matrix swap R i j is the identity matrix with the i-th and j-th rows modified such that multiplying by it on the left (resp. right) corresponds to swapping the i-th and j-th row (resp. column).

Instances For
    source
    📐 coverage
    theorem Matrix.swap_comm {R : Type u_1} {n : Type u_2} [Zero R] [One R] [DecidableEq n] (i j : n) :
    swap R i j = swap R j i
    source
    📐 coverage
    @[simp]
    theorem Matrix.transpose_swap {R : Type u_1} {n : Type u_2} [Zero R] [One R] [DecidableEq n] (i j : n) :
    (swap R i j).transpose = swap R i j
    source
    📐 coverage
    theorem Matrix.isSymm_swap {R : Type u_1} {n : Type u_2} [Zero R] [One R] [DecidableEq n] (i j : n) :
    (swap R i j).IsSymm
    source
    📐 coverage
    @[simp]
    theorem Matrix.conjTranspose_swap {n : Type u_2} [DecidableEq n] {R : Type u_3} [NonAssocSemiring R] [StarRing R] (i j : n) :
    (swap R i j).conjTranspose = swap R i j
    source
    📐 coverage
    @[simp]
    theorem Matrix.map_swap {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] {S : Type u_4} [NonAssocSemiring S] (f : R →+* S) (i j : n) :
    (swap R i j).map ⇑f = swap S i j
    source
    📐 coverage
    theorem Matrix.swap_mulVec {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : n → R) :
    (swap R i j).mulVec a = a ∘ ⇑(Equiv.swap i j)
    source
    📐 coverage
    theorem Matrix.vecMul_swap {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : n → R) :
    vecMul a (swap R i j) = a ∘ ⇑(Equiv.swap i j)
    source
    📐 coverage
    @[simp]
    theorem Matrix.swap_mulVec_apply {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : n → R) :
    (swap R i j).mulVec a i = a j
    source
    📐 coverage
    @[simp]
    theorem Matrix.vecMul_swap_apply {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : n → R) :
    vecMul a (swap R i j) i = a j
    source
    📐 coverage
    @[simp]
    theorem Matrix.swap_mul_apply_left {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : m) (g : Matrix n m R) :
    (swap R i j * g) i a = g j a

    Multiplying with swap R i j on the left swaps the i-th row with the j-th row.

    source
    📐 coverage
    @[simp]
    theorem Matrix.swap_mul_apply_right {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : m) (g : Matrix n m R) :
    (swap R i j * g) j a = g i a

    Multiplying with swap R i j on the left swaps the j-th row with the i-th row.

    source
    📐 coverage
    theorem Matrix.swap_mul_of_ne {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] {i j a : n} {b : m} (hai : a ≠ i) (haj : a ≠ j) (g : Matrix n m R) :
    (swap R i j * g) a b = g a b
    source
    📐 coverage
    @[simp]
    theorem Matrix.mul_swap_apply_left {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : m) (g : Matrix m n R) :
    (g * swap R i j) a i = g a j

    Multiplying with swap R i j on the right swaps the i-th column with the j-th column.

    source
    📐 coverage
    @[simp]
    theorem Matrix.mul_swap_apply_right {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) (a : m) (g : Matrix m n R) :
    (g * swap R i j) a j = g a i

    Multiplying with swap R i j on the right swaps the j-th column with the i-th column.

    source
    📐 coverage
    theorem Matrix.mul_swap_of_ne {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [DecidableEq n] [Fintype n] {i j b : n} {a : m} (hbi : b ≠ i) (hbj : b ≠ j) (g : Matrix m n R) :
    (g * swap R i j) a b = g a b
    source
    📐 coverage
    theorem Matrix.swap_mul_self {R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] [Fintype n] (i j : n) :
    swap R i j * swap R i j = 1

    Swap matrices are self inverse.

    source
    🔸 coverage
    def Matrix.GeneralLinearGroup.swap (R : Type u_1) {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (i j : n) :
    GL n R

    Matrix.swap as an element of GL n R.

    Instances For
      source
      📐 coverage
      @[simp]
      theorem Matrix.GeneralLinearGroup.val_inv_swap (R : Type u_1) {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (i j : n) :
      ↑(swap R i j)⁻¹ = Matrix.swap R i j
      source
      📐 coverage
      @[simp]
      theorem Matrix.GeneralLinearGroup.val_swap (R : Type u_1) {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] (i j : n) :
      ↑(swap R i j) = Matrix.swap R i j
      source
      📐 coverage
      @[simp]
      theorem Matrix.GeneralLinearGroup.map_swap {R : Type u_1} {n : Type u_2} [CommRing R] [DecidableEq n] [Fintype n] {S : Type u_3} [CommRing S] (f : R →+* S) (i j : n) :
      (map f) (swap R i j) = swap S i j