feat(linear_algebra): Matrix inverses for square nonsingular matrices (#1816)

* Prove that some matrices have inverses

* Finish the proof: show that the determinant is 0 if a column is repeated

* Show that nonsingular_inv is also a right inverse

* Cleanup and code movement

* Small lemmata on transpose

* WIP: some work on inverse matrices

* Code cleanup and documentation

* More cleanup and documentation

* Generalize det_zero_of_column_eq to remove the linear order assumption

* Fix linting issues.

* Unneeded import can be removed

* A little bit more cleanup

* Generalize nonsing_inv to any ring with inverse

* Improve comments for `nonsingular_inverse`

* Remove the less general `det_zero_of_column_eq_of_char_ne_two` proof

* Rename `cramer_map_val` -> `cramer_map_def`

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* whitespace

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* whitespace: indent tactic proofs

* More renaming `cramer_map_val` -> `cramer_map_def`

* `swap_mul_self_mul` can be a `simp` lemma

* Make parameter σ to `swap_mul_eq_iff` implicit

* Update usage of `function.update_same` and `function.update_noteq`

* Replace `det_permute` with `det_permutation`

Although the statement now gives the determinant of a permutation matrix,
the proof is easier if we write it as a permuted identity matrix.
Thus the proof is basically the same, except a different line showing that the
entries are the same.

* Re-introduce `matrix.det_permute` (now based on `matrix.det_permutation`)

* Delete `cramer_at` and clean up the proofs depending on it

* Replace `cramer_map` with `cramer` after defining `cramer`

* Apply suggestions from code review

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Clean up imports

* Formatting: move } to previous lines

* Move assumptions of `det_zero_of_repeated_column` from variable to argument

* whitespace

Insert space between `finset.filter` and the filter condition.

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Improve docstrings

* Make argument to `prod_cancels_of_partition_cancels` explicit

* Rename `replace_column` and `replace_row` to `update_column` and `update_row`

* Replace `update_column_eq` with `update_column_self` + rewriting step

* whitespace

Newlines between all lemmas

* whitespace

Newline before 'begin'

* Fix conflicts with latest mathlib

* Remove unnecessary explicitification of arguments

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 4 people

src/algebra/big_operators.lean

@@ -229,14 +229,28 @@ calc s.prod (λ x, h (if p x then f x else g x))
     (prod_congr rfl (by simp {contextual := tt}))
     (prod_congr rfl (by simp {contextual := tt}))
 
-@[simp, to_additive] lemma prod_ite_eq [decidable_eq α] (s : finset α) (a : α) (b : β) :
-  s.prod (λ x, (ite (a = x) b 1)) = ite (a ∈ s) b 1 :=
+@[simp, to_additive] lemma prod_ite_eq [decidable_eq α] (s : finset α) (a : α) (b : α → β) :
+  s.prod (λ x, (ite (a = x) (b x) 1)) = ite (a ∈ s) (b a) 1 :=
 begin
   rw ←finset.prod_filter,
   split_ifs;
   simp only [filter_eq, if_true, if_false, h, prod_empty, prod_singleton, insert_empty_eq_singleton],
 end
 
+/--
+  When a product is taken over a conditional whose condition is an equality test on the index
+  and whose alternative is 1, then the product's value is either the term at that index or `1`.
+
+  The difference with `prod_ite_eq` is that the arguments to `eq` are swapped.
+-/
+@[simp, to_additive] lemma prod_ite_eq' [decidable_eq α] (s : finset α) (a : α) (b : α → β) :
+  s.prod (λ x, (ite (x = a) (b x) 1)) = ite (a ∈ s) (b a) 1 :=
+begin
+  rw ←prod_ite_eq,
+  congr, ext x,
+  by_cases x = a; finish
+end
+
 @[to_additive]
 lemma prod_attach {f : α → β} : s.attach.prod (λx, f x.val) = s.prod f :=
 by haveI := classical.dec_eq α; exact
@@ -458,6 +472,22 @@ begin
     congr' 1,
     rw mul_comm }
 end
+    
+/-- If we can partition a product into subsets that cancel out, then the whole product cancels. -/
+@[to_additive]
+lemma prod_cancels_of_partition_cancels (R : setoid α) [decidable_rel R.r]
+  (h : ∀ x ∈ s, (s.filter (λy, y ≈ x)).prod f = 1) : s.prod f = 1 :=
+begin
+  suffices : (s.image quotient.mk).prod (λ xbar, (s.filter (λ y, ⟦y⟧ = xbar)).prod f) = s.prod f,
+  { rw [←this, ←finset.prod_eq_one],
+    intros xbar xbar_in_s,
+    rcases (mem_image).mp xbar_in_s with ⟨x, x_in_s, xbar_eq_x⟩,
+    rw [←xbar_eq_x, filter_congr (λ y _, @quotient.eq _ R y x)],
+    apply h x x_in_s },
+  apply finset.prod_image' f,
+  intros,
+  refl
+end
 
 end comm_monoid
 
