This file defines totally unimodular matrices and provides lemmas about them. It will be soon replaced by the implementation that got into Mathlib (slighlty different but mathematically equivalent).

def Matrix.TU {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix X Y R) : Prop

Is the matrix A totally unimodular?

Equations

• A.TU = ∀ (k : ℕ) (f : Fin k → X) (g : Fin k → Y), Function.Injective f → Function.Injective g → (A.submatrix f g).det = 0 ∨ (A.submatrix f g).det = 1 ∨ (A.submatrix f g).det = -1

theorem Matrix.TU_iff {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix X Y R) : A.TU ↔ ∀ (k : ℕ) (f : Fin k → X) (g : Fin k → Y), (A.submatrix f g).det = 0 ∨ (A.submatrix f g).det = 1 ∨ (A.submatrix f g).det = -1

theorem Matrix.TU_iff_fntp {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix X Y R) : A.TU ↔ ∀ (ι : Type u) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → X) (g : ι → Y), (A.submatrix f g).det = 0 ∨ (A.submatrix f g).det = 1 ∨ (A.submatrix f g).det = -1

theorem Matrix.TU.apply {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] {A : Matrix X Y R} (hA : A.TU) (i : X) (j : Y) : A i j = 0 ∨ A i j = 1 ∨ A i j = -1

theorem Matrix.TU.submatrix {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] {A : Matrix X Y R} (hA : A.TU) {X' : Type u_4} {Y' : Type u_5} (f : X' → X) (g : Y' → Y) : (A.submatrix f g).TU

theorem Matrix.TU.transpose {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] {A : Matrix X Y R} (hA : A.TU) : A.transpose.TU

theorem Matrix.TU_iff_transpose {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix X Y R) : A.TU ↔ A.transpose.TU

theorem Matrix.mapEquiv_rows_TU {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] {X' : Type u_4} [DecidableEq X'] (A : Matrix X Y R) (eX : X' ≃ X) : Matrix.TU (A ∘ ⇑eX) ↔ A.TU

theorem Matrix.TU.comp_rows {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] {X' : Type u_4} {A : Matrix X Y R} (hA : A.TU) (e : X' → X) : Matrix.TU (A ∘ e)

theorem Matrix.mapEquiv_cols_TU {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] {Y' : Type u_4} [DecidableEq Y'] (A : Matrix X Y R) (eY : Y' ≃ Y) : (Matrix.TU fun (x : X) => A x ∘ ⇑eY) ↔ A.TU

theorem Matrix.TU.comp_cols {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] {Y' : Type u_4} {A : Matrix X Y R} (hA : A.TU) (e : Y' → Y) : Matrix.TU fun (x : X) => A x ∘ e

theorem Matrix.mapEquiv_both_TU {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] {X' : Type u_4} {Y' : Type u_5} [DecidableEq X'] [DecidableEq Y'] (A : Matrix X Y R) (eX : X' ≃ X) (eY : Y' ≃ Y) : Matrix.TU ((fun (x : X) => A x ∘ ⇑eY) ∘ ⇑eX) ↔ A.TU

theorem Matrix.TU_adjoin_row0s_iff {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] (A : Matrix X Y R) {X' : Type u_4} : (A.fromRows (Matrix.row X' 0)).TU ↔ A.TU

theorem Matrix.TU_adjoin_id_below_iff {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y R) : (A.fromRows 1).TU ↔ A.TU

theorem Matrix.TU_adjoin_id_above_iff {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y R) : (Matrix.fromRows 1 A).TU ↔ A.TU

theorem Matrix.TU_adjoin_id_left_iff {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y R) : (Matrix.fromColumns 1 A).TU ↔ A.TU

theorem Matrix.TU_adjoin_id_right_iff {X : Type u_1} {Y : Type u_2} {R : Type u_3} [CommRing R] [DecidableEq X] [DecidableEq Y] (A : Matrix X Y R) : (A.fromColumns 1).TU ↔ A.TU

theorem Matrix.fromColumns_zero_rank {X : Type u_1} {R : Type u_3} [CommRing R] {Y₁ : Type u_6} {Y₂ : Type u_7} [Fintype Y₁] [Fintype Y₂] (A : Matrix X Y₂ R) : (Matrix.fromColumns 0 A).rank = A.rank

theorem Matrix.fromRows_rank_subadditive {Y : Type u_2} {R : Type u_3} [CommRing R] {X₁ : Type u_4} {X₂ : Type u_5} [Fintype Y] (A₁ : Matrix X₁ Y R) (A₂ : Matrix X₂ Y R) : (A₁.fromRows A₂).rank ≤ A₁.rank + A₂.rank

theorem Matrix.det_zero_of_rank_lt {X : Type u_1} {R : Type u_8} [LinearOrderedField R] [Fintype X] [DecidableEq X] {A : Matrix X X R} (hA : A.rank < Fintype.card X) : A.det = 0

theorem Matrix.fromBlocks_submatrix_apply {X₁ : Type u_4} {X₂ : Type u_5} {Y₁ : Type u_6} {Y₂ : Type u_7} {β : Type u_8} {ι : Type u_9} {γ : Type u_10} (f : ι → X₁ ⊕ X₂) (g : γ → Y₁ ⊕ Y₂) (A₁₁ : Matrix X₁ Y₁ β) (A₁₂ : Matrix X₁ Y₂ β) (A₂₁ : Matrix X₂ Y₁ β) (A₂₂ : Matrix X₂ Y₂ β) (i : ι) (j : γ) : (Matrix.fromBlocks A₁₁ A₁₂ A₂₁ A₂₂).submatrix f g i j = match f i with | Sum.inl i₁ => match g j with | Sum.inl j₁ => A₁₁ i₁ j₁ | Sum.inr j₂ => A₁₂ i₁ j₂ | Sum.inr i₂ => match g j with | Sum.inl j₁ => A₂₁ i₂ j₁ | Sum.inr j₂ => A₂₂ i₂ j₂

theorem Matrix.submatrix_det_abs {X : Type u_1} {Y : Type u_2} {R : Type u_8} [LinearOrderedCommRing R] [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] (A : Matrix X X R) (e₁ : Y ≃ X) (e₂ : Y ≃ X) : |(A.submatrix ⇑e₁ ⇑e₂).det| = |A.det|

theorem Matrix.submatrix_det_abs' {Y : Type u_2} {X₁ : Type u_4} {X₂ : Type u_5} {R : Type u_8} [LinearOrderedCommRing R] [Fintype X₁] [DecidableEq X₁] [Fintype X₂] [DecidableEq X₂] [Fintype Y] [DecidableEq Y] (A : Matrix X₁ X₂ R) (e₁ : Y ≃ X₁) (e₂ : Y ≃ X₂) : |(A.submatrix ⇑e₁ ⇑e₂).det| = |(A.submatrix (⇑(e₂.symm.trans e₁)) id).det|

theorem Matrix.fromBlocks_TU {X₁ : Type u_4} {X₂ : Type u_5} {Y₁ : Type u_6} {Y₂ : Type u_7} {R : Type u_8} [LinearOrderedField R] [Fintype X₁] [DecidableEq X₁] [Fintype Y₁] [DecidableEq Y₁] [Fintype X₂] [DecidableEq X₂] [Fintype Y₂] [DecidableEq Y₂] {A₁ : Matrix X₁ Y₁ R} {A₂ : Matrix X₂ Y₂ R} (hA₁ : A₁.TU) (hA₂ : A₂.TU) : (Matrix.fromBlocks A₁ 0 0 A₂).TU

A matrix composed of TU blocks on the diagonal is TU.