From 8f8b194a1c61b519ed9626fc31477014e01aa165 Mon Sep 17 00:00:00 2001
From: Anne Baanen <vierkantor@vierkantor.com>
Date: Sat, 24 Apr 2021 19:36:54 +0000
Subject: [PATCH] feat(linear_algebra): Lagrange formulas for expanding `det`
 along a row or column (#6897)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR proves the full Lagrange formulas for writing the determinant of a `n+1 × n+1` matrix as an alternating sum of minors. @pechersky and @eric-wieser already put together enough of the pieces so that `simp` could apply this formula to matrices of a known size. In the end I still had to apply a couple of permutations (`fin.cycle_range` defined in #6815) to the entries to get to the "official" formula.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
---
 src/group_theory/perm/fin.lean        | 37 +++++++++++++
 src/linear_algebra/bilinear_form.lean |  9 +--
 src/linear_algebra/determinant.lean   | 80 +++++++++++++++++++++++++++
 test/matrix.lean                      | 19 +++++--
 4 files changed, 135 insertions(+), 10 deletions(-)

diff --git a/src/group_theory/perm/fin.lean b/src/group_theory/perm/fin.lean
index cb555f9d7be99..7d980935e0e02 100644
--- a/src/group_theory/perm/fin.lean
+++ b/src/group_theory/perm/fin.lean
@@ -189,6 +189,43 @@ end
   perm.sign (cycle_range i) = (-1) ^ (i : ℕ) :=
 by simp [cycle_range]
 
+@[simp] lemma succ_above_cycle_range {n : ℕ} (i j : fin n) :
+  i.succ.succ_above (i.cycle_range j) = swap 0 i.succ j.succ :=
+begin
+  cases n,
+  { rcases j with ⟨_, ⟨⟩⟩ },
+  rcases lt_trichotomy j i with hlt | heq | hgt,
+  { have : (j + 1).cast_succ = j.succ,
+    { ext, rw [coe_cast_succ, coe_succ, fin.coe_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)] },
+    rw [fin.cycle_range_of_lt hlt, fin.succ_above_below, this, swap_apply_of_ne_of_ne],
+    { apply fin.succ_ne_zero },
+    { exact (fin.succ_injective _).ne hlt.ne },
+    { rw fin.lt_iff_coe_lt_coe,
+      simpa [this] using hlt } },
+  { rw [heq, fin.cycle_range_self, fin.succ_above_below, swap_apply_right, fin.cast_succ_zero],
+    { rw fin.cast_succ_zero, apply fin.succ_pos } },
+  { rw [fin.cycle_range_of_gt hgt, fin.succ_above_above, swap_apply_of_ne_of_ne],
+    { apply fin.succ_ne_zero },
+    { apply (fin.succ_injective _).ne hgt.ne.symm },
+    { simpa [fin.le_iff_coe_le_coe] using hgt } },
+end
+
+@[simp] lemma cycle_range_succ_above {n : ℕ} (i : fin (n + 1)) (j : fin n) :
+  i.cycle_range (i.succ_above j) = j.succ :=
+begin
+  cases lt_or_ge j.cast_succ i with h h,
+  { rw [fin.succ_above_below _ _ h, fin.cycle_range_of_lt h, fin.coe_succ_eq_succ] },
+  { rw [fin.succ_above_above _ _ h, fin.cycle_range_of_gt (fin.le_cast_succ_iff.mp h)] }
+end
+
+@[simp] lemma cycle_range_symm_zero {n : ℕ} (i : fin (n + 1)) :
+  i.cycle_range.symm 0 = i :=
+i.cycle_range.injective (by simp)
+
+@[simp] lemma cycle_range_symm_succ {n : ℕ} (i : fin (n + 1)) (j : fin n) :
+  i.cycle_range.symm j.succ = i.succ_above j :=
+i.cycle_range.injective (by simp)
+
 end fin
 
 end cycle_range
diff --git a/src/linear_algebra/bilinear_form.lean b/src/linear_algebra/bilinear_form.lean
index d2ca3d9b990a3..a643f5354a5ed 100644
--- a/src/linear_algebra/bilinear_form.lean
+++ b/src/linear_algebra/bilinear_form.lean
@@ -254,10 +254,11 @@ def to_lin_hom : bilin_form R M →ₗ[R₂] M →ₗ[R₂] M →ₗ[R] R :=
     { to_fun := λ y, A x y,
       map_add' := A.bilin_add_right x,
       map_smul' := λ c, A.bilin_smul_right c x },
-    map_add' := λ x₁ x₂, by { ext, simp },
-    map_smul' := λ c x, by { ext y, simpa using smul_left (c • (1 : R)) x y } },
-  map_add' := λ A₁ A₂, by { ext, simp },
-  map_smul' := λ c A, by { ext, simp } }
+    map_add' := λ x₁ x₂, by { ext, simp only [linear_map.coe_mk, linear_map.add_apply, add_left] },
+    map_smul' := λ c x, by { ext, simp only [← algebra_map_smul R c x, algebra.smul_def,
+                                      linear_map.coe_mk, linear_map.smul_apply, smul_left] } },
+  map_add' := λ A₁ A₂, by { ext, simp only [linear_map.coe_mk, linear_map.add_apply, add_apply] },
+  map_smul' := λ c A, by { ext, simp only [linear_map.coe_mk, linear_map.smul_apply, smul_apply] } }
 
 variables {R₂}
 
diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
index 9743bbca02c99..426cfa06415d8 100644
--- a/src/linear_algebra/determinant.lean
+++ b/src/linear_algebra/determinant.lean
@@ -5,6 +5,7 @@ Authors: Kenny Lau, Chris Hughes, Tim Baanen
 -/
 import data.matrix.pequiv
 import data.fintype.card
+import group_theory.perm.fin
 import group_theory.perm.sign
 import algebra.algebra.basic
 import tactic.ring
@@ -96,6 +97,14 @@ begin
   simp [det_apply, card_eq_zero.mp h, perm_eq],
 end
 
+/-- Specialize `det_eq_one_of_card_eq_zero` to `fin 0`.
+
+This is especially useful in combination with the `det_succ_` lemmas,
+for computing the determinant of a matrix given in the `![...]` notation.
+-/
+@[simp] lemma det_fin_zero {A : matrix (fin 0) (fin 0) R}: det A = 1 :=
+det_eq_one_of_card_eq_zero (fintype.card_fin _)
+
 /-- If `n` has only one element, the determinant of an `n` by `n` matrix is just that element.
 Although `unique` implies `decidable_eq` and `fintype`, the instances might
 not be syntactically equal. Thus, we need to fill in the args explicitly. -/
@@ -403,4 +412,75 @@ begin
       rw [hx, from_blocks_apply₂₁], refl }}
 end
 
+/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along column 0. -/
+lemma det_succ_column_zero {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) R) :
+  det A = ∑ i : fin n.succ, (-1) ^ (i : ℕ) * A i 0 *
+    det (A.minor i.succ_above fin.succ) :=
+begin
+  rw [matrix.det_apply, finset.univ_perm_fin_succ, ← finset.univ_product_univ],
+  simp only [finset.sum_map, equiv.to_embedding_apply, finset.sum_product, matrix.minor],
+  refine finset.sum_congr rfl (λ i _, fin.cases _ (λ i, _) i),
+  { simp only [fin.prod_univ_succ, matrix.det_apply, finset.mul_sum,
+        equiv.perm.decompose_fin_symm_apply_zero, fin.coe_zero, one_mul,
+        equiv.perm.decompose_fin.symm_sign, equiv.swap_self, if_true, id.def, eq_self_iff_true,
+        equiv.perm.decompose_fin_symm_apply_succ, fin.succ_above_zero, equiv.coe_refl, pow_zero,
+        algebra.mul_smul_comm] },
+  -- `univ_perm_fin_succ` gives a different embedding of `perm (fin n)` into
+  -- `perm (fin n.succ)` than the determinant of the submatrix we want,
+  -- permute `A` so that we get the correct one.
+  have : (-1 : R) ^ (i : ℕ) = i.cycle_range.sign,
+  { simp [fin.sign_cycle_range] },
+  rw [fin.coe_succ, pow_succ, this, mul_assoc, mul_assoc, mul_left_comm ↑(equiv.perm.sign _),
+      ← det_permute, matrix.det_apply, finset.mul_sum, finset.mul_sum],
+  -- now we just need to move the corresponding parts to the same place
+  refine finset.sum_congr rfl (λ σ _, _),
+  rw [equiv.perm.decompose_fin.symm_sign, if_neg (fin.succ_ne_zero i)],
+  calc ((-1) * σ.sign : ℤ) • ∏ i', A (equiv.perm.decompose_fin.symm (fin.succ i, σ) i') i'
+      = ((-1) * σ.sign : ℤ) • (A (fin.succ i) 0 *
+        ∏ i', A (((fin.succ i).succ_above) (fin.cycle_range i (σ i'))) i'.succ) : _
+  ... = (-1) * (A (fin.succ i) 0 * (σ.sign : ℤ) •
+        ∏ i', A (((fin.succ i).succ_above) (fin.cycle_range i (σ i'))) i'.succ) : by simp,
+  simp only [fin.prod_univ_succ, fin.succ_above_cycle_range,
+      equiv.perm.decompose_fin_symm_apply_zero, equiv.perm.decompose_fin_symm_apply_succ]
+end
+
+/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along row 0. -/
+lemma det_succ_row_zero {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) R) :
+  det A = ∑ j : fin n.succ, (-1) ^ (j : ℕ) * A 0 j *
+    det (A.minor fin.succ j.succ_above) :=
+by { rw [← det_transpose A, det_succ_column_zero],
+     refine finset.sum_congr rfl (λ i _, _),
+     rw [← det_transpose],
+     simp only [transpose_apply, transpose_minor, transpose_transpose] }
+
+/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along row `i`. -/
+lemma det_succ_row {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) R) (i : fin n.succ) :
+  det A = ∑ j : fin n.succ, (-1) ^ (i + j : ℕ) * A i j *
+    det (A.minor i.succ_above j.succ_above) :=
+begin
+  simp_rw [pow_add, mul_assoc, ← mul_sum],
+  have : det A = (-1 : R) ^ (i : ℕ) * (i.cycle_range⁻¹).sign * det A,
+  { calc det A = ↑((-1 : units ℤ) ^ (i : ℕ) * (-1 : units ℤ) ^ (i : ℕ) : units ℤ) * det A :
+             by simp
+           ... = (-1 : R) ^ (i : ℕ) * (i.cycle_range⁻¹).sign * det A :
+             by simp [-int.units_mul_self] },
+  rw [this, mul_assoc],
+  congr,
+  rw [← det_permute, det_succ_row_zero],
+  refine finset.sum_congr rfl (λ j _, _),
+  rw [mul_assoc, matrix.minor, matrix.minor],
+  congr,
+  { rw [equiv.perm.inv_def, fin.cycle_range_symm_zero] },
+  { ext i' j',
+    rw [equiv.perm.inv_def, fin.cycle_range_symm_succ] },
+end
+
+/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along column `j`. -/
+lemma det_succ_column {n : ℕ} (A : matrix (fin n.succ) (fin n.succ) R) (j : fin n.succ) :
+  det A = ∑ i : fin n.succ, (-1) ^ (i + j : ℕ) * A i j *
+    det (A.minor i.succ_above j.succ_above) :=
+by { rw [← det_transpose, det_succ_row _ j],
+     refine finset.sum_congr rfl (λ i _, _),
+     rw [add_comm, ← det_transpose, transpose_apply, transpose_minor, transpose_transpose] }
+
 end matrix
