chore(linear_algebra/determinant): redefine det using multilinear_map…

….alternatization (#6708)

This slightly changes the definitional unfolding of `matrix.det` (moving a function application outside a sum and adjusting the version of int-multiplication used).

By doing this, a large number of proofs become a trivial application of a more general statement about alternating maps.

`det_row_multilinear` already existed prior to this commit, but now `det` is defined in terms of it instead of the other way around.
We still need both, as otherwise we would break `M.det` dot notation, as `det_row_multilinear` does not have its argument expressed as a matrix.

src/linear_algebra/alternating.lean

@@ -144,6 +144,15 @@ f.to_multilinear_map.map_smul' v i r x
   f v = 0 :=
 f.map_eq_zero_of_eq' v i j h hij
 
+lemma map_coord_zero {m : ι → M} (i : ι) (h : m i = 0) : f m = 0 :=
+f.to_multilinear_map.map_coord_zero i h
+
+@[simp] lemma map_update_zero (m : ι → M) (i : ι) : f (update m i 0) = 0 :=
+f.to_multilinear_map.map_update_zero m i
+
+@[simp] lemma map_zero [nonempty ι] : f 0 = 0 :=
+f.to_multilinear_map.map_zero
+
 /-!
 ### Algebraic structure inherited from `multilinear_map`
 

src/linear_algebra/char_poly/coeff.lean

@@ -58,7 +58,7 @@ variable (M)
 lemma char_poly_sub_diagonal_degree_lt :
 (char_poly M - ∏ (i : n), (X - C (M i i))).degree < ↑(fintype.card n - 1) :=
 begin
-  rw [char_poly, det, ← insert_erase (mem_univ (equiv.refl n)),
+  rw [char_poly, det_apply', ← insert_erase (mem_univ (equiv.refl n)),
     sum_insert (not_mem_erase (equiv.refl n) univ), add_comm],
   simp only [char_matrix_apply_eq, one_mul, equiv.perm.sign_refl, id.def, int.cast_one,
     units.coe_one, add_sub_cancel, equiv.coe_refl],

src/linear_algebra/determinant.lean

@@ -9,6 +9,7 @@ import group_theory.perm.sign
 import algebra.algebra.basic
 import tactic.ring
 import linear_algebra.alternating
+import linear_algebra.pi
 
 /-!
 # Determinant of a matrix
@@ -45,12 +46,32 @@ variables {R : Type v} [comm_ring R]
 
 local notation `ε` σ:max := ((sign σ : ℤ ) : R)
 
+
+/-- `det` is an `alternating_map` in the rows of the matrix. -/
+def det_row_multilinear : alternating_map R (n → R) R n :=
+((multilinear_map.mk_pi_algebra R n R).comp_linear_map (linear_map.proj)).alternatization
+
 /-- The determinant of a matrix given by the Leibniz formula. -/
-definition det (M : matrix n n R) : R :=
-∑ σ : perm n, ε σ * ∏ i, M (σ i) i
+abbreviation det (M : matrix n n R) : R :=
+det_row_multilinear M
+
+lemma det_apply (M : matrix n n R) :
+  M.det = ∑ σ : perm n, (σ.sign : ℤ) • ∏ i, M (σ i) i :=
+multilinear_map.alternatization_apply _ M
+
+-- This is what the old definition was. We use it to avoid having to change the old proofs below
+lemma det_apply' (M : matrix n n R) :
+  M.det = ∑ σ : perm n, ε σ * ∏ i, M (σ i) i :=
+begin
+  rw det_apply,
+  have : ∀ (r : R) (z : ℤ), z • r = (z : R) * r := λ r z, by
+    rw [←gsmul_eq_smul, ←smul_eq_mul, ←gsmul_eq_smul_cast],
+  simp only [this],
+end
 
 @[simp] lemma det_diagonal {d : n → R} : det (diagonal d) = ∏ i, d i :=
 begin
+  rw det_apply',
   refine (finset.sum_eq_single 1 _ _).trans _,
   { intros σ h1 h2,
     cases not_forall.1 (mt equiv.ext h2) with x h3,
@@ -63,8 +84,7 @@ begin
 end
 
 @[simp] lemma det_zero (h : nonempty n) : det (0 : matrix n n R) = 0 :=
-by rw [← diagonal_zero, det_diagonal, finset.prod_const, ← fintype.card,
-  zero_pow (fintype.card_pos_iff.2 h)]
+(det_row_multilinear : alternating_map R (n → R) R n).map_zero
 
 @[simp] lemma det_one : det (1 : matrix n n R) = 1 :=
 by rw [← diagonal_one]; simp [-diagonal_one]
@@ -73,7 +93,7 @@ lemma det_eq_one_of_card_eq_zero {A : matrix n n R} (h : fintype.card n = 0) : d
 begin
   have perm_eq : (univ : finset (perm n)) = {1} :=
   univ_eq_singleton_of_card_one (1 : perm n) (by simp [card_univ, fintype.card_perm, h]),
-  simp [det, card_eq_zero.mp h, perm_eq],
+  simp [det_apply, card_eq_zero.mp h, perm_eq],
 end
 
 /-- If `n` has only one element, the determinant of an `n` by `n` matrix is just that element.
@@ -82,7 +102,7 @@ not be syntactically equal. Thus, we need to fill in the args explicitly. -/
 @[simp]
 lemma det_unique {n : Type*} [unique n] [decidable_eq n] [fintype n] (A : matrix n n R) :
   det A = A (default n) (default n) :=
-by simp [det, univ_unique]
+by simp [det_apply, univ_unique]
 
 lemma det_eq_elem_of_card_eq_one {A : matrix n n R} (h : fintype.card n = 1) (k : n) :
   det A = A k k :=
@@ -91,7 +111,7 @@ begin
   { apply univ_eq_singleton_of_card_one (1 : perm n),
     simp [card_univ, fintype.card_perm, h] },
   have h2 := univ_eq_singleton_of_card_one k h,
-  simp [det, h1, h2],
+  simp [det_apply, h1, h2],
 end
 
 lemma det_mul_aux {M N : matrix n n R} {p : n → n} (H : ¬bijective p) :
@@ -117,7 +137,7 @@ end
 
 @[simp] lemma det_mul (M N : matrix n n R) : det (M ⬝ N) = det M * det N :=
 calc det (M ⬝ N) = ∑ p : n → n, ∑ σ : perm n, ε σ * ∏ i, (M (σ i) (p i) * N (p i) i) :
-  by simp only [det, mul_apply, prod_univ_sum, mul_sum,
+  by simp only [det_apply', mul_apply, prod_univ_sum, mul_sum,
     fintype.pi_finset_univ]; rw [finset.sum_comm]
 ... = ∑ p in (@univ (n → n) _).filter bijective, ∑ σ : perm n,
     ε σ * ∏ i, (M (σ i) (p i) * N (p i) i) :
@@ -128,7 +148,7 @@ calc det (M ⬝ N) = ∑ p : n → n, ∑ σ : perm n, ε σ * ∏ i, (M (σ i)
     (λ _ _, rfl) (λ _ _ _ _ h, by injection h)
     (λ b _, ⟨b, mem_filter.2 ⟨mem_univ _, b.bijective⟩, injective_coe_fn rfl⟩)
 ... = ∑ σ : perm n, ∑ τ : perm n, (∏ i, N (σ i) i) * ε τ * (∏ j, M (τ j) (σ j)) :
-  by simp [mul_sum, det, mul_comm, mul_left_comm, prod_mul_distrib, mul_assoc]
+  by simp [mul_sum, det_apply', mul_comm, mul_left_comm, prod_mul_distrib, mul_assoc]
 ... = ∑ σ : perm n, ∑ τ : perm n, (((∏ i, N (σ i) i) * (ε σ * ε τ)) * ∏ i, M (τ i) i) :
   sum_congr rfl (λ σ _, sum_bij (λ τ _, τ * σ⁻¹) (λ _ _, mem_univ _)
     (λ τ _,
@@ -140,7 +160,7 @@ calc det (M ⬝ N) = ∑ p : n → n, ∑ σ : perm n, ε σ * ∏ i, (M (σ i)
         ... = ε τ : by simp,
       by rw h; simp [this, mul_comm, mul_assoc, mul_left_comm])
     (λ _ _ _ _, mul_right_cancel) (λ τ _, ⟨τ * σ, by simp⟩))
-... = det M * det N : by simp [det, mul_assoc, mul_sum, mul_comm, mul_left_comm]
+... = det M * det N : by simp [det_apply', mul_assoc, mul_sum, mul_comm, mul_left_comm]
 
 instance : is_monoid_hom (det : matrix n n R → R) :=
 { map_one := det_one,
@@ -149,6 +169,7 @@ instance : is_monoid_hom (det : matrix n n R → R) :=
 /-- Transposing a matrix preserves the determinant. -/
 @[simp] lemma det_transpose (M : matrix n n R) : Mᵀ.det = M.det :=
 begin
+  rw [det_apply', det_apply'],
   apply sum_bij (λ σ _, σ⁻¹),
   { intros σ _, apply mem_univ },
   { intros σ _,
@@ -163,28 +184,20 @@ begin
   { 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 τ _,
-    rw [←mul_assoc, sign_mul, coe_coe, ←int.cast_mul, ←units.coe_mul, ←mul_assoc,
-        int.units_mul_self, one_mul],
-    congr,
-    ext i,
-    apply pequiv.equiv_to_pequiv_to_matrix },
-  { intros τ τ' _ _, exact (mul_right_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]
+begin
+  have : (σ.sign : ℤ) • M.det = (σ.sign * M.det : R),
+  { rw [coe_coe, ←gsmul_eq_smul, ←smul_eq_mul, ←gsmul_eq_smul_cast] },
+  exact ((det_row_multilinear : alternating_map R (n → R) R n).map_perm M σ).trans this,
+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 :=
+by rw [←matrix.mul_one (σ.to_pequiv.to_matrix : matrix n n R), pequiv.to_pequiv_mul_matrix,
+  det_permute, det_one, mul_one]
 
 @[simp] lemma det_smul {A : matrix n n R} {c : R} : det (c • A) = c ^ fintype.card n * det A :=
 calc det (c • A) = det (matrix.mul (diagonal (λ _, c)) A) : by rw [smul_eq_diagonal_mul]
@@ -197,7 +210,7 @@ variables {S : Type w} [comm_ring S]
 
 lemma ring_hom.map_det {M : matrix n n R} {f : R →+* S} :
   f M.det = matrix.det (f.map_matrix M) :=
-by simp [matrix.det, f.map_sum, f.map_prod]
+by simp [matrix.det_apply', f.map_sum, f.map_prod]
 
 lemma alg_hom.map_det [algebra R S] {T : Type z} [comm_ring T] [algebra R T]
   {M : matrix n n S} {f : S →ₐ[R] T} :
@@ -214,15 +227,7 @@ Prove that a matrix with a repeated column has determinant equal to zero.
 -/
 
 lemma det_eq_zero_of_row_eq_zero {A : matrix n n R} (i : n) (h : ∀ j, A i j = 0) : det A = 0 :=
-begin
-  rw [←det_transpose, det],
-  convert @sum_const_zero _ _ (univ : finset (perm n)) _,
-  ext σ,
-  convert mul_zero ↑(sign σ),
-  apply prod_eq_zero (mem_univ i),
-  rw [transpose_apply],
-  apply h
-end
+(det_row_multilinear : alternating_map R (n → R) R n).map_coord_zero i (funext h)
 
 lemma det_eq_zero_of_column_eq_zero {A : matrix n n R} (j : n) (h : ∀ i, A i j = 0) : det A = 0 :=
 by { rw ← det_transpose, exact det_eq_zero_of_row_eq_zero j h, }
@@ -231,83 +236,37 @@ variables {M : matrix n n R} {i j : n}
 
 /-- If a matrix has a repeated row, the determinant will be zero. -/
 theorem det_zero_of_row_eq (i_ne_j : i ≠ j) (hij : M i = M j) : M.det = 0 :=
-begin
-  apply finset.sum_involution
-    (λ σ _, swap i j * σ)
-    (λ σ _, _)
-    (λ σ _ _, (not_congr swap_mul_eq_iff).mpr i_ne_j)
-    (λ σ _, finset.mem_univ _)
-    (λ σ _, swap_mul_involutive i j σ),
-  convert add_right_neg (↑↑(sign σ) * ∏ i, M (σ i) i),
-  rw neg_mul_eq_neg_mul,
-  congr,
-  { rw [sign_mul, sign_swap i_ne_j], norm_num },
-  { ext j, rw [perm.mul_apply, apply_swap_eq_self hij], }
-end
+(det_row_multilinear : alternating_map R (n → R) R n).map_eq_zero_of_eq M hij i_ne_j
 
 end det_zero
 
-lemma det_update_column_add (M : matrix n n R) (j : n) (u v : n → R) :
-  det (update_column M j $ u + v) = det (update_column M j u) + det (update_column M j v) :=
-begin
-  simp only [det],
-  have : ∀ σ : perm n, ∏ i, M.update_column j (u + v) (σ i) i =
-                       ∏ i, M.update_column j u (σ i) i + ∏ i, M.update_column j v (σ i) i,
-  { intros σ,
-    simp only [update_column_apply, prod_ite, filter_eq',
-               finset.prod_singleton, finset.mem_univ, if_true, pi.add_apply, add_mul] },
-  rw [← sum_add_distrib],
-  apply sum_congr rfl,
-  intros x _,
-  rw [this, mul_add]
-end
-
 lemma det_update_row_add (M : matrix n n R) (j : n) (u v : n → R) :
   det (update_row M j $ u + v) = det (update_row M j u) + det (update_row M j v) :=
-begin
-  rw [← det_transpose, ← update_column_transpose, det_update_column_add],
-  simp [update_column_transpose, det_transpose]
-end
+(det_row_multilinear : alternating_map R (n → R) R n).map_add M j u v
 
-lemma det_update_column_smul (M : matrix n n R) (j : n) (s : R) (u : n → R) :
-  det (update_column M j $ s • u) = s * det (update_column M j u) :=
+lemma det_update_column_add (M : matrix n n R) (j : n) (u v : n → R) :
+  det (update_column M j $ u + v) = det (update_column M j u) + det (update_column M j v) :=
 begin
-  simp only [det],
-  have : ∀ σ : perm n, ∏ i, M.update_column j (s • u) (σ i) i =
-    s * ∏ i, M.update_column j u (σ i) i,
-  { intros σ,
-    simp only [update_column_apply, prod_ite, filter_eq', finset.prod_singleton, finset.mem_univ,
-               if_true, algebra.id.smul_eq_mul, pi.smul_apply],
-    ring },
-  rw mul_sum,
-  apply sum_congr rfl,
-  intros x _,
-  rw this,
-  ring
+  rw [← det_transpose, ← update_row_transpose, det_update_row_add],
+  simp [update_row_transpose, det_transpose]
 end
 
 lemma det_update_row_smul (M : matrix n n R) (j : n) (s : R) (u : n → R) :
   det (update_row M j $ s • u) = s * det (update_row M j u) :=
+(det_row_multilinear : alternating_map R (n → R) R n).map_smul M j s u
+
+lemma det_update_column_smul (M : matrix n n R) (j : n) (s : R) (u : n → R) :
+  det (update_column M j $ s • u) = s * det (update_column M j u) :=
 begin
-  rw [← det_transpose, ← update_column_transpose, det_update_column_smul],
-  simp [update_column_transpose, det_transpose]
+  rw [← det_transpose, ← update_row_transpose, det_update_row_smul],
+  simp [update_row_transpose, det_transpose]
 end
 
-/-- `det` is an alternating multilinear map over the rows of the matrix.
-
-See also `is_basis.det`. -/
-@[simps apply]
-def det_row_multilinear : alternating_map R (n → R) R n:=
-{ to_fun := det,
-  map_add' := det_update_row_add,
-  map_smul' := det_update_row_smul,
-  map_eq_zero_of_eq' := λ M i j h hij, det_zero_of_row_eq hij h }
-
 @[simp] lemma det_block_diagonal {o : Type*} [fintype o] [decidable_eq o] (M : o → matrix n n R) :
   (block_diagonal M).det = ∏ k, (M k).det :=
 begin
   -- Rewrite the determinants as a sum over permutations.
-  unfold det,
+  simp_rw [det_apply'],
   -- The right hand side is a product of sums, rewrite it as a sum of products.
   rw finset.prod_sum,
   simp_rw [finset.mem_univ, finset.prod_attach_univ, finset.univ_pi_univ],
@@ -369,7 +328,7 @@ the determinants of the diagonal blocks. For the generalization to any number of
 lemma upper_two_block_triangular_det (A : matrix m m R) (B : matrix m n R) (D : matrix n n R) :
   (matrix.from_blocks A B 0 D).det = A.det * D.det :=
 begin
-  unfold det,
+  simp_rw det_apply',
   rw sum_mul_sum,
   let preserving_A : finset (perm (m ⊕ n)) :=
     univ.filter (λ σ, ∀ x, ∃ y, sum.inl y = (σ (sum.inl x))),

src/linear_algebra/matrix.lean

@@ -949,7 +949,7 @@ lemma det_reindex_self' [decidable_eq m] [decidable_eq n] [comm_ring R]
   (e : m ≃ n) (A : matrix m m R) :
   det (λ i j, A (e.symm i) (e.symm j)) = det A :=
 begin
-  unfold det,
+  rw [det_apply', det_apply'],
   apply finset.sum_bij' (λ σ _, equiv.perm_congr e.symm σ) _ _ (λ σ _, equiv.perm_congr e σ),
   { intros σ _, ext, simp only [equiv.symm_symm, equiv.perm_congr_apply, equiv.apply_symm_apply] },
   { intros σ _, ext, simp only [equiv.symm_symm, equiv.perm_congr_apply, equiv.symm_apply_apply] },
@@ -1185,7 +1185,7 @@ lemma det_to_block (M : matrix m m R) (p : m → Prop) [decidable_pred p] :
     (to_block M (λ j, ¬p j) p) (to_block M (λ j, ¬p j) (λ j, ¬p j))).det :=
 begin
   rw ← matrix.det_reindex_self (equiv.sum_compl p).symm M,
-  unfold det,
+  rw [det_apply', det_apply'],
   congr, ext σ, congr, ext,
   generalize hy : σ x = y,
   cases x; cases y;

src/linear_algebra/nonsingular_inverse.lean

@@ -66,31 +66,8 @@ variables (A : matrix n n α) (b : n → α)
 def cramer_map (i : n) : α := (A.update_column i b).det
 
 lemma cramer_map_is_linear (i : n) : is_linear_map α (λ b, cramer_map A b i) :=
-begin
-  have : Π {f : n → n} {i : n} (x : n → α),
-    (∏ i' : n, (update_column A i x) (f i') i')
-    = (∏ i' : n, if i' = i then x (f i') else A (f i') i'),
-  { intros, congr' with i', apply update_column_apply, },
-  split,
-  { intros x y,
-    repeat { rw [cramer_map, det] },
-    rw [←sum_add_distrib],
-    congr' with σ,
-    rw [←mul_add ↑↑(sign σ)],
-    congr,
-    repeat { erw [this, finset.prod_ite] },
-    erw [finset.filter_eq', if_pos (mem_univ i), prod_singleton, prod_singleton,
-      prod_singleton, ←add_mul],
-    refl },
-  { intros c x,
-    repeat { rw [cramer_map, det] },
-    rw [smul_eq_mul, mul_sum],
-    congr' with σ,
-    rw [←mul_assoc, mul_comm c, mul_assoc], congr,
-    repeat { erw [this, finset.prod_ite] },
-    erw [finset.filter_eq', if_pos (mem_univ i),
-      prod_singleton, prod_singleton, mul_assoc], }
-end
+{ map_add := det_update_column_add _ _,
+  map_smul := det_update_column_smul _ _ }
 
 lemma cramer_is_linear : is_linear_map α (cramer_map A) :=
 begin
@@ -171,6 +148,7 @@ lemma adjugate_transpose (A : matrix n n α) : (adjugate A)ᵀ = adjugate (Aᵀ)
 begin
   ext i j,
   rw [transpose_apply, adjugate_apply, adjugate_apply, update_row_transpose, det_transpose],
+  rw [det_apply', det_apply'],
   apply finset.sum_congr rfl,
   intros σ _,
   congr' 1,
@@ -242,13 +220,9 @@ h (adjugate A).det (calc A.det * (adjugate A).det = (A ⬝ adjugate A).det   : (
 
 lemma adjugate_eq_one_of_card_eq_one {A : matrix n n α} (h : fintype.card n = 1) : adjugate A = 1 :=
 begin
+  haveI : subsingleton n := fintype.card_le_one_iff_subsingleton.mp h.le,
   ext i j,
-  have univ_eq_i := univ_eq_singleton_of_card_one i h,
-  have univ_eq_j := univ_eq_singleton_of_card_one j h,
-  have i_eq_j : i = j := singleton_inj.mp (by rw [←univ_eq_i, univ_eq_j]),
-  have perm_eq : (univ : finset (perm n)) = {1} :=
-    univ_eq_singleton_of_card_one (1 : perm n) (by simp [card_univ, fintype.card_perm, h]),
-  simp [adjugate_apply, det, univ_eq_i, perm_eq, i_eq_j]
+  simp [subsingleton.elim i j, adjugate_apply, det_eq_elem_of_card_eq_one h j],
 end
 
 @[simp] lemma adjugate_zero (h : 1 < fintype.card n) : adjugate (0 : matrix n n α) = 0 :=