Transvections

Transvections are matrices of the form 1 + stdBasisMatrix i j c, where stdBasisMatrix i j c is the basic matrix with a c at position (i, j). Multiplying by such a transvection on the left (resp. on the right) amounts to adding c times the j-th row to the i-th row (resp c times the i-th column to the j-th column). Therefore, they are useful to present algorithms operating on rows and columns.

Transvections are a special case of elementary matrices (according to most references, these also contain the matrices exchanging rows, and the matrices multiplying a row by a constant).

We show that, over a field, any matrix can be written as L * D * L', where L and L' are products of transvections and D is diagonal. In other words, one can reduce a matrix to diagonal form by operations on its rows and columns, a variant of Gauss' pivot algorithm.

Main definitions and results

• transvection i j c is the matrix equal to 1 + stdBasisMatrix i j c.

• TransvectionStruct n R is a structure containing the data of i, j, c and a proof that i ≠ j. These are often easier to manipulate than straight matrices, especially in inductive arguments.

• exists_list_transvec_mul_diagonal_mul_list_transvec states that any matrix M over a field can be written in the form t_1 * ... * t_k * D * t'_1 * ... * t'_l, where D is diagonal and the t_i, t'_j are transvections.

• diagonal_transvection_induction shows that a property which is true for diagonal matrices and transvections, and invariant under product, is true for all matrices.

• diagonal_transvection_induction_of_det_ne_zero is the same statement over invertible matrices.

Implementation details

The proof of the reduction results is done inductively on the size of the matrices, reducing an (r + 1) × (r + 1) matrix to a matrix whose last row and column are zeroes, except possibly for the last diagonal entry. This step is done as follows.

If all the coefficients on the last row and column are zero, there is nothing to do. Otherwise, one can put a nonzero coefficient in the last diagonal entry by a row or column operation, and then subtract this last diagonal entry from the other entries in the last row and column to make them vanish.

This step is done in the type Fin r ⊕ Unit, where Fin r is useful to choose arbitrarily some order in which we cancel the coefficients, and the sum structure is useful to use the formalism of block matrices.

To proceed with the induction, we reindex our matrices to reduce to the above situation.

def Matrix.transvection {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) (c : R) : Matrix n n R

The transvection matrix transvection i j c is equal to the identity plus c at position (i, j). Multiplying by it on the left (as in transvection i j c * M) corresponds to adding c times the j-th row of M to its i-th row. Multiplying by it on the right corresponds to adding c times the i-th column to the j-th column.

Equations

• Matrix.transvection i j c = 1 + Matrix.stdBasisMatrix i j c

@[simp]

theorem Matrix.transvection_zero {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) : Matrix.transvection i j 0 = 1

theorem Matrix.updateRow_eq_transvection {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) [Finite n] (c : R) : Matrix.updateRow 1 i (1 i + c • 1 j) = Matrix.transvection i j c

A transvection matrix is obtained from the identity by adding c times the j-th row to the i-th row.

theorem Matrix.transvection_mul_transvection_same {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) [Fintype n] (h : i ≠ j) (c : R) (d : R) : Matrix.transvection i j c * Matrix.transvection i j d = Matrix.transvection i j (c + d)

@[simp]

theorem Matrix.transvection_mul_apply_same {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) [Fintype n] (b : n) (c : R) (M : Matrix n n R) : (Matrix.transvection i j c * M) i b = M i b + c * M j b

@[simp]

theorem Matrix.mul_transvection_apply_same {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) [Fintype n] (a : n) (c : R) (M : Matrix n n R) : (M * Matrix.transvection i j c) a j = M a j + c * M a i

@[simp]

theorem Matrix.transvection_mul_apply_of_ne {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) [Fintype n] (a : n) (b : n) (ha : a ≠ i) (c : R) (M : Matrix n n R) : (Matrix.transvection i j c * M) a b = M a b

@[simp]

theorem Matrix.mul_transvection_apply_of_ne {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) [Fintype n] (a : n) (b : n) (hb : b ≠ j) (c : R) (M : Matrix n n R) : (M * Matrix.transvection i j c) a b = M a b

@[simp]

theorem Matrix.det_transvection_of_ne {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) [Fintype n] (h : i ≠ j) (c : R) : (Matrix.transvection i j c).det = 1

structure Matrix.TransvectionStruct (n : Type u_1) (R : Type u₂) : Type (max u_1 u₂)

A structure containing all the information from which one can build a nontrivial transvection. This structure is easier to manipulate than transvections as one has a direct access to all the relevant fields.

• i : n
• j : n
• hij : self.i ≠ self.j
• c : R

