feat(linear_algebra/*): Use alternating maps for wedge and determinant (#5124)

This :

* Adds `exterior_algebra.ι_multi`, where `ι_multi ![a, b ,c]` = `ι a * ι b * ι c`
* Makes `det_row_multilinear` an `alternating_map`
* Makes `is_basis.det` an `alternating_map`

Author: eric-wieser

src/linear_algebra/determinant.lean

@@ -8,7 +8,7 @@ import data.fintype.card
 import group_theory.perm.sign
 import algebra.algebra.basic
 import tactic.ring
-import linear_algebra.multilinear
+import linear_algebra.alternating
 
 universes u v w z
 open equiv equiv.perm finset function
@@ -274,14 +274,15 @@ begin
   simp [update_column_transpose, det_transpose]
 end
 
-/-- `det` is a multilinear map over the rows of the matrix.
+/-- `det` is an alternating multilinear map over the rows of the matrix.
 
 See also `is_basis.det`. -/
 @[simps apply]
-def det_row_multilinear : multilinear_map R (λ (i : n), n → R) R :=
+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_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 :=

src/linear_algebra/exterior_algebra.lean

@@ -6,6 +6,7 @@ Authors: Zhangir Azerbayev, Adam Topaz, Eric Wieser.
 
 import algebra.ring_quot
 import linear_algebra.tensor_algebra
+import linear_algebra.alternating
 import group_theory.perm.sign
 
 /-!
@@ -31,6 +32,10 @@ of the exterior algebra.
 1. `ι_comp_lift` is  fact that the composition of `ι R` with `lift R f cond` agrees with `f`.
 2. `lift_unique` ensures the uniqueness of `lift R f cond` with respect to 1.
 
+## Definitions
+
+* `ι_multi` is the `alternating_map` corresponding to the wedge product of `ι R m` terms.
+
 ## Implementation details
 
 The exterior algebra of `M` is constructed as a quotient of the tensor algebra, as follows.
@@ -156,4 +161,58 @@ begin
   simp only [h],
 end
 
+@[simp]
+lemma ι_add_mul_swap (x y : M) : ι R x * ι R y + ι R y * ι R x = 0 :=
+calc _ = ι R (x + y) * ι R (x + y) : by simp [mul_add, add_mul]
+   ... = _ : ι_square_zero _
+
+lemma ι_mul_prod_list {n : ℕ} (f : fin n → M) (i : fin n) :
+  (ι R $ f i) * (list.of_fn $ λ i, ι R $ f i).prod = 0 :=
+begin
+  induction n with n hn,
+  { exact i.elim0, },
+  { rw [list.of_fn_succ, list.prod_cons, ←mul_assoc],
+    by_cases h : i = 0,
+    { rw [h, ι_square_zero, zero_mul], },
+    { replace hn := congr_arg ((*) $ ι R $ f 0) (hn (λ i, f $ fin.succ i) (i.pred h)),
+      simp only at hn,
+      rw [fin.succ_pred, ←mul_assoc, mul_zero] at hn,
+      refine (eq_zero_iff_eq_zero_of_add_eq_zero _).mp hn,
+      rw [← add_mul, ι_add_mul_swap, zero_mul], } }
+end
+
+variables (R)
+/-- The product of `n` terms of the form `ι R m` is an alternating map.
+
+This is a special case of `multilinear_map.mk_pi_algebra_fin` -/
+def ι_multi (n : ℕ) :
+  alternating_map R M (exterior_algebra R M) (fin n) :=
+let F := (multilinear_map.mk_pi_algebra_fin R n (exterior_algebra R M)).comp_linear_map (λ i, ι R)
+in
+{ map_eq_zero_of_eq' := λ f x y hfxy hxy, begin
+    rw [multilinear_map.comp_linear_map_apply, multilinear_map.mk_pi_algebra_fin_apply],
+    wlog h : x < y := lt_or_gt_of_ne hxy using x y,
+    clear hxy,
+    induction n with n hn generalizing x y,
+    { exact x.elim0, },
+    { rw [list.of_fn_succ, list.prod_cons],
+      by_cases hx : x = 0,
+      -- one of the repeated terms is on the left
+      { rw hx at hfxy h,
+        rw [hfxy, ←fin.succ_pred y (ne_of_lt h).symm],
+        exact ι_mul_prod_list (f ∘ fin.succ) _, },
+      -- ignore the left-most term and induct on the remaining ones, decrementing indices
+      { convert mul_zero _,
+        refine hn (λ i, f $ fin.succ i)
+          (x.pred hx) (y.pred (ne_of_lt $ lt_of_le_of_lt x.zero_le h).symm)
+          (fin.pred_lt_pred_iff.mpr h) _,
+        simp only [fin.succ_pred],
+        exact hfxy, } }
+  end,
+  to_fun := F, ..F}
+variables {R}
+
+lemma ι_multi_apply {n : ℕ} (v : fin n → M) :
+  ι_multi R n v = (list.of_fn $ λ i, ι R (v i)).prod := rfl
+
 end exterior_algebra

src/linear_algebra/matrix.lean

@@ -210,10 +210,18 @@ begin
     contradiction }
 end
 
+lemma linear_map.to_matrix_transpose_apply (f : M₁ →ₗ[R] M₂) (j : n) :
+  (linear_map.to_matrix hv₁ hv₂ f)ᵀ j = hv₂.equiv_fun (f (v₁ j)) :=
+funext $ λ i, f.to_matrix_apply _ _ i j
+
 lemma linear_map.to_matrix_apply' (f : M₁ →ₗ[R] M₂) (i : m) (j : n) :
   linear_map.to_matrix hv₁ hv₂ f i j = hv₂.repr (f (v₁ j)) i :=
 linear_map.to_matrix_apply hv₁ hv₂ f i j
 
+lemma linear_map.to_matrix_transpose_apply' (f : M₁ →ₗ[R] M₂) (j : n) :
+  (linear_map.to_matrix hv₁ hv₂ f)ᵀ j = hv₂.repr (f (v₁ j)) :=
+linear_map.to_matrix_transpose_apply hv₁ hv₂ f j
+
 lemma matrix.to_lin_apply (M : matrix m n R) (v : M₁) :
   matrix.to_lin hv₁ hv₂ M v = ∑ j, M.mul_vec (hv₁.equiv_fun v) j • v₂ j :=
 show hv₂.equiv_fun.symm (matrix.to_lin' M (hv₁.equiv_fun v)) = _,
@@ -286,6 +294,9 @@ namespace is_basis
 lemma to_matrix_apply : he.to_matrix v i j = he.equiv_fun (v j) i :=
 rfl
 
+lemma to_matrix_transpose_apply : (he.to_matrix v)ᵀ j = he.repr (v j) :=
+funext $ (λ _, rfl)
+
 lemma to_matrix_eq_to_matrix_constr [decidable_eq ι] (v : ι → M) :
   he.to_matrix v = linear_map.to_matrix he he (he.constr v) :=
 by { ext, simp [is_basis.to_matrix_apply, linear_map.to_matrix_apply] }
@@ -409,8 +420,9 @@ def linear_equiv.of_is_unit_det {f : M →ₗ[R] M'} {hv : is_basis R v} {hv' :
 
 variables {e : ι → M} (he : is_basis R e)
 
-/-- The determinant of a family of vectors with respect to some basis, as a multilinear map. -/
-def is_basis.det : multilinear_map R (λ i : ι, M) R :=
+/-- The determinant of a family of vectors with respect to some basis, as an alternating
+multilinear map. -/
+def is_basis.det : alternating_map R M R ι :=
 { to_fun := λ v, det (he.to_matrix v),
   map_add' := begin
     intros v i x y,
@@ -421,6 +433,13 @@ def is_basis.det : multilinear_map R (λ i : ι, M) R :=
     intros u i c x,
     simp only [he.to_matrix_update, algebra.id.smul_eq_mul, map_smul_of_tower],
     apply det_update_column_smul
+  end,
+  map_eq_zero_of_eq' := begin
+    intros v i j h hij,
+    rw [←function.update_eq_self i v, h, ←det_transpose, he.to_matrix_update,
+        ←update_row_transpose, ←he.to_matrix_transpose_apply],
+    apply det_zero_of_row_eq hij,
+    rw [update_row_ne hij.symm, update_row_self],
   end }
 
 lemma is_basis.det_apply (v : ι → M) : he.det v = det (he.to_matrix v) := rfl