Pivots of a matrix

Matrix.IsPivotedBy A l defines a map-based representation l for the pivot, stating that l i is the pivot column of each row i of A, with ⊤ for a zero row.

Main definitions

• Matrix.IsPivotedBy: l i : WithTop n is the pivot column of each row i of A.

Main results

• Matrix.IsPivotedBy.rank_eq: the rank of a matrix is its number of pivots.
• Matrix.IsPivotedBy.unique: the pivot of a matrix is unique if the column indices have a linear order.
• Matrix.isPivotedBy_iff: the map-structural characterisation of pivots.

Tags

matrix, echelon form, pivot

structure Matrix.IsPivotedBy {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] [LT m] [LT n] (A : Matrix m n R) (l : m → WithTop n) : Prop

A is in row echelon form and l i is the leading position of each row i, with ⊤ for a zero row.

• isRowEchelon : A.IsRowEchelon
• isPivotEntry (i : m) : (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0

theorem Matrix.IsPivotedBy.isLeadingEntry {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [LT m] [LT n] {i : m} {c : n} (hA : A.IsPivotedBy l) (hc : l i = ↑c) : A.IsLeadingEntry i c

theorem Matrix.IsPivotedBy.eq_top_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [LT m] [LT n] {i : m} (hA : A.IsPivotedBy l) : l i = ⊤ ↔ A i = 0

theorem Matrix.IsPivotedBy.lt_of_lt_of_ne_top {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [LinearOrder n] [LT m] {i₁ i₂ : m} (hA : A.IsPivotedBy l) (hlt : i₁ < i₂) (h₁ : l i₁ ≠ ⊤) : l i₁ < l i₂

theorem Matrix.IsPivotedBy.unique {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [LinearOrder n] [LT m] {l' : m → WithTop n} (hl : A.IsPivotedBy l) (hl' : A.IsPivotedBy l') : l = l'

The pivots of a matrix are unique.

theorem Matrix.IsPivotedBy.strictMonoOn {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [LinearOrder n] [Preorder m] (hA : A.IsPivotedBy l) : StrictMonoOn l {i : m | l i ≠ ⊤}

theorem Matrix.IsPivotedBy.monotone {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [LinearOrder n] [PartialOrder m] (hA : A.IsPivotedBy l) : Monotone l

theorem Matrix.isPivotedBy_iff {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [PartialOrder m] [LinearOrder n] : A.IsPivotedBy l ↔ Monotone l ∧ StrictMonoOn l {i : m | l i ≠ ⊤} ∧ ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0

The map-structural characterisation of pivots. This is useful for proving that a matrix is in row echelon form.

theorem Matrix.isPivotedBy_iff' {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] {A : Matrix m n R} {l : m → WithTop n} [PartialOrder m] [LinearOrder n] : A.IsPivotedBy l ↔ Monotone l ∧ StrictMonoOn l {i : m | l i ≠ ⊤} ∧ ∀ (i : m), l i = ⊤ ∧ A i = 0 ∨ ∃ (c : n), l i = ↑c ∧ A.IsLeadingEntry i c

A variant of isPivotedBy_iff phrased with Matrix.IsLeadingEntry.

theorem Matrix.IsPivotedBy.rank_eq {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [LinearOrder m] [LinearOrder n] [CommRing R] [IsDomain R] {A : Matrix m n R} {l : m → WithTop n} (hA : A.IsPivotedBy l) : A.rank = {i : m | l i ≠ ⊤}.card

Decidability

@[instance_reducible]

instance Matrix.instDecidableIsPivotedByOfFintype {m : Type u_1} {n : Type u_2} {R : Type u_3} [Zero R] [DecidableEq R] [Fintype m] [LinearOrder m] [Fintype n] [LinearOrder n] (A : Matrix m n R) (l : m → WithTop n) : Decidable (A.IsPivotedBy l)

Equations

• One or more equations did not get rendered due to their size.