Nonsingular inverses over semirings

This files 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) : R

The determinant, but only the terms of a given sign.

Equations

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

@[simp]

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

@[simp]

theorem Matrix.detp_neg_one_one {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] : Matrix.detp (-1) 1 = 0

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) => ∑ σ ∈ Finset.filter (fun (x : Equiv.Perm n) => x j = i) (Equiv.Perm.ofSign s), ∏ k ∈ {j}ᶜ, A k (σ k)

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) : Matrix.adjp s A i j = ∑ σ ∈ Finset.filter (fun (x : Equiv.Perm n) => x j = i) (Equiv.Perm.ofSign s), ∏ k ∈ {j}ᶜ, A k (σ k)

theorem Matrix.detp_mul {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A B : Matrix n n R) : Matrix.detp 1 (A * B) + (Matrix.detp 1 A * Matrix.detp (-1) B + Matrix.detp (-1) A * Matrix.detp 1 B) = Matrix.detp (-1) (A * B) + (Matrix.detp 1 A * Matrix.detp 1 B + Matrix.detp (-1) A * Matrix.detp (-1) B)

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 * Matrix.adjp s A) i i = Matrix.detp s A

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 * Matrix.adjp 1 A) i j = (A * Matrix.adjp (-1) A) i j

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 * Matrix.adjp 1 A + Matrix.detp (-1) A • 1 = A * Matrix.adjp (-1) A + Matrix.detp 1 A • 1

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

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} (hAB : A * B = 1) : IsAddUnit (Matrix.detp 1 A * Matrix.detp (-1) B + Matrix.detp (-1) A * Matrix.detp 1 B)

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} (hAB : A * B = 1) : IsAddUnit (Matrix.detp 1 A • (B * Matrix.adjp (-1) B) + Matrix.detp (-1) A • (B * Matrix.adjp 1 B))

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) : Matrix.detp 1 B • A + Matrix.adjp (-1) B = Matrix.detp (-1) B • A + Matrix.adjp 1 B

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 + (Matrix.detp 1 A • Matrix.adjp (-1) B + Matrix.detp (-1) A • Matrix.adjp 1 B) = Matrix.detp 1 A • Matrix.adjp 1 B + Matrix.detp (-1) A • Matrix.adjp (-1) B

theorem Matrix.mul_eq_one_comm {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A B : Matrix n n R} : A * B = 1 ↔ B * A = 1

def Matrix.invertibleOfLeftInverse {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A B : Matrix n n R) (h : B * A = 1) : Invertible A

We can construct an instance of invertible A if A has a left inverse.

Equations

• A.invertibleOfLeftInverse B h = { invOf := B, invOf_mul_self := h, mul_invOf_self := ⋯ }

def Matrix.invertibleOfRightInverse {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] (A B : Matrix n n R) (h : A * B = 1) : Invertible A

We can construct an instance of invertible A if A has a right inverse.

Equations

• A.invertibleOfRightInverse B h = { invOf := B, invOf_mul_self := ⋯, mul_invOf_self := h }

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

theorem Matrix.exists_left_inverse_iff_isUnit {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} : (∃ (B : Matrix n n R), B * A = 1) ↔ IsUnit A

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

theorem Matrix.exists_right_inverse_iff_isUnit {n : Type u_1} {R : Type u_3} [Fintype n] [DecidableEq n] [CommSemiring R] {A : Matrix n n R} : (∃ (B : Matrix n n R), A * B = 1) ↔ IsUnit A

theorem Matrix.mul_eq_one_comm_of_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 m n R} {B : Matrix n m R} (e : m ≃ n) : A * B = 1 ↔ B * A = 1

A version of mul_eq_one_comm that works for square matrices with rectangular types.