feat(linear_algebra/determinant): alternating maps as multiples of de…

…terminant (#10233)

Add the lemma that any alternating map with the same type as the
determinant map with respect to a basis is a multiple of the
determinant map (given by the value of the alternating map applied to
the basis vectors).

src/linear_algebra/alternating.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser, Zhangir Azerbayev
 -/
 
+import linear_algebra.multilinear.basis
 import linear_algebra.multilinear.tensor_product
 import linear_algebra.linear_independent
 import group_theory.perm.sign
@@ -156,6 +157,14 @@ f.to_multilinear_map.map_update_zero m i
 @[simp] lemma map_zero [nonempty ι] : f 0 = 0 :=
 f.to_multilinear_map.map_zero
 
+lemma map_eq_zero_of_not_injective (v : ι → M) (hv : ¬function.injective v) : f v = 0 :=
+begin
+  rw function.injective at hv,
+  push_neg at hv,
+  rcases hv with ⟨i₁, i₂, heq, hne⟩,
+  exact f.map_eq_zero_of_eq v heq hne
+end
+
 /-!
 ### Algebraic structure inherited from `multilinear_map`
 
@@ -765,3 +774,26 @@ begin
 end
 
 end coprod
+
+section basis
+
+open alternating_map
+
+variables {ι₁ : Type*} [fintype ι]
+variables {R' : Type*} {N₁ N₂ : Type*} [comm_semiring R'] [add_comm_monoid N₁] [add_comm_monoid N₂]
+variables [module R' N₁] [module R' N₂]
+
+/-- Two alternating maps indexed by a `fintype` are equal if they are equal when all arguments
+are distinct basis vectors. -/
+lemma basis.ext_alternating {f g : alternating_map R' N₁ N₂ ι} (e : basis ι₁ R' N₁)
+  (h : ∀ v : ι → ι₁, function.injective v → f (λ i, e (v i)) = g (λ i, e (v i))) : f = g :=
+begin
+  refine alternating_map.coe_multilinear_map_injective (basis.ext_multilinear e $ λ v, _),
+  by_cases hi : function.injective v,
+  { exact h v hi },
+  { have : ¬function.injective (λ i, e (v i)) := hi.imp function.injective.of_comp,
+    rw [coe_multilinear_map, coe_multilinear_map,
+        f.map_eq_zero_of_not_injective _ this, g.map_eq_zero_of_not_injective _ this], }
+end
+
+end basis

src/linear_algebra/determinant.lean

@@ -8,7 +8,7 @@ import linear_algebra.matrix.basis
 import linear_algebra.matrix.diagonal
 import linear_algebra.matrix.to_linear_equiv
 import linear_algebra.matrix.reindex
-import linear_algebra.multilinear.basic
+import linear_algebra.multilinear.basis
 import linear_algebra.dual
 import ring_theory.algebra_tower
 
@@ -368,6 +368,16 @@ end
 lemma basis.is_unit_det (e' : basis ι R M) : is_unit (e.det e') :=
 (is_basis_iff_det e).mp ⟨e'.linear_independent, e'.span_eq⟩
 
+/-- Any alternating map to `R` where `ι` has the cardinality of a basis equals the determinant
+map with respect to that basis, multiplied by the value of that alternating map on that basis. -/
+lemma alternating_map.eq_smul_basis_det (f : alternating_map R M R ι) : f = f e • e.det :=
+begin
+  refine basis.ext_alternating e (λ i h, _),
+  let σ : equiv.perm ι := equiv.of_bijective i (fintype.injective_iff_bijective.1 h),
+  change f (e ∘ σ) = (f e • e.det) (e ∘ σ),
+  simp [alternating_map.map_perm, basis.det_self]
+end
+
 variables {A : Type*} [comm_ring A] [is_domain A] [module A M]
 
 @[simp] lemma basis.det_comp (e : basis ι A M) (f : M →ₗ[A] M) (v : ι → M) :