Pivoting

This file defines and studies pivoting in matrices. Pivoting is later used in many auxiliary constructions.

Elementary row operations

All declarations in this section are private.

Long-tableau pivoting

def Matrix.longTableauPivot {X : Type u_1} {Y : Type u_2} {F : Type u_3} [One F] [SMul F F] [Div F] [Sub F] [DecidableEq X] (A : Matrix X Y F) (x : X) (y : Y) : Matrix X Y F

The result of pivoting in a long tableau. This definition makes sense only if A x y is non-zero. The recommending spelling when calling the function is (A.longTableauPivot x y) i j when pivoting in A on [x,y] and indexing at [i,j] even tho the ( ) is redundant.

Equations

• A.longTableauPivot x y = Matrix.of fun (i : X) => if i = x then (1 / A x y) • A i else A i - (A i y / A x y) • A x

theorem Matrix.longTableauPivot_elem_pivot_eq_one {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DecidableEq X] [DivisionSemiring F] [Sub F] (A : Matrix X Y F) {x : X} {y : Y} (hAxy : A x y ≠ 0) : A.longTableauPivot x y x y = 1

Long-tableau pivoting changes the nonzero pivot to one.

theorem Matrix.longTableauPivot_elem_in_pivot_col_eq_zero {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DecidableEq X] [DivisionRing F] (A : Matrix X Y F) {x i : X} {y : Y} (hix : i ≠ x) (hAxy : A x y ≠ 0) : A.longTableauPivot x y i y = 0

Long-tableau pivoting changes all nonpivot elements in the pivot column to zeros.

theorem Matrix.longTableauPivot_elem_in_pivot_row_eq_zero {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DecidableEq X] [NonAssocSemiring F] [Sub F] [Div F] (A : Matrix X Y F) {x : X} {j : Y} (hAxj : A x j = 0) (y : Y) : A.longTableauPivot x y x j = 0

Long-tableau pivoting preserves zeros of all nonpivot elements in the pivot row.

theorem Matrix.longTableauPivot_elem_of_zero_in_pivot_row {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DecidableEq X] [NonAssocRing F] [Div F] (A : Matrix X Y F) {x i : X} {j : Y} (hix : i ≠ x) (hAxj : A x j = 0) (y : Y) : A.longTableauPivot x y i j = A i j

Long-tableau pivoting preserves the original values in the nonpivot row whereëver the pivot row has zeros.

theorem Matrix.IsTotallyUnimodular.longTableauPivot {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DecidableEq X] [Field F] {A : Matrix X Y F} (hA : A.IsTotallyUnimodular) (x : X) (y : Y) (hAxy : A x y ≠ 0) : (A.longTableauPivot x y).IsTotallyUnimodular

Long-tableau pivoting preserves total unimodularity.

theorem Matrix.longTableauPivot_linearIndepenOn {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DecidableEq X] [Field F] (A : Matrix X Y F) {x : X} {y : Y} (hAxy : A x y ≠ 0) (S : Set Y) : LinearIndepOn F (A.longTableauPivot x y).transpose S ↔ LinearIndepOn F A.transpose S

Long-tableau pivoting preserves linear independence on transpose.

Short-tableau pivoting

def Matrix.shortTableauPivot {X : Type u_1} {Y : Type u_2} {F : Type u_3} [One F] [SMul F F] [Div F] [Zero F] [Sub F] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y F) (x : X) (y : Y) : Matrix X Y F

The result of pivoting in a short tableau. This definition makes sense only if A x y is non-zero. The recommending spelling when calling the function is (A.shortTableauPivot x y) i j when pivoting in A on [x,y] and indexing at [i,j] even tho the ( ) is redundant.

Equations

• A.shortTableauPivot x y = ((1 ◫ A).longTableauPivot x ◪y).submatrix id fun (j : Y) => if j = y then ◩x else ◪j

@[simp]

theorem Matrix.shortTableauPivot_eq {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DivisionRing F] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y F) (x : X) (y : Y) : A.shortTableauPivot x y = of fun (i : X) (j : Y) => if i = x then if j = y then 1 / A x y else 1 / A x y * A x j else if j = y then -A i y / A x y else A i j - A i y / A x y * A x j

Explicit formula for the short-tableau pivoting.

theorem Matrix.IsTotallyUnimodular.shortTableauPivot {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DecidableEq X] [DecidableEq Y] [Field F] {A : Matrix X Y F} (hA : A.IsTotallyUnimodular) {x : X} {y : Y} (hAxy : A x y ≠ 0) : (A.shortTableauPivot x y).IsTotallyUnimodular

Short-tableau pivoting preserves total unimodularity.

theorem Matrix.shortTableauPivot_zero {X : Type u_1} {Y : Type u_2} {F : Type u_3} {X' : Type u_4} {Y' : Type u_5} [DecidableEq X] [DecidableEq Y] [DecidableEq X'] [DivisionRing F] (A : Matrix X Y F) (x : X') (y : Y) (f : X' → X) (g : Y' → Y) (hg : y ∉ g.range) (hAfg : ∀ (i : X') (j : Y'), A (f i) (g j) = 0) (i : X') (j : Y') : A.shortTableauPivot (f x) y (f i) (g j) = 0

theorem Matrix.shortTableauPivot_submatrix_zero_external_row {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DivisionRing F] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y F) (x : X) (y : Y) {X' : Type u_4} {Y' : Type u_5} (f : X' → X) (g : Y' → Y) (hf : x ∉ f.range) (hg : y ∉ g.range) (hAg : ∀ (j : Y'), A x (g j) = 0) : (A.shortTableauPivot x y).submatrix f g = A.submatrix f g

theorem Matrix.submatrix_shortTableauPivot {X : Type u_1} {Y : Type u_2} {F : Type u_3} [DecidableEq X] [DecidableEq Y] {X' : Type u_4} {Y' : Type u_5} [DecidableEq X'] [DecidableEq Y'] [DivisionRing F] {f : X' → X} {g : Y' → Y} (A : Matrix X Y F) (hf : Function.Injective f) (hg : Function.Injective g) (x : X') (y : Y') : (A.submatrix f g).shortTableauPivot x y = (A.shortTableauPivot (f x) (g y)).submatrix f g

Lemma 1 of Proof of Regularity of 2-Sum and 3-Sum of Matroids

theorem shortTableauPivot_submatrix_det_abs_eq_div {F : Type u_3} [LinearOrderedField F] {k : ℕ} {A : Matrix (Fin k.succ) (Fin k.succ) F} {x y : Fin k.succ} (hAxy : A x y ≠ 0) : ∃ (f : Fin k → Fin k.succ) (g : Fin k → Fin k.succ), |((A.shortTableauPivot x y).submatrix f g).det| = |A.det| / |A x y|

theorem Matrix.abs_det_eq_shortTableauPivot_submatrix_abs_det {F : Type u_3} [LinearOrderedField F] {k : ℕ} (A : Matrix (Fin k.succ) (Fin k.succ) F) {i j : Fin k.succ} (hAij : A i j = 1 ∨ A i j = -1) : ∃ (f : Fin k → Fin k.succ) (g : Fin k → Fin k.succ), |A.det| = |((A.shortTableauPivot i j).submatrix f g).det|