feat(linear_algebra/determinant): the determinant associated to the s…

…tandard basis of the free module is the usual matrix determinant (#10278)

Formalized as part of the Sphere Eversion project.

src/linear_algebra/determinant.lean

@@ -401,6 +401,12 @@ lemma basis.det_map (b : basis ι R M) (f : M ≃ₗ[R] M') (v : ι → M') :
   (b.map f).det v = b.det (f.symm ∘ v) :=
 by { rw [basis.det_apply, basis.to_matrix_map, basis.det_apply] }
 
+@[simp] lemma pi.basis_fun_det : (pi.basis_fun R ι).det = matrix.det_row_alternating :=
+begin
+  ext M,
+  rw [basis.det_apply, basis.coe_pi_basis_fun.to_matrix_eq_transpose, det_transpose],
+end
+
 /-- If we fix a background basis `e`, then for any other basis `v`, we can characterise the
 coordinates provided by `v` in terms of determinants relative to `e`. -/
 lemma basis.det_smul_mk_coord_eq_det_update {v : ι → M}

src/linear_algebra/matrix/basis.lean

@@ -61,6 +61,11 @@ lemma to_matrix_eq_to_matrix_constr [fintype ι] [decidable_eq ι] (v : ι → M
   e.to_matrix v = linear_map.to_matrix e e (e.constr ℕ v) :=
 by { ext, rw [basis.to_matrix_apply, linear_map.to_matrix_apply, basis.constr_basis] }
 
+-- TODO (maybe) Adjust the definition of `basis.to_matrix` to eliminate the transpose.
+lemma coe_pi_basis_fun.to_matrix_eq_transpose [fintype ι] :
+  ((pi.basis_fun R ι).to_matrix : matrix ι ι R → matrix ι ι R) = matrix.transpose :=
+by { ext M i j, refl, }
+
 @[simp] lemma to_matrix_self [decidable_eq ι] : e.to_matrix e = 1 :=
 begin
   rw basis.to_matrix,

src/linear_algebra/matrix/determinant.lean

@@ -21,7 +21,7 @@ This file defines the determinant of a matrix, `matrix.det`, and its essential p
 ## Main definitions
 
  - `matrix.det`: the determinant of a square matrix, as a sum over permutations
- - `matrix.det_row_multilinear`: the determinant, as an `alternating_map` in the rows of the matrix
+ - `matrix.det_row_alternating`: the determinant, as an `alternating_map` in the rows of the matrix
 
 ## Main results
 
@@ -50,12 +50,12 @@ 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 :=
+def det_row_alternating : 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. -/
 abbreviation det (M : matrix n n R) : R :=
-det_row_multilinear M
+det_row_alternating M
 
 lemma det_apply (M : matrix n n R) :
   M.det = ∑ σ : perm n, σ.sign • ∏ i, M (σ i) i :=
@@ -81,7 +81,7 @@ begin
 end
 
 @[simp] lemma det_zero (h : nonempty n) : det (0 : matrix n n R) = 0 :=
-(det_row_multilinear : alternating_map R (n → R) R n).map_zero
+(det_row_alternating : 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]
@@ -206,7 +206,7 @@ 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 :=
-((det_row_multilinear : alternating_map R (n → R) R n).map_perm M σ).trans
+((det_row_alternating : alternating_map R (n → R) R n).map_perm M σ).trans
   (by simp [units.smul_def])
 
 /-- Permuting rows and columns with the same equivalence has no effect. -/
@@ -294,7 +294,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 :=
-(det_row_multilinear : alternating_map R (n → R) R n).map_coord_zero i (funext h)
+(det_row_alternating : 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, }
@@ -303,7 +303,7 @@ 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 :=
-(det_row_multilinear : alternating_map R (n → R) R n).map_eq_zero_of_eq M hij i_ne_j
+(det_row_alternating : alternating_map R (n → R) R n).map_eq_zero_of_eq M hij i_ne_j
 
 /-- If a matrix has a repeated column, the determinant will be zero. -/
 theorem det_zero_of_column_eq (i_ne_j : i ≠ j) (hij : ∀ k, M k i = M k j) : M.det = 0 :=
@@ -313,7 +313,7 @@ end det_zero
 
 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) :=
-(det_row_multilinear : alternating_map R (n → R) R n).map_add M j u v
+(det_row_alternating : alternating_map R (n → R) R n).map_add M j u v
 
 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) :=
@@ -324,7 +324,7 @@ 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
+(det_row_alternating : 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) :=