@@ -574,14 +604,14 @@ lemma mul_sum : b * s.sum f = s.sum (λx, b * f x) :=
 @[simp] lemma sum_mul_boole [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
   s.sum (λ x, (f x * ite (a = x) 1 0)) = ite (a ∈ s) (f a) 0 :=
 begin
-  convert sum_ite_eq s a (f a),
+  convert sum_ite_eq s a f,
   funext,
   split_ifs with h; simp [h],
 end
 @[simp] lemma sum_boole_mul [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
   s.sum (λ x, (ite (a = x) 1 0) * f x) = ite (a ∈ s) (f a) 0 :=
 begin
-  convert sum_ite_eq s a (f a),
+  convert sum_ite_eq s a f,
   funext,
   split_ifs with h; simp [h],
 end

src/data/finset.lean

@@ -791,6 +791,11 @@ noncomputable instance {α : Type*} : has_sep α (finset α) := ⟨λ p x, x.fil
 
 end classical
 
+/--
+  After filtering out everything that does not equal a given value, at most that value remains.
+
+  This is equivalent to `filter_eq'` with the equality the other way.
+-/
 -- This is not a good simp lemma, as it would prevent `finset.mem_filter` from firing
 -- on, e.g. `x ∈ s.filter(eq b)`.
 lemma filter_eq [decidable_eq β] (s : finset β) (b : β) :
@@ -805,6 +810,15 @@ begin
     rintros m ⟨e⟩, exact h m, }
 end
 
+/--
+  After filtering out everything that does not equal a given value, at most that value remains.
+
+  This is equivalent to `filter_eq` with the equality the other way.
+-/
+lemma filter_eq' [decidable_eq β] (s : finset β) (b : β) :
+  s.filter (λ a, a = b) = ite (b ∈ s) {b} ∅ :=
+trans (filter_congr (λ _ _, ⟨eq.symm, eq.symm⟩)) (filter_eq s b)
+
 end filter
 
 /-! ### range -/

src/data/matrix/basic.lean

@@ -293,21 +293,33 @@ section transpose
 
 open_locale matrix
 
+/--
+  Tell `simp` what the entries are in a transposed matrix.
+
+  Compare with `mul_val`, `diagonal_val_eq`, etc.
+-/
+@[simp] lemma transpose_val (M : matrix m n α) (i j) : M.transpose j i = M i j := rfl
+
 @[simp] lemma transpose_transpose (M : matrix m n α) :
   Mᵀᵀ = M :=
 by ext; refl
 
 @[simp] lemma transpose_zero [has_zero α] : (0 : matrix m n α)ᵀ = 0 :=
 by ext i j; refl
 
-@[simp] lemma transpose_add [has_add α] (M : matrix m n α) (N : matrix m n α) :
-  (M + N)ᵀ = Mᵀ + Nᵀ  :=
+@[simp] lemma transpose_one [decidable_eq n] [has_zero α] [has_one α] : (1 : matrix n n α)ᵀ = 1 :=
 begin
   ext i j,
-  dsimp [transpose],
-  refl
+  unfold has_one.one transpose,
+  by_cases i = j,
+  { simp only [h, diagonal_val_eq] },
+  { simp only [diagonal_val_ne h, diagonal_val_ne (λ p, h (symm p))] }
 end
 
+@[simp] lemma transpose_add [has_add α] (M : matrix m n α) (N : matrix m n α) :
+  (M + N)ᵀ = Mᵀ + Nᵀ  :=
+by { ext i j, simp }
+
 @[simp] lemma transpose_mul [comm_ring α] (M : matrix m n α) (N : matrix n l α) :
   (M ⬝ N)ᵀ = Nᵀ ⬝ Mᵀ  :=
 begin
@@ -318,6 +330,10 @@ begin
   ac_refl
 end
 
+@[simp] lemma transpose_smul [comm_ring α] (c : α)(M : matrix m n α) :
+  (c • M)ᵀ = c • Mᵀ := 
+by { ext i j, refl }
+
 @[simp] lemma transpose_neg [comm_ring α] (M : matrix m n α) :
   (- M)ᵀ = - Mᵀ  :=
 by ext i j; refl

src/data/matrix/pequiv.lean

@@ -76,6 +76,10 @@ begin
     simp [h, eq_comm] {contextual := tt} }
 end
 
