Basic stuff about matrices

This file provides a specific API about matrices for the purposes of our project.

Basic lemmas

@[simp]

theorem Matrix.one_fromCols_transpose {α : Type} [Zero α] [One α] {m n : Type} [DecidableEq m] (A : Matrix m n α) : (1 ◫ A).transpose = 1 ⊟ A.transpose

@[simp]

theorem Matrix.one_fromRows_transpose {α : Type} [Zero α] [One α] {m n : Type} [DecidableEq n] (A : Matrix m n α) : (1 ⊟ A).transpose = 1 ◫ A.transpose

@[simp]

theorem Matrix.fromCols_one_transpose {α : Type} [Zero α] [One α] {m n : Type} [DecidableEq m] (A : Matrix m n α) : (A ◫ 1).transpose = A.transpose ⊟ 1

@[simp]

theorem Matrix.fromRows_one_transpose {α : Type} [Zero α] [One α] {m n : Type} [DecidableEq n] (A : Matrix m n α) : (A ⊟ 1).transpose = A.transpose ◫ 1

theorem Matrix.ext_col {α m n : Type} {A B : Matrix m n α} (hAB : ∀ (i : m), A i = B i) : A = B

Two matrices are equal if they agree on all columns.

theorem Matrix.det_int_coe {α : Type} [DecidableEq α] [Fintype α] (A : Matrix α α ℤ) (F : Type) [Field F] : ↑A.det = (A.map Int.cast).det

Computing the determinant of a square integer matrix and then converting it to a general field gives the same result as converting all elements to given field and computing the determinant afterwards.

theorem Matrix.det_rat_coe {α : Type} [DecidableEq α] [Fintype α] (A : Matrix α α ℚ) (F : Type) [Field F] [CharZero F] : ↑A.det = (A.map Rat.cast).det

Computing the determinant of a square rational matrix and then converting it to a CharZero field gives the same result as converting all elements to given field and computing the determinant afterwards.

theorem Matrix.entryProd_outerProd_eq_mul_col_mul_row {α m n : Type} [Semigroup α] (A : Matrix m n α) (c : m → α) (r : n → α) : (fun {X Y α β : Type} [SMul α β] (A : Matrix X Y α) (B : Matrix X Y β) => of fun (i : X) (j : Y) => A i j • B i j) A ((fun {X Y α : Type} [Mul α] (c : X → α) (r : Y → α) => of fun (i : X) (j : Y) => c i * r j) c r) = of fun (i : m) (j : n) => A i j * c i * r j

theorem Matrix.entryProd_outerProd_eq_mul_row_mul_col {α m n : Type} [CommSemigroup α] (A : Matrix m n α) (c : m → α) (r : n → α) : (fun {X Y α β : Type} [SMul α β] (A : Matrix X Y α) (B : Matrix X Y β) => of fun (i : X) (j : Y) => A i j • B i j) A ((fun {X Y α : Type} [Mul α] (c : X → α) (r : Y → α) => of fun (i : X) (j : Y) => c i * r j) c r) = of fun (i : m) (j : n) => A i j * r j * c i

theorem sum_elem_matrix_row_of_mem {α : Type} [DecidableEq α] {β : Type} [AddCommMonoidWithOne β] {x : α} {S : Set α} [Fintype ↑S] (hxS : x ∈ S) : ∑ i : ↑S, 1 x ↑i = 1

theorem sum_elem_matrix_row_of_nmem {α : Type} [DecidableEq α] {β : Type} [AddCommMonoidWithOne β] {x : α} {S : Set α} [Fintype ↑S] (hxS : x ∉ S) : ∑ i : ↑S, 1 x ↑i = 0

theorem sum_elem_smul_matrix_row_of_mem {α : Type} [DecidableEq α] {β : Type} [NonAssocSemiring β] {x : α} {S : Set α} [Fintype ↑S] (f : α → β) (hxS : x ∈ S) : ∑ i : ↑S, f ↑i • 1 x ↑i = f x