theorem Matrix.TransvectionStruct.hij {n : Type u_1} {R : Type u₂} (self : Matrix.TransvectionStruct n R) : self.i ≠ self.j

instance Matrix.instNonemptyTransvectionStructOfNontrivial (n : Type u_1) (R : Type u₂) [CommRing R] [Nontrivial n] : Nonempty (Matrix.TransvectionStruct n R)

Equations

• ⋯ = ⋯

def Matrix.TransvectionStruct.toMatrix {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (t : Matrix.TransvectionStruct n R) : Matrix n n R

Associating to a transvection_struct the corresponding transvection matrix.

Equations

• t.toMatrix = Matrix.transvection t.i t.j t.c

@[simp]

theorem Matrix.TransvectionStruct.toMatrix_mk {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] (i : n) (j : n) (hij : i ≠ j) (c : R) : { i := i, j := j, hij := hij, c := c }.toMatrix = Matrix.transvection i j c

@[simp]

theorem Matrix.TransvectionStruct.det {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (t : Matrix.TransvectionStruct n R) : t.toMatrix.det = 1

@[simp]

theorem Matrix.TransvectionStruct.det_toMatrix_prod {n : Type u_1} {𝕜 : Type u_3} [Field 𝕜] [DecidableEq n] [Fintype n] (L : List (Matrix.TransvectionStruct n 𝕜)) : (List.map Matrix.TransvectionStruct.toMatrix L).prod.det = 1

@[simp]

theorem Matrix.TransvectionStruct.inv_c {n : Type u_1} {R : Type u₂} [CommRing R] (t : Matrix.TransvectionStruct n R) : t.inv.c = -t.c

@[simp]

theorem Matrix.TransvectionStruct.inv_i {n : Type u_1} {R : Type u₂} [CommRing R] (t : Matrix.TransvectionStruct n R) : t.inv.i = t.i

@[simp]

theorem Matrix.TransvectionStruct.inv_j {n : Type u_1} {R : Type u₂} [CommRing R] (t : Matrix.TransvectionStruct n R) : t.inv.j = t.j

def Matrix.TransvectionStruct.inv {n : Type u_1} {R : Type u₂} [CommRing R] (t : Matrix.TransvectionStruct n R) : Matrix.TransvectionStruct n R

The inverse of a TransvectionStruct, designed so that t.inv.toMatrix is the inverse of t.toMatrix.

Equations

• t.inv = { i := t.i, j := t.j, hij := ⋯, c := -t.c }

theorem Matrix.TransvectionStruct.inv_mul {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (t : Matrix.TransvectionStruct n R) : t.inv.toMatrix * t.toMatrix = 1

theorem Matrix.TransvectionStruct.mul_inv {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (t : Matrix.TransvectionStruct n R) : t.toMatrix * t.inv.toMatrix = 1

theorem Matrix.TransvectionStruct.reverse_inv_prod_mul_prod {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (L : List (Matrix.TransvectionStruct n R)) : (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.inv) L.reverse).prod * (List.map Matrix.TransvectionStruct.toMatrix L).prod = 1

theorem Matrix.TransvectionStruct.prod_mul_reverse_inv_prod {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] (L : List (Matrix.TransvectionStruct n R)) : (List.map Matrix.TransvectionStruct.toMatrix L).prod * (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.inv) L.reverse).prod = 1

theorem Matrix.mem_range_scalar_of_commute_transvectionStruct {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] {M : Matrix n n R} (hM : ∀ (t : Matrix.TransvectionStruct n R), Commute t.toMatrix M) : M ∈ Set.range ⇑(Matrix.scalar n)

M is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix).

theorem Matrix.mem_range_scalar_iff_commute_transvectionStruct {n : Type u_1} {R : Type u₂} [DecidableEq n] [CommRing R] [Fintype n] {M : Matrix n n R} : M ∈ Set.range ⇑(Matrix.scalar n) ↔ ∀ (t : Matrix.TransvectionStruct n R), Commute t.toMatrix M

def Matrix.TransvectionStruct.sumInl {n : Type u_1} (p : Type u_2) {R : Type u₂} (t : Matrix.TransvectionStruct n R) : Matrix.TransvectionStruct (n ⊕ p) R

Given a TransvectionStruct on n, define the corresponding TransvectionStruct on n ⊕ p using the identity on p.

Equations

• Matrix.TransvectionStruct.sumInl p t = { i := Sum.inl t.i, j := Sum.inl t.j, hij := ⋯, c := t.c }

theorem Matrix.TransvectionStruct.toMatrix_sumInl {n : Type u_1} (p : Type u_2) {R : Type u₂} [DecidableEq n] [DecidableEq p] [CommRing R] (t : Matrix.TransvectionStruct n R) : (Matrix.TransvectionStruct.sumInl p t).toMatrix = Matrix.fromBlocks t.toMatrix 0 0 1

@[simp]

theorem Matrix.TransvectionStruct.sumInl_toMatrix_prod_mul {n : Type u_1} (p : Type u_2) {R : Type u₂} [DecidableEq n] [DecidableEq p] [CommRing R] [Fintype n] [Fintype p] (M : Matrix n n R) (L : List (Matrix.TransvectionStruct n R)) (N : Matrix p p R) : (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.sumInl p) L).prod * Matrix.fromBlocks M 0 0 N = Matrix.fromBlocks ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M) 0 0 N