+lemma to_pequiv_mul_matrix [semiring α] (f : n ≃ n) (M : matrix n n α) :
+  (f.to_pequiv.to_matrix * M) = λ i, M (f i) :=
+by { ext i j, rw [mul_eq_mul, mul_matrix_apply, equiv.to_pequiv_apply] }
+
 lemma to_matrix_trans [semiring α] (f : l ≃. m) (g : m ≃. n) :
   ((f.trans g).to_matrix : matrix l n α) = f.to_matrix ⬝ g.to_matrix :=
 begin
@@ -128,4 +132,9 @@ by rw [← to_matrix_trans, single_trans_single_of_ne hb, to_matrix_bot]
   (single a c).to_matrix ⬝ M :=
 by rw [← matrix.mul_assoc, single_mul_single]
 
+/-- We can also define permutation matrices by permuting the rows of the identity matrix. -/
+lemma equiv_to_pequiv_to_matrix [has_one α] [has_zero α] (σ : equiv n n) (i j : n) :
+  σ.to_pequiv.to_matrix i j = (1 : matrix n n α) (σ i) j :=
+if_congr option.some_inj rfl rfl
+
 end pequiv

src/data/pequiv.lean

@@ -326,4 +326,6 @@ lemma to_pequiv_trans (f : α ≃ β) (g : β ≃ γ) : (f.trans g).to_pequiv =
 
 lemma to_pequiv_symm (f : α ≃ β) : f.symm.to_pequiv = f.to_pequiv.symm := rfl
 
+lemma to_pequiv_apply (f : α ≃ β) (x : α) : f.to_pequiv x = some (f x) := rfl
+
 end equiv

src/group_theory/perm/sign.lean

@@ -161,6 +161,19 @@ by rw [swap_mul_eq_mul_swap, inv_apply_self, inv_apply_self]
 @[simp] lemma swap_mul_self (i j : α) : equiv.swap i j * equiv.swap i j = 1 :=
 equiv.swap_swap i j
 
+/-- Multiplying a permutation with `swap i j` twice gives the original permutation.
+
+  This specialization of `swap_mul_self` is useful when using cosets of permutations.
+-/
+@[simp]
+lemma swap_mul_self_mul (i j : α) (σ : perm α) : equiv.swap i j * (equiv.swap i j * σ) = σ :=
+by rw [←mul_assoc (swap i j) (swap i j) σ, equiv.perm.swap_mul_self, one_mul]
+
+lemma swap_mul_eq_iff {i j : α} {σ : perm α} : swap i j * σ = σ ↔ i = j :=
+⟨(assume h, have swap_id : swap i j = 1 := mul_right_cancel (trans h (one_mul σ).symm),
+  by {rw [←swap_apply_right i j, swap_id], refl}),
+(assume h, by erw [h, swap_self, one_mul])⟩
+
 @[simp] lemma swap_swap_apply (i j k : α) : equiv.swap i j (equiv.swap i j k) = k :=
 equiv.swap_core_swap_core k i j
 

src/linear_algebra/determinant.lean

@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kenny Lau, Chris Hughes
+Authors: Kenny Lau, Chris Hughes, Tim Baanen
 -/
 import data.matrix.basic
+import data.matrix.pequiv
 import group_theory.perm.sign
 
 universes u v
@@ -15,6 +16,7 @@ variables {n : Type u} [fintype n] [decidable_eq n] {R : Type v} [comm_ring R]
 
 local notation `ε` σ:max := ((sign σ : ℤ ) : R)
 
+/-- The determinant of a matrix given by the Leibniz formula. -/
 definition det (M : matrix n n R) : R :=
 univ.sum (λ (σ : perm n), ε σ * univ.prod (λ i, M (σ i) i))
 
@@ -103,4 +105,95 @@ instance : is_monoid_hom (det : matrix n n R → R) :=
 { map_one := det_one,
   map_mul := det_mul }
 