diff --git a/test/matrix.lean b/test/matrix.lean
index d5006062da3e7..01aefc126484e 100644
--- a/test/matrix.lean
+++ b/test/matrix.lean
@@ -60,9 +60,12 @@ example {a b c d e f g h : α} : ![a, b, c, d, e, f, g, h] 99 = d := by simp
 example {α : Type*} [comm_ring α] {a b c d : α} :
   matrix.det ![![a, b], ![c, d]] = a * d - b * c :=
 begin
-  -- TODO: can we make this require less steering?
-  simp [matrix.det_apply', finset.univ_perm_fin_succ, ←finset.univ_product_univ, finset.sum_product,
-        fin.sum_univ_succ, fin.prod_univ_succ],
+  simp [matrix.det_succ_row_zero, fin.sum_univ_succ],
+  /-
+  Try this: simp only [matrix.det_succ_row_zero, fin.sum_univ_succ, det_fin_zero,
+      finset.sum_singleton, fin.sum_univ_zero, minor_apply, cons_val_zero, cons_val_succ,
+      fin.succ_above_zero, fin.coe_succ, fin.coe_zero],
+  -/
   ring
 end
 
@@ -70,9 +73,13 @@ example {α : Type*} [comm_ring α] (A : matrix (fin 3) (fin 3) α) {a b c d e f
         matrix.det ![![a, b, c], ![d, e, f], ![g, h, i]] =
           a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g :=
 begin
-  -- We utilize the `norm_swap` plugin for `norm_num` to reduce swap terms
-  norm_num [matrix.det_apply', finset.univ_perm_fin_succ, ←finset.univ_product_univ,
-            finset.sum_product, fin.sum_univ_succ, fin.prod_univ_succ],
+  simp [matrix.det_succ_row_zero, fin.sum_univ_succ],
+  /-
+  Try this: simp only [matrix.det_succ_row_zero, fin.sum_univ_succ, det_fin_zero,
+      finset.sum_singleton, fin.sum_univ_zero, minor_apply, cons_val_zero, cons_val_succ,
+      fin.succ_above_zero, fin.succ_succ_above_zero, fin.succ_succ_above_succ,
+      fin.coe_zero, fin.coe_succ, pow_zero, pow_add],
+   -/
   ring
 end