Echelon decomposition certificates

Echelon.Decomposition A certifies an echelon decomposition of the matrix A.

Main definitions

• Echelon.Decomposition: the certificate structure.

Main results

• Echelon.Decomposition.rank_eq: A.rank is the pivot count of any certificate for A.

Tags

matrix, echelon form

structure Echelon.Decomposition {m : Type u_1} [Fintype m] [LinearOrder m] {n : Type u_2} [LinearOrder n] {R : Type u_3} [CommRing R] (A : Matrix m n R) : Type (max (max u_1 u_2) u_3)

A certificate of an echelon form decomposition of A, certifying that L * (A.submatrix σ id) is in echelon form by providing a pivot, where L is lower triangular with nonzero diagonal, and σ the permutation on the rows of A. This version does not store the final echelon form itself as it can be computed by the data enclosed.

• L : Matrix m m R

  The transformation matrix.

• σ : Equiv.Perm m

  The row permutation on the rows of A.

• pivot : m → WithTop n

  The pivot of the resulting echelon form.

• isPivotedBy : (self.L * A.submatrix (⇑self.σ) id).IsPivotedBy self.pivot
• L_lowerTriangular : self.L.IsLowerTriangular
• L_diag_ne_zero (i : m) : self.L.diag i ≠ 0

theorem Echelon.Decomposition.rank_eq {m : Type u_1} [Fintype m] [LinearOrder m] {n : Type u_2} [Fintype n] [LinearOrder n] {R : Type u_3} [CommRing R] [IsDomain R] {A : Matrix m n R} (cert : Decomposition A) : A.rank = {i : m | cert.pivot i ≠ ⊤}.card