+/-- Transposing a matrix preserves the determinant. -/
+@[simp] lemma det_transpose (M : matrix n n R) : M.transpose.det = M.det :=
+begin
+  apply sum_bij (λ σ _, σ⁻¹),
+  { intros σ _, apply mem_univ },
+  { intros σ _,
+    rw [sign_inv],
+    congr' 1,
+    apply prod_bij (λ i _, σ i),
+    { intros i _, apply mem_univ },
+    { intros i _, simp },
+    { intros i j _ _ h, simp at h, assumption },
+    { intros i _, use σ⁻¹ i, finish } },
+  { intros σ σ' _ _ h, simp at h, assumption },
+  { intros σ _, use σ⁻¹, finish }
+end
+
+/-- The determinant of a permutation matrix equals its sign. -/
+@[simp] lemma det_permutation (σ : perm n) :
+  matrix.det (σ.to_pequiv.to_matrix : matrix n n R) = σ.sign := begin
+  suffices : matrix.det (σ.to_pequiv.to_matrix) = ↑σ.sign * det (1 : matrix n n R), { simp [this] },
+  unfold det,
+  rw mul_sum,
+  apply sum_bij (λ τ _, σ * τ),
+  { intros τ _, apply mem_univ },
+  { intros τ _,
+    conv_lhs { rw [←one_mul (sign τ), ←int.units_pow_two (sign σ)] },
+    conv_rhs { rw [←mul_assoc, coe_coe, sign_mul, units.coe_mul, int.cast_mul, ←mul_assoc] },
+    congr,
+    { norm_num },
+    { ext i, apply pequiv.equiv_to_pequiv_to_matrix } },
+  { intros τ τ' _ _, exact (mul_left_inj σ).mp },
+  { intros τ _, use σ⁻¹ * τ, use (mem_univ _), exact (mul_inv_cancel_left _ _).symm }
+end
+
+/-- Permuting the columns changes the sign of the determinant. -/
+lemma det_permute (σ : perm n) (M : matrix n n R) : matrix.det (λ i, M (σ i)) = σ.sign * M.det :=
+by rw [←det_permutation, ←det_mul, pequiv.to_pequiv_mul_matrix]
+
+section det_zero
+/-! ### `det_zero` section
+
+  Prove that a matrix with a repeated column has determinant equal to zero.
+-/
+
+/--
+  `mod_swap i j` contains permutations up to swapping `i` and `j`.
+
+  We use this to partition permutations in the expression for the determinant,
+  such that each partitions sums up to `0`.
+-/
+def mod_swap {n : Type u} [decidable_eq n] (i j : n) : setoid (perm n) :=
+⟨ λ σ τ, σ = τ ∨ σ = swap i j * τ,
+  λ σ, or.inl (refl σ),
+  λ σ τ h, or.cases_on h (λ h, or.inl h.symm) (λ h, or.inr (by rw [h, swap_mul_self_mul])),
+  λ σ τ υ hστ hτυ, by cases hστ; cases hτυ; try {rw [hστ, hτυ, swap_mul_self_mul]}; finish⟩
+
+instance (i j : n) : decidable_rel (mod_swap i j).r := λ σ τ, or.decidable
+
+variables {M : matrix n n R} {i j : n}
+
+/-- If a matrix has a repeated column, the determinant will be zero. -/
+theorem det_zero_of_column_eq (i_ne_j : i ≠ j) (hij : M i = M j) : M.det = 0 :=
+begin
+  have swap_invariant : ∀ k, M (swap i j k) = M k,
+  { intros k,
+    rw [swap_apply_def],
+    by_cases k = i, { rw [if_pos h, h, ←hij] },
+    rw [if_neg h],
+    by_cases k = j, { rw [if_pos h, h, hij] },
+    rw [if_neg h] },
+
+  have : ∀ σ, _root_.disjoint (_root_.singleton σ) (_root_.singleton (swap i j * σ)),
+  { intros σ,
+    rw [finset.singleton_eq_singleton, finset.singleton_eq_singleton, disjoint_singleton],
+    apply (not_congr mem_singleton).mpr,
+    exact (not_congr swap_mul_eq_iff).mpr i_ne_j },
+
+  apply finset.sum_cancels_of_partition_cancels (mod_swap i j),
+  intros σ _,
+  erw [filter_or, filter_eq', filter_eq', if_pos (mem_univ σ), if_pos (mem_univ (swap i j * σ)),
+    sum_union (this σ), sum_singleton, sum_singleton],
+  convert add_right_neg (↑↑(sign σ) * finset.prod univ (λ (i : n), M (σ i) i)),
+  rw [neg_mul_eq_neg_mul],
+  congr,
+  { rw [sign_mul, sign_swap i_ne_j], norm_num },
+  ext j, rw [mul_apply, swap_invariant]
+end
+
+end det_zero
+
 end matrix