theorem sum_elem_smul_matrix_row_of_nmem {α : Type} [DecidableEq α] {β : Type} [NonAssocSemiring β] {x : α} {S : Set α} [Fintype ↑S] (f : α → β) (hxS : x ∉ S) : ∑ i : ↑S, f ↑i • 1 x ↑i = 0

def Matrix.abs {α : Type} [LinearOrderedAddCommGroup α] {m n : Type} (A : Matrix m n α) : Matrix m n α

The absolute value of a matrix is a matrix made of absolute values of respective elements.

Equations

• A.abs = Matrix.of fun (x1 : m) (x2 : n) => |A x1 x2|

def «term|___|_1» : Lean.ParserDescr

Equations

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

Conversion between set-indexed block-like matrices and type-indexed block matrices

def Matrix.toMatrixUnionUnion {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] (A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β) : Matrix (↑(T₁ ∪ T₂)) (↑(S₁ ∪ S₂)) β

Convert a block matrix to a matrix over set unions.

Equations

• A.toMatrixUnionUnion x✝ = (A ∘ Subtype.toSum) x✝ ∘ Subtype.toSum

def Matrix.toMatrixSumSum {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} (A : Matrix (↑(T₁ ∪ T₂)) (↑(S₁ ∪ S₂)) β) : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β

Convert a matrix over set unions to a block matrix.

Equations

• A.toMatrixSumSum x✝ = (A ∘ Sum.toUnion) x✝ ∘ Sum.toUnion

@[simp]

theorem toMatrixUnionUnion_toMatrixSumSum {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] (hT : T₁ ⫗ T₂) (hS : S₁ ⫗ S₂) (A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β) : A.toMatrixUnionUnion.toMatrixSumSum = A

Converting a block matrix to a matrix over set unions and back to a block matrix gives the original matrix, assuming that both said unions are disjoint.

@[simp]

theorem toMatrixSumSum_toMatrixUnionUnion {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] (A : Matrix (↑(T₁ ∪ T₂)) (↑(S₁ ∪ S₂)) β) : A.toMatrixSumSum.toMatrixUnionUnion = A

Converting a matrix over set unions to a block matrix and back to a matrix over set unions gives the original matrix.

theorem Matrix.IsTotallyUnimodular.toMatrixUnionUnion {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] [CommRing β] {A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β} (hA : A.IsTotallyUnimodular) : A.toMatrixUnionUnion.IsTotallyUnimodular

A totally unimodular block matrix stays totally unimodular after converting to a matrix over set unions.

def Matrix.toMatrixElemElem {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] {T S : Set α} (A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β) (hT : T = T₁ ∪ T₂) (hS : S = S₁ ∪ S₂) : Matrix (↑T) (↑S) β

Convert a block matrix to a matrix over set unions named as single indexing sets.

Equations

• A.toMatrixElemElem hT hS = ⋯ ▸ ⋯ ▸ A.toMatrixUnionUnion

theorem Matrix.toMatrixElemElem_apply {α : Type} {T₁ T₂ S₁ S₂ : Set α} {β : Type} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] {T S : Set α} (A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) β) (hT : T = T₁ ∪ T₂) (hS : S = S₁ ∪ S₂) (i : ↑T) (j : ↑S) : A.toMatrixElemElem hT hS i j = A (hT ▸ i).toSum (hS ▸ j).toSum

Direct characterization of Matrix.toMatrixElemElem entries.

theorem Matrix.IsTotallyUnimodular.toMatrixElemElem {α : Type} {T₁ T₂ S₁ S₂ : Set α} [(a : α) → Decidable (a ∈ T₁)] [(a : α) → Decidable (a ∈ T₂)] [(a : α) → Decidable (a ∈ S₁)] [(a : α) → Decidable (a ∈ S₂)] {T S : Set α} {A : Matrix (↑T₁ ⊕ ↑T₂) (↑S₁ ⊕ ↑S₂) ℚ} (hA : A.IsTotallyUnimodular) (hT : T = T₁ ∪ T₂) (hS : S = S₁ ∪ S₂) : (A.toMatrixElemElem hT hS).IsTotallyUnimodular

A totally unimodular block matrix stays totally unimodular after converting to a matrix over set unions named as single indexing sets.