Nonsingular inverses over semirings #

This file proves A * B = 1 ↔ B * A = 1 for square matrices over a commutative semiring.

def Matrix.detp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) :

The determinant, but only the terms of a given sign. A.detp 1 is written |A|⁺ in the literature and A.detp (-1) is written |A|⁻.

Equations

Matrix.detp s A = ∑ σ ∈ Equiv.Perm.ofSign s, ∏ k : n, A k (σ k)

Instances For

source

@[simp]

theorem Matrix.detp_transpose {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) :

detp s A.transpose = detp s A

source

@[simp]

theorem Matrix.detp_zero {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) [Nonempty n] :

detp s 0 = 0

source

@[simp]

theorem Matrix.detp_one_diagonal {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (d : n → R) :

detp 1 (diagonal d) = ∏ i : n, d i

source

@[simp]

theorem Matrix.detp_one_one {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] :

detp 1 1 = 1

source

@[simp]

theorem Matrix.detp_neg_one_diagonal {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (d : n → R) :

detp (-1) (diagonal d) = 0

source

@[simp]

theorem Matrix.detp_neg_one_one {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] :

detp (-1) 1 = 0

source

@[simp]

theorem Matrix.detp_one_of_isEmpty {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) [IsEmpty n] :

detp 1 A = 1

source

@[simp]

theorem Matrix.detp_neg_one_of_isEmpty {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) [IsEmpty n] :

detp (-1) A = 0

source

@[simp]

theorem Matrix.detp_submatrix_equiv_equiv {n : Type u_1} {m : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) (f g : m ≃ n) :

detp s (A.submatrix ⇑f ⇑g) = detp (s * Equiv.Perm.sign (f.symm.trans g)) A

source

theorem Matrix.detp_submatrix_equiv_self {n : Type u_1} {m : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) (e : m ≃ n) :

detp s (A.submatrix ⇑e ⇑e) = detp s A

source

theorem Matrix.detp_smul {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) (c : R) :

detp s (c • A) = c ^ Fintype.card n * detp s A

source

theorem Matrix.detp_map {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) {S : Type u_4} [CommSemiring S] (f : R →+* S) :

detp s (A.map ⇑f) = f (detp s A)

source

def Matrix.IsDetpBalanced {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) (a b : R) :

Prop

A square matrix A over a commutative semiring R is "determinant balanced" with respect to a b : R if a|A|⁺ + b|A|⁻ = b|A|⁺ + a|A|⁻. Over a commutative ring, this is equivalent to (a - b)|A| = 0, see Matrix.isDetpBalanced_iff_sub_mul_det_eq_zero.

Equations

A.IsDetpBalanced a b = (a * Matrix.detp 1 A + b * Matrix.detp (-1) A = b * Matrix.detp 1 A + a * Matrix.detp (-1) A)

Instances For

source

theorem Matrix.IsDetpBalanced.refl {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) (a : R) :

A.IsDetpBalanced a a

source

theorem Matrix.IsDetpBalanced.of_eq {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} (eq : detp 1 A = detp (-1) A) :

A.IsDetpBalanced a b

source

theorem Matrix.IsDetpBalanced.symm {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} :

A.IsDetpBalanced a b → A.IsDetpBalanced b a

source

theorem Matrix.IsDetpBalanced_comm {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} :

A.IsDetpBalanced a b ↔ A.IsDetpBalanced b a

source

theorem Matrix.IsDetpBalanced.trans {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b c : R} [IsCancelAdd R] (hab : A.IsDetpBalanced a b) (hbc : A.IsDetpBalanced b c) :

A.IsDetpBalanced a c

source

theorem Matrix.IsDetpBalanced.mul_add_mul_eq {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} (h : A.IsDetpBalanced a b) (s t : ℤ ˣ) :

a * detp s A + b * detp t A = b * detp s A + a * detp t A

source

@[simp]

theorem Matrix.isDetpBalanced_transpose_iff {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} :

A.transpose.IsDetpBalanced a b ↔ A.IsDetpBalanced a b

source

theorem Matrix.IsDetpBalanced.transpose {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} :

A.IsDetpBalanced a b → A.transpose.IsDetpBalanced a b

Alias of the reverse direction of Matrix.isDetpBalanced_transpose_iff.

source

theorem Matrix.IsDetpBalanced.of_transpose {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} :

A.transpose.IsDetpBalanced a b → A.IsDetpBalanced a b

Alias of the forward direction of Matrix.isDetpBalanced_transpose_iff.

source

theorem Matrix.IsDetpBalanced.submatrix_equiv {n : Type u_1} {m : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} (e₁ e₂ : m ≃ n) (h : A.IsDetpBalanced a b) :

(A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b

source

@[simp]

theorem Matrix.isDetpBalanced_submatrix_equiv_iff {n : Type u_1} {m : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} {e₁ e₂ : m ≃ n} :

(A.submatrix ⇑e₁ ⇑e₂).IsDetpBalanced a b ↔ A.IsDetpBalanced a b

source

theorem Matrix.IsDetpBalanced.smul {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} (h : A.IsDetpBalanced a b) (c : R) :

(c • A).IsDetpBalanced a b

source

def Matrix.Nonsingular {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) :

Prop

A square matrix A over a commutative semiring R is called nonsingular if it is only determinant balanced with respect to equal elements.

See also See also Matrix.Nondegenerate.

Equations

A.Nonsingular = ∀ (a b : R), A.IsDetpBalanced a b → a = b

Instances For

source

theorem Matrix.Nonsingular.eq_of_IsDetpBalanced {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} (hA : A.Nonsingular) (hAd : A.IsDetpBalanced a b) :

a = b

source

theorem Matrix.IsDetpBalanced.eq_of_nonsingular {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} (hA : A.IsDetpBalanced a b) (hAn : A.Nonsingular) :

a = b

source

@[simp]

theorem Matrix.nonsingular_one {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] :

Nonsingular 1

source

@[simp]

theorem Matrix.Nonsingular.of_isEmpty {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) [IsEmpty n] :

A.Nonsingular

source

@[simp]

theorem Matrix.nonsingular_transpose_iff {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} :

A.transpose.Nonsingular ↔ A.Nonsingular

source

theorem Matrix.Nonsingular.transpose {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} :

A.Nonsingular → A.transpose.Nonsingular

Alias of the reverse direction of Matrix.nonsingular_transpose_iff.

source

theorem Matrix.Nonsingular.of_transpose {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} :

A.transpose.Nonsingular → A.Nonsingular

Alias of the forward direction of Matrix.nonsingular_transpose_iff.

source

@[simp]

theorem Matrix.nonsingular_submatrix_equiv_iff {n : Type u_1} {m : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {e₁ e₂ : m ≃ n} :

(A.submatrix ⇑e₁ ⇑e₂).Nonsingular ↔ A.Nonsingular

source

theorem Matrix.Nonsingular.submatrix_equiv {n : Type u_1} {m : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {e₁ e₂ : m ≃ n} :

A.Nonsingular → (A.submatrix ⇑e₁ ⇑e₂).Nonsingular

Alias of the reverse direction of Matrix.nonsingular_submatrix_equiv_iff.

source

theorem Matrix.detp_eq_of_row_eq {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {p q : n} (hpq : p ≠ q) (hrow : A.row p = A.row q) (s : ℤ ˣ := 1) (t : ℤ ˣ := -1) :

detp s A = detp t A

source

theorem Matrix.detp_eq_of_col_eq {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {p q : n} (hpq : p ≠ q) (hcol : A.col p = A.col q) (s : ℤ ˣ := 1) (t : ℤ ˣ := -1) :

detp s A = detp t A

source

theorem Matrix.detp_eq_of_row_eq_zero {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) {A : Matrix n n R} {p : n} (hrow : A.row p = 0) :

detp s A = 0

source

theorem Matrix.detp_eq_of_col_eq_zero {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) {A : Matrix n n R} {p : n} (hcol : A.col p = 0) :

detp s A = 0

source

theorem Matrix.IsDetpBalanced.submatrix_of_card_le {n : Type u_1} {m : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} {a b : R} (h : A.IsDetpBalanced a b) (le : Fintype.card n ≤ Fintype.card m) (f g : m → n) :

(A.submatrix f g).IsDetpBalanced a b

If A is determinant balanced with respect to a and b, any submatrix of the same or bigger size (possibly with repeated rows or columns) is also.

source

def Matrix.adjp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) :

Matrix n n R

The adjugate matrix, but only the terms of a given sign.

Equations

Matrix.adjp s A = Matrix.of fun (i j : n) => ∑ σ ∈ Equiv.Perm.ofSign s with σ j = i, ∏ k ∈ {j}ᶜ, A k (σ k)

Instances For

source

theorem Matrix.adjp_apply {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) (i j : n) :

adjp s A i j = ∑ σ ∈ Equiv.Perm.ofSign s with σ j = i, ∏ k ∈ {j}ᶜ, A k (σ k)

source

theorem Matrix.adjp_transpose {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) :

adjp s A.transpose = (adjp s A).transpose

source

theorem Matrix.adjp_none_none {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix (Option n) (Option n) R) :

adjp s A none none = detp s (A.submatrix some some)

source

theorem Matrix.adjp_some_none {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (i : n) (A : Matrix (Option n) (Option n) R) :

adjp s A (some i) none = detp (-s) (A.submatrix some (Function.update some i none))

source

theorem Matrix.adjp_none_some {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (i : n) (A : Matrix (Option n) (Option n) R) :

adjp s A none (some i) = detp (-s) (A.submatrix (Function.update some i none) some)

source

theorem Matrix.detp_mul {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A B : Matrix n n R) :

detp 1 (A * B) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) = detp (-1) (A * B) + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

source

theorem Matrix.mul_adjp_apply_eq {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) (i : n) :

(A * adjp s A) i i = detp s A

source

theorem Matrix.mul_adjp_apply_ne {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) (i j : n) (h : i ≠ j) :

(A * adjp 1 A) i j = (A * adjp (-1) A) i j

source

theorem Matrix.adjp_mul_apply_eq {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix n n R) (i : n) :

(adjp s A * A) i i = detp s A

source

theorem Matrix.adjp_mul_apply_ne {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) (i j : n) (h : i ≠ j) :

(adjp 1 A * A) i j = (adjp (-1) A * A) i j

source

theorem Matrix.mul_adjp_add_detp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A : Matrix n n R) :

A * adjp 1 A + detp (-1) A • 1 = A * adjp (-1) A + detp 1 A • 1

source

theorem Matrix.detp_option_expand_row_none {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (s : ℤ ˣ) (A : Matrix (Option n) (Option n) R) :

detp s A = A none none * detp s (A.submatrix some some) + ∑ k : n, A none (some k) * detp (-s) (A.submatrix some (Function.update some k none))

Laplace expansion of detp along the none row of an Option-indexed matrix.

source

theorem Matrix.isAddUnit_mul {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} {d : n → R} (hAB : A * B = diagonal d) (i j k : n) (hij : i ≠ j) :

IsAddUnit (A i k * B k j)

source

theorem Matrix.isAddUnit_detp_mul_detp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} {d : n → R} (hAB : A * B = diagonal d) :

IsAddUnit (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)

source

theorem Matrix.isAddUnit_detp_smul_mul_adjp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} {d : n → R} (hAB : A * B = diagonal d) :

IsAddUnit (detp 1 A • (B * adjp (-1) B) + detp (-1) A • (B * adjp 1 B))

source

theorem Matrix.detp_smul_add_adjp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} (hAB : A * B = 1) :

detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

source

theorem Matrix.detp_smul_adjp {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} (hAB : A * B = 1) :

A + (detp 1 A • adjp (-1) B + detp (-1) A • adjp 1 B) = detp 1 A • adjp 1 B + detp (-1) A • adjp (-1) B

source

@[instance 100]

instance Matrix.instIsStablyFiniteRingOfCommSemiring {R : Type u_3} [CommSemiring R] :

IsStablyFiniteRing R

Documentation

Mathlib.LinearAlgebra.Matrix.SemiringInverse

Nonsingular inverses over semirings #