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_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_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

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 #