@[simp]

theorem Matrix.TransvectionStruct.mul_sumInl_toMatrix_prod {n : Type u_1} (p : Type u_2) {R : Type u₂} [DecidableEq n] [DecidableEq p] [CommRing R] [Fintype n] [Fintype p] (M : Matrix n n R) (L : List (Matrix.TransvectionStruct n R)) (N : Matrix p p R) : Matrix.fromBlocks M 0 0 N * (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.sumInl p) L).prod = Matrix.fromBlocks (M * (List.map Matrix.TransvectionStruct.toMatrix L).prod) 0 0 N

def Matrix.TransvectionStruct.reindexEquiv {n : Type u_1} {p : Type u_2} {R : Type u₂} (e : n ≃ p) (t : Matrix.TransvectionStruct n R) : Matrix.TransvectionStruct p R

Given a TransvectionStruct on n and an equivalence between n and p, define the corresponding TransvectionStruct on p.

Equations

• Matrix.TransvectionStruct.reindexEquiv e t = { i := e t.i, j := e t.j, hij := ⋯, c := t.c }

theorem Matrix.TransvectionStruct.toMatrix_reindexEquiv {n : Type u_1} {p : Type u_2} {R : Type u₂} [DecidableEq n] [DecidableEq p] [CommRing R] [Fintype n] [Fintype p] (e : n ≃ p) (t : Matrix.TransvectionStruct n R) : (Matrix.TransvectionStruct.reindexEquiv e t).toMatrix = (Matrix.reindexAlgEquiv R R e) t.toMatrix

theorem Matrix.TransvectionStruct.toMatrix_reindexEquiv_prod {n : Type u_1} {p : Type u_2} {R : Type u₂} [DecidableEq n] [DecidableEq p] [CommRing R] [Fintype n] [Fintype p] (e : n ≃ p) (L : List (Matrix.TransvectionStruct n R)) : (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.reindexEquiv e) L).prod = (Matrix.reindexAlgEquiv R R e) (List.map Matrix.TransvectionStruct.toMatrix L).prod

Reducing matrices by left and right multiplication by transvections

In this section, we show that any matrix can be reduced to diagonal form by left and right multiplication by transvections (or, equivalently, by elementary operations on lines and columns). The main step is to kill the last row and column of a matrix in Fin r ⊕ Unit with nonzero last coefficient, by subtracting this coefficient from the other ones. The list of these operations is recorded in list_transvec_col M and list_transvec_row M. We have to analyze inductively how these operations affect the coefficients in the last row and the last column to conclude that they have the desired effect.

Once this is done, one concludes the reduction by induction on the size of the matrices, through a suitable reindexing to identify any fintype with Fin r ⊕ Unit.

def Matrix.Pivot.listTransvecCol {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)

A list of transvections such that multiplying on the left with these transvections will replace the last column with zeroes.

Equations

• Matrix.Pivot.listTransvecCol M = List.ofFn fun (i : Fin r) => Matrix.transvection (Sum.inl i) (Sum.inr ()) (-M (Sum.inl i) (Sum.inr ()) / M (Sum.inr ()) (Sum.inr ()))

def Matrix.Pivot.listTransvecRow {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)

A list of transvections such that multiplying on the right with these transvections will replace the last row with zeroes.

Equations

• Matrix.Pivot.listTransvecRow M = List.ofFn fun (i : Fin r) => Matrix.transvection (Sum.inr ()) (Sum.inl i) (-M (Sum.inr ()) (Sum.inl i) / M (Sum.inr ()) (Sum.inr ()))

@[simp]

