Echelon decomposition certificates

Echelon.Decomposition A L σ pivot 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.
• Echelon.Decomposition.prod_diag_mul_det: A.det is determined by the diagonal products of L and of the echelon form 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) (L : Matrix m m R) (σ : Equiv.Perm m) (pivot : m → WithTop n) : Prop

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

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

theorem Echelon.Decomposition.prod_diag_mul_det {m : Type u_1} [Fintype m] [LinearOrder m] {R : Type u_3} [CommRing R] {L : Matrix m m R} {σ : Equiv.Perm m} [DecidableEq m] {A : Matrix m m R} {pivot : m → WithTop m} (cert : Decomposition A L σ pivot) : (∏ i : m, L i i) * (↑↑(Equiv.Perm.sign σ) * A.det) = ∏ i : m, (L * A.submatrix (⇑σ) id) i i

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] {A : Matrix m n R} {L : Matrix m m R} {σ : Equiv.Perm m} {pivot : m → WithTop n} [IsDomain R] (cert : Decomposition A L σ pivot) : A.rank = {i : m | pivot i ≠ ⊤}.card