theorem Matrix.Pivot.length_listTransvecCol {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : (Matrix.Pivot.listTransvecCol M).length = r

theorem Matrix.Pivot.listTransvecCol_get {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin (Matrix.Pivot.listTransvecCol M).length) : (Matrix.Pivot.listTransvecCol M).get i = Matrix.transvection (Sum.inl (Fin.cast ⋯ i)) (Sum.inr ()) (-M (Sum.inl (Fin.cast ⋯ i)) (Sum.inr ()) / M (Sum.inr ()) (Sum.inr ()))

@[simp]

theorem Matrix.Pivot.length_listTransvecRow {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : (Matrix.Pivot.listTransvecRow M).length = r

theorem Matrix.Pivot.listTransvecRow_get {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin (Matrix.Pivot.listTransvecRow M).length) : (Matrix.Pivot.listTransvecRow M).get i = Matrix.transvection (Sum.inr ()) (Sum.inl (Fin.cast ⋯ i)) (-M (Sum.inr ()) (Sum.inl (Fin.cast ⋯ i)) / M (Sum.inr ()) (Sum.inr ()))

theorem Matrix.Pivot.listTransvecCol_mul_last_row_drop {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit) {k : ℕ} (hk : k ≤ r) : ((List.drop k (Matrix.Pivot.listTransvecCol M)).prod * M) (Sum.inr ()) i = M (Sum.inr ()) i

Multiplying by some of the matrices in listTransvecCol M does not change the last row.

theorem Matrix.Pivot.listTransvecCol_mul_last_row {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit) : ((Matrix.Pivot.listTransvecCol M).prod * M) (Sum.inr ()) i = M (Sum.inr ()) i

Multiplying by all the matrices in listTransvecCol M does not change the last row.

theorem Matrix.Pivot.listTransvecCol_mul_last_col {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0) (i : Fin r) : ((Matrix.Pivot.listTransvecCol M).prod * M) (Sum.inl i) (Sum.inr ()) = 0

Multiplying by all the matrices in listTransvecCol M kills all the coefficients in the last column but the last one.

theorem Matrix.Pivot.mul_listTransvecRow_last_col_take {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit) {k : ℕ} (hk : k ≤ r) : (M * (List.take k (Matrix.Pivot.listTransvecRow M)).prod) i (Sum.inr ()) = M i (Sum.inr ())

Multiplying by some of the matrices in listTransvecRow M does not change the last column.

theorem Matrix.Pivot.mul_listTransvecRow_last_col {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit) : (M * (Matrix.Pivot.listTransvecRow M).prod) i (Sum.inr ()) = M i (Sum.inr ())

Multiplying by all the matrices in listTransvecRow M does not change the last column.

theorem Matrix.Pivot.mul_listTransvecRow_last_row {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0) (i : Fin r) : (M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inr ()) (Sum.inl i) = 0

Multiplying by all the matrices in listTransvecRow M kills all the coefficients in the last row but the last one.

theorem Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_col {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0) (i : Fin r) : ((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inr ()) (Sum.inl i) = 0

Multiplying by all the matrices either in listTransvecCol M and listTransvecRow M kills all the coefficients in the last row but the last one.

theorem Matrix.Pivot.listTransvecCol_mul_mul_listTransvecRow_last_row {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0) (i : Fin r) : ((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod) (Sum.inl i) (Sum.inr ()) = 0

Multiplying by all the matrices either in listTransvecCol M and listTransvecRow M kills all the coefficients in the last column but the last one.

theorem Matrix.Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0) : ((Matrix.Pivot.listTransvecCol M).prod * M * (Matrix.Pivot.listTransvecRow M).prod).IsTwoBlockDiagonal

Multiplying by all the matrices either in listTransvecCol M and listTransvecRow M turns the matrix in block-diagonal form.

theorem Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0) : ∃ (L : List (Matrix.TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (Matrix.TransvectionStruct (Fin r ⊕ Unit) 𝕜)), ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal

There exist two lists of TransvectionStruct such that multiplying by them on the left and on the right makes a matrix block-diagonal, when the last coefficient is nonzero.

theorem Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : ∃ (L : List (Matrix.TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (Matrix.TransvectionStruct (Fin r ⊕ Unit) 𝕜)), ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal

There exist two lists of TransvectionStruct such that multiplying by them on the left and on the right makes a matrix block-diagonal.

theorem Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (IH : ∀ (M : Matrix (Fin r) (Fin r) 𝕜), ∃ (L₀ : List (Matrix.TransvectionStruct (Fin r) 𝕜)) (L₀' : List (Matrix.TransvectionStruct (Fin r) 𝕜)) (D₀ : Fin r → 𝕜), (List.map Matrix.TransvectionStruct.toMatrix L₀).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L₀').prod = Matrix.diagonal D₀) (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : ∃ (L : List (Matrix.TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (L' : List (Matrix.TransvectionStruct (Fin r ⊕ Unit) 𝕜)) (D : Fin r ⊕ Unit → 𝕜), (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D

Inductive step for the reduction: if one knows that any size r matrix can be reduced to diagonal form by elementary operations, then one deduces it for matrices over Fin r ⊕ Unit.

theorem Matrix.Pivot.reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal {n : Type u_1} {p : Type u_2} {𝕜 : Type u_3} [Field 𝕜] [DecidableEq n] [DecidableEq p] [Fintype n] [Fintype p] (M : Matrix p p 𝕜) (e : p ≃ n) (H : ∃ (L : List (Matrix.TransvectionStruct n 𝕜)) (L' : List (Matrix.TransvectionStruct n 𝕜)) (D : n → 𝕜), (List.map Matrix.TransvectionStruct.toMatrix L).prod * (Matrix.reindexAlgEquiv 𝕜 𝕜 e) M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D) : ∃ (L : List (Matrix.TransvectionStruct p 𝕜)) (L' : List (Matrix.TransvectionStruct p 𝕜)) (D : p → 𝕜), (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D

Reduction to diagonal form by elementary operations is invariant under reindexing.

theorem Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux {𝕜 : Type u_3} [Field 𝕜] (n : Type) [Fintype n] [DecidableEq n] (M : Matrix n n 𝕜) : ∃ (L : List (Matrix.TransvectionStruct n 𝕜)) (L' : List (Matrix.TransvectionStruct n 𝕜)) (D : n → 𝕜), (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D

Any matrix can be reduced to diagonal form by elementary operations. Formulated here on Type 0 because we will make an induction using Fin r. See exists_list_transvec_mul_mul_list_transvec_eq_diagonal for the general version (which follows from this one and reindexing).

theorem Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal {n : Type u_1} {𝕜 : Type u_3} [Field 𝕜] [DecidableEq n] [Fintype n] (M : Matrix n n 𝕜) : ∃ (L : List (Matrix.TransvectionStruct n 𝕜)) (L' : List (Matrix.TransvectionStruct n 𝕜)) (D : n → 𝕜), (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D

Any matrix can be reduced to diagonal form by elementary operations.

theorem Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec {n : Type u_1} {𝕜 : Type u_3} [Field 𝕜] [DecidableEq n] [Fintype n] (M : Matrix n n 𝕜) : ∃ (L : List (Matrix.TransvectionStruct n 𝕜)) (L' : List (Matrix.TransvectionStruct n 𝕜)) (D : n → 𝕜), M = (List.map Matrix.TransvectionStruct.toMatrix L).prod * Matrix.diagonal D * (List.map Matrix.TransvectionStruct.toMatrix L').prod

Any matrix can be written as the product of transvections, a diagonal matrix, and transvections.

theorem Matrix.diagonal_transvection_induction {n : Type u_1} {𝕜 : Type u_3} [Field 𝕜] [DecidableEq n] [Fintype n] (P : Matrix n n 𝕜 → Prop) (M : Matrix n n 𝕜) (hdiag : ∀ (D : n → 𝕜), (Matrix.diagonal D).det = M.det → P (Matrix.diagonal D)) (htransvec : ∀ (t : Matrix.TransvectionStruct n 𝕜), P t.toMatrix) (hmul : ∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)) : P M

Induction principle for matrices based on transvections: if a property is true for all diagonal matrices, all transvections, and is stable under product, then it is true for all matrices. This is the useful way to say that matrices are generated by diagonal matrices and transvections.

We state a slightly more general version: to prove a property for a matrix M, it suffices to assume that the diagonal matrices we consider have the same determinant as M. This is useful to obtain similar principles for SLₙ or GLₙ.

theorem Matrix.diagonal_transvection_induction_of_det_ne_zero {n : Type u_1} {𝕜 : Type u_3} [Field 𝕜] [DecidableEq n] [Fintype n] (P : Matrix n n 𝕜 → Prop) (M : Matrix n n 𝕜) (hMdet : M.det ≠ 0) (hdiag : ∀ (D : n → 𝕜), (Matrix.diagonal D).det ≠ 0 → P (Matrix.diagonal D)) (htransvec : ∀ (t : Matrix.TransvectionStruct n 𝕜), P t.toMatrix) (hmul : ∀ (A B : Matrix n n 𝕜), A.det ≠ 0 → B.det ≠ 0 → P A → P B → P (A * B)) : P M

Induction principle for invertible matrices based on transvections: if a property is true for all invertible diagonal matrices, all transvections, and is stable under product of invertible matrices, then it is true for all invertible matrices. This is the useful way to say that invertible matrices are generated by invertible diagonal matrices and transvections.