feat(linear_algebra): determinant of vectors in a basis (#3919)

From the sphere eversion project, define the determinant of a family of vectors with respects to a basis. 

The main result is `is_basis.iff_det` asserting a family of vectors is a basis iff its determinant in some basis is invertible.

Also renames `equiv_fun_basis` to `is_basis.equiv_fun` and `equiv_fun_basis_symm_apply` to `is_basis.equiv_fun_symm_apply`, in order to use dot notation.

Co-authored-by: Anne Baanen t.baanen@vu.nl



Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

Author: PatrickMassot

src/algebra/big_operators/pi.lean

@@ -37,6 +37,11 @@ lemma finset.prod_apply {α : Type*} {β : α → Type*} {γ} [∀a, comm_monoid
 show (s.val.map g).prod a = (s.val.map (λc, g c a)).prod,
   by rw [pi.multiset_prod_apply, multiset.map_map]
 
+@[simp, to_additive]
+lemma fintype.prod_apply {α : Type*} {β : α → Type*} {γ : Type*} [fintype γ]
+  [∀a, comm_monoid (β a)] (a : α) (g : γ → Πa, β a) : (∏ c, g c) a = ∏ c, g c a :=
+finset.prod_apply a finset.univ g
+
 @[to_additive prod_mk_sum]
 lemma prod_mk_prod {α β γ : Type*} [comm_monoid α] [comm_monoid β] (s : finset γ)
   (f : γ → α) (g : γ → β) : (∏ x in s, f x, ∏ x in s, g x) = ∏ x in s, (f x, g x) :=

src/analysis/normed_space/finite_dimension.lean

@@ -74,13 +74,13 @@ all norms are equivalent in finite dimension.
 This statement is superceded by the fact that every linear map on a finite-dimensional space is
 continuous, in `linear_map.continuous_of_finite_dimensional`. -/
 lemma continuous_equiv_fun_basis {ι : Type v} [fintype ι] (ξ : ι → E) (hξ : is_basis 𝕜 ξ) :
-  continuous (equiv_fun_basis hξ) :=
+  continuous hξ.equiv_fun :=
 begin
   unfreezingI { induction hn : fintype.card ι with n IH generalizing ι E },
   { apply linear_map.continuous_of_bound _ 0 (λx, _),
-    have : equiv_fun_basis hξ x = 0,
+    have : hξ.equiv_fun x = 0,
       by { ext i, exact (fintype.card_eq_zero_iff.1 hn i).elim },
-    change ∥equiv_fun_basis hξ x∥ ≤ 0 * ∥x∥,
+    change ∥hξ.equiv_fun x∥ ≤ 0 * ∥x∥,
     rw this,
     simp [norm_nonneg] },
   { haveI : finite_dimensional 𝕜 E := of_finite_basis hξ,
@@ -90,11 +90,11 @@ begin
     { assume s s_dim,
       rcases exists_is_basis_finite 𝕜 s with ⟨b, b_basis, b_finite⟩,
       letI : fintype b := finite.fintype b_finite,
-      have U : uniform_embedding (equiv_fun_basis b_basis).symm.to_equiv,
+      have U : uniform_embedding b_basis.equiv_fun.symm.to_equiv,
       { have : fintype.card b = n,
           by { rw ← s_dim, exact (findim_eq_card_basis b_basis).symm },
-        have : continuous (equiv_fun_basis b_basis) := IH (subtype.val : b → s) b_basis this,
-        exact (equiv_fun_basis b_basis).symm.uniform_embedding (linear_map.continuous_on_pi _) this },
+        have : continuous b_basis.equiv_fun := IH (subtype.val : b → s) b_basis this,
+        exact b_basis.equiv_fun.symm.uniform_embedding (linear_map.continuous_on_pi _) this },
       have : is_complete (s : set E),
         from complete_space_coe_iff_is_complete.1 ((complete_space_congr U).1 (by apply_instance)),
       exact this.is_closed },
@@ -124,9 +124,9 @@ begin
       exact linear_map.continuous_iff_is_closed_ker.2 this },
     -- third step: applying the continuity to the linear form corresponding to a coefficient in the
     -- basis decomposition, deduce that all such coefficients are controlled in terms of the norm
-    have : ∀i:ι, ∃C, 0 ≤ C ∧ ∀(x:E), ∥equiv_fun_basis hξ x i∥ ≤ C * ∥x∥,
+    have : ∀i:ι, ∃C, 0 ≤ C ∧ ∀(x:E), ∥hξ.equiv_fun x i∥ ≤ C * ∥x∥,
     { assume i,
-      let f : E →ₗ[𝕜] 𝕜 := (linear_map.proj i).comp (equiv_fun_basis hξ),
+      let f : E →ₗ[𝕜] 𝕜 := (linear_map.proj i).comp hξ.equiv_fun,
       let f' : E →L[𝕜] 𝕜 := { cont := H₂ f, ..f },
       exact ⟨∥f'∥, norm_nonneg _, λx, continuous_linear_map.le_op_norm f' x⟩ },
     -- fourth step: combine the bound on each coefficient to get a global bound and the continuity
@@ -149,12 +149,12 @@ begin
   -- argue that all linear maps there are continuous.
   rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
   letI : fintype b := finite.fintype b_finite,
-  have A : continuous (equiv_fun_basis b_basis) :=
+  have A : continuous b_basis.equiv_fun :=
     continuous_equiv_fun_basis _ b_basis,
-  have B : continuous (f.comp ((equiv_fun_basis b_basis).symm : (b → 𝕜) →ₗ[𝕜] E)) :=
+  have B : continuous (f.comp (b_basis.equiv_fun.symm : (b → 𝕜) →ₗ[𝕜] E)) :=
     linear_map.continuous_on_pi _,
-  have : continuous ((f.comp ((equiv_fun_basis b_basis).symm : (b → 𝕜) →ₗ[𝕜] E))
-                      ∘ (equiv_fun_basis b_basis)) := B.comp A,
+  have : continuous ((f.comp (b_basis.equiv_fun.symm : (b → 𝕜) →ₗ[𝕜] E))
+                      ∘ b_basis.equiv_fun) := B.comp A,
   convert this,
   ext x,
   dsimp,
@@ -183,10 +183,10 @@ lemma finite_dimensional.complete [finite_dimensional 𝕜 E] : complete_space E
 begin
   rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
   letI : fintype b := finite.fintype b_finite,
-  have : uniform_embedding (equiv_fun_basis b_basis).symm :=
+  have : uniform_embedding b_basis.equiv_fun.symm :=
     linear_equiv.uniform_embedding _ (linear_map.continuous_of_finite_dimensional _)
     (linear_map.continuous_of_finite_dimensional _),
-  change uniform_embedding (equiv_fun_basis b_basis).symm.to_equiv at this,
+  change uniform_embedding b_basis.equiv_fun.symm.to_equiv at this,
   exact (complete_space_congr this).1 (by apply_instance)
 end
 
@@ -221,7 +221,7 @@ lemma finite_dimensional.proper [finite_dimensional 𝕜 E] : proper_space E :=
 begin
   rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
   letI : fintype b := finite.fintype b_finite,
-  let e := equiv_fun_basis b_basis,
+  let e := b_basis.equiv_fun,
   let f : E →L[𝕜] (b → 𝕜) :=
     { cont := linear_map.continuous_of_finite_dimensional _, ..e.to_linear_map },
   refine metric.proper_image_of_proper e.symm

src/linear_algebra/basic.lean

@@ -1738,6 +1738,9 @@ rfl
 @[simp] theorem map_zero : e 0 = 0 := e.to_linear_map.map_zero
 @[simp] theorem map_smul (c : R) (x : M) : e (c • x) = c • e x := e.map_smul' c x
 
+@[simp] lemma map_sum {s : finset ι} (u : ι → M) : e (∑ i in s, u i) = ∑ i in s, e (u i) :=
+e.to_linear_map.map_sum
+
 @[simp] theorem map_eq_zero_iff {x : M} : e x = 0 ↔ x = 0 :=
 e.to_add_equiv.map_eq_zero_iff
 theorem map_ne_zero_iff {x : M} : e x ≠ 0 ↔ x ≠ 0 :=

src/linear_algebra/basis.lean

@@ -777,6 +777,10 @@ end
 lemma is_basis.repr_eq_single {i} : hv.repr (v i) = finsupp.single i 1 :=
 by apply hv.1.repr_eq_single; simp
 
+@[simp]
+lemma is_basis.repr_self_apply (i j : ι) : hv.repr (v i) j = if i = j then 1 else 0 :=
+by rw [hv.repr_eq_single, finsupp.single_apply]
+
 /-- Construct a linear map given the value at the basis. -/
 def is_basis.constr (f : ι → M') : M →ₗ[R] M' :=
 (finsupp.total M' M' R id).comp $ (finsupp.lmap_domain R R f).comp hv.repr
@@ -976,7 +980,7 @@ variables [fintype ι] (h : is_basis R v)
 
 /-- A module over `R` with a finite basis is linearly equivalent to functions from its basis to `R`.
 -/
-def equiv_fun_basis  : M ≃ₗ[R] (ι → R) :=
+def is_basis.equiv_fun : M ≃ₗ[R] (ι → R) :=
 linear_equiv.trans (module_equiv_finsupp h)
   { to_fun := finsupp.to_fun,
     map_add' := λ x y, by ext; exact finsupp.add_apply,
@@ -985,17 +989,17 @@ linear_equiv.trans (module_equiv_finsupp h)
 
 /-- A module over a finite ring that admits a finite basis is finite. -/
 def module.fintype_of_fintype [fintype R] : fintype M :=
-fintype.of_equiv _ (equiv_fun_basis h).to_equiv.symm
+fintype.of_equiv _ h.equiv_fun.to_equiv.symm
 
 theorem module.card_fintype [fintype R] [fintype M] :
   card M = (card R) ^ (card ι) :=
-calc card M = card (ι → R)    : card_congr (equiv_fun_basis h).to_equiv
+calc card M = card (ι → R)    : card_congr h.equiv_fun.to_equiv
         ... = card R ^ card ι : card_fun
 
 /-- Given a basis `v` indexed by `ι`, the canonical linear equivalence between `ι → R` and `M` maps
 a function `x : ι → R` to the linear combination `∑_i x i • v i`. -/
-@[simp] lemma equiv_fun_basis_symm_apply (x : ι → R) :
-  (equiv_fun_basis h).symm x = ∑ i, x i • v i :=
+@[simp] lemma is_basis.equiv_fun_symm_apply (x : ι → R) :
+  h.equiv_fun.symm x = ∑ i, x i • v i :=
 begin
   change finsupp.sum
       ((finsupp.equiv_fun_on_fintype.symm : (ι → R) ≃ (ι →₀ R)) x) (λ (i : ι) (a : R), a • v i)
@@ -1008,6 +1012,18 @@ begin
   { simp [H], refl }
 end
 
+lemma is_basis.equiv_fun_apply (u : M) : h.equiv_fun u = h.repr u := rfl
+
+lemma is_basis.equiv_fun_total (u : M) : ∑ i, h.equiv_fun u i • v i = u:=
+begin
+  conv_rhs { rw ← h.total_repr u },
+  simp [finsupp.total_apply, finsupp.sum_fintype, h.equiv_fun_apply]
+end
+
+@[simp]
+lemma is_basis.equiv_fun_self (i j : ι) : h.equiv_fun (v i) j = if i = j then 1 else 0 :=
+by { rw [h.equiv_fun_apply, h.repr_self_apply] }
+
 end module
 
 section vector_space

src/linear_algebra/matrix.lean

@@ -1,10 +1,11 @@
 /-
 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Johannes Hölzl, Casper Putz
+Author: Johannes Hölzl, Patrick Massot, Casper Putz
 -/
 import linear_algebra.finite_dimensional
 import linear_algebra.nonsingular_inverse
+import linear_algebra.multilinear
 
 /-!
 # Linear maps and matrices
@@ -15,16 +16,37 @@ to matrices. This defines a linear equivalence between linear maps
 between finite-dimensional vector spaces and matrices indexed by
 the respective bases.
 
+It also defines the trace of an endomorphism, and the determinant of a family of vectors with
+respect to some basis.
+
 Some results are proved about the linear map corresponding to a
 diagonal matrix (`range`, `ker` and `rank`).
 
 ## Main definitions
 
-`to_lin`, `to_matrix`, `linear_equiv_matrix`
+In the list below, and in all this file, `R` is a commutative ring (semiring
+is sometimes enough), `M` and its variations are `R`-modules, `ι`, `κ`, `n` and `m` are finite
+types used for indexing.
+
+* `to_lin`: the `R`-linear map from `matrix m n R` to `R`-linear maps from `n → R` to `m → R`
+* `to_matrix`: the map in the other direction
+* `linear_equiv_matrix`: given bases `v₁ : ι → M₁` and `v₂ : κ → M₂`, the `R`-linear equivalence
+  from `M₁ →ₗ[R] M₂` to `matrix κ ι R`
+* `linear_equiv_matrix'`: the same thing but with `M₁ = n → R` and `M₂ = m → R`, using their
+  standard bases
+* `alg_equiv_matrix`: given a basis indexed by `n`, the `R`-algebra equivalence between
+  `R`-endomorphisms of `M` and `matrix n n R`
+* `matrix.trace`: the trace of a square matrix
+* `linear_map.trace`: the trace of an endomorphism
+* `is_basis.to_matrix`: the matrix whose columns are a given family of vectors in a given basis
+* `is_basis.to_matrix_equiv`: given a basis, the linear equivalence between families of vectors
+  and matrices arising from `is_basis.to_matrix`
+* `is_basis.det`: the determinant of a family of vectors with respect to a basis, as a multilinear
+  map
 
 ## Tags
 
-linear_map, matrix, linear_equiv, diagonal
+linear_map, matrix, linear_equiv, diagonal, det, trace
 
 -/
 
@@ -202,16 +224,16 @@ variables {ι κ M₁ M₂ : Type*}
 equivalence between linear maps `M₁ →ₗ M₂` and matrices over `R` indexed by the bases. -/
 def linear_equiv_matrix (hv₁ : is_basis R v₁) (hv₂ : is_basis R v₂) :
   (M₁ →ₗ[R] M₂) ≃ₗ[R] matrix κ ι R :=
-linear_equiv.trans (linear_equiv.arrow_congr (equiv_fun_basis hv₁) (equiv_fun_basis hv₂)) linear_equiv_matrix'
+linear_equiv.trans (linear_equiv.arrow_congr hv₁.equiv_fun hv₂.equiv_fun) linear_equiv_matrix'
 
 variables (hv₁ : is_basis R v₁) (hv₂ : is_basis R v₂)
 
 lemma linear_equiv_matrix_apply (f : M₁ →ₗ[R] M₂) (i : κ) (j : ι) :
-  linear_equiv_matrix hv₁ hv₂ f i j = equiv_fun_basis hv₂ (f (v₁ j)) i :=
+  linear_equiv_matrix hv₁ hv₂ f i j = hv₂.equiv_fun (f (v₁ j)) i :=
 by simp only [linear_equiv_matrix, to_matrix, to_matrixₗ, ite_smul,
   linear_equiv.trans_apply, linear_equiv.arrow_congr_apply,
   linear_equiv.coe_coe, linear_equiv_matrix'_apply, finset.mem_univ, if_true,
-  one_smul, zero_smul, finset.sum_ite_eq, equiv_fun_basis_symm_apply]
+  one_smul, zero_smul, finset.sum_ite_eq, hv₁.equiv_fun_symm_apply]
 
 lemma linear_equiv_matrix_apply' (f : M₁ →ₗ[R] M₂) (i : κ) (j : ι) :
   linear_equiv_matrix hv₁ hv₂ f i j = hv₂.repr (f (v₁ j)) i :=
@@ -221,7 +243,7 @@ linear_equiv_matrix_apply hv₁ hv₂ f i j
 lemma linear_equiv_matrix_id : linear_equiv_matrix hv₁ hv₁ id = 1 :=
 begin
   ext i j,
-  simp [linear_equiv_matrix_apply, equiv_fun_basis, matrix.one_apply, finsupp.single, eq_comm]
+  simp [linear_equiv_matrix_apply, is_basis.equiv_fun, matrix.one_apply, finsupp.single, eq_comm]
 end
 
 @[simp] lemma linear_equiv_matrix_symm_one : (linear_equiv_matrix hv₁ hv₁).symm 1 = id :=
@@ -242,7 +264,7 @@ begin
     ← equiv.of_injective_apply _ hv₁.injective, ← equiv.of_injective_apply _ hv₂.injective,
     to_matrix_of_equiv, ← linear_equiv.trans_apply, linear_equiv.arrow_congr_trans], congr' 3;
   refine function.left_inverse.injective linear_equiv.symm_symm _; ext x;
-  simp_rw [linear_equiv.symm_trans_apply, equiv_fun_basis_symm_apply, fun_congr_left_symm,
+  simp_rw [linear_equiv.symm_trans_apply, is_basis.equiv_fun_symm_apply, fun_congr_left_symm,
     fun_congr_left_apply, fun_left_apply],
   convert (finset.sum_equiv (equiv.of_injective _ hv₁.injective) _).symm,
   simp_rw [equiv.symm_apply_apply, equiv.of_injective_apply, subtype.coe_mk],
@@ -275,7 +297,7 @@ lemma linear_equiv_matrix_comp [decidable_eq ι] (f : M₂ →ₗ[R] M₃) (g :
   linear_equiv_matrix hv₁ hv₃ (f.comp g) =
   linear_equiv_matrix hv₂ hv₃ f ⬝ linear_equiv_matrix hv₁ hv₂ g :=
 by simp_rw [linear_equiv_matrix, linear_equiv.trans_apply, linear_equiv_matrix'_apply,
-    linear_equiv.arrow_congr_comp _ (equiv_fun_basis hv₂), comp_to_matrix_mul]
+    linear_equiv.arrow_congr_comp _ hv₂.equiv_fun, comp_to_matrix_mul]
 
 lemma linear_equiv_matrix_mul [decidable_eq ι] (f g : M₁ →ₗ[R] M₁) :
   linear_equiv_matrix hv₁ hv₁ (f * g) = linear_equiv_matrix hv₁ hv₁ f * linear_equiv_matrix hv₁ hv₁ g :=
@@ -294,8 +316,81 @@ end
 
 end comp
 
-section det
+end matrix
+
+section is_basis_to_matrix
+
+variables {ι ι' R M : Type*} [fintype ι] [decidable_eq ι]
+          [comm_ring R] [add_comm_group M] [module R M]
+
+open function matrix
+
+/-- From a basis `e : ι → M` and a family of vectors `v : ι → M`, make the matrix whose columns
+are the vectors `v i` written in the basis `e`. -/
+def is_basis.to_matrix {e : ι → M} (he : is_basis R e) (v : ι → M) : matrix ι ι R :=
+linear_equiv_matrix he he (he.constr v)
+
+variables {e : ι → M} (he : is_basis R e) (v : ι → M) (i j : ι)
+
+namespace is_basis
+
+lemma to_matrix_apply : he.to_matrix v i j = he.equiv_fun (v j) i :=
+by simp [is_basis.to_matrix, linear_equiv_matrix_apply]
+
+@[simp] lemma to_matrix_self : he.to_matrix e = 1 :=
+begin
+  rw is_basis.to_matrix,
+  ext i j,
+  simp [linear_equiv_matrix_apply, is_basis.equiv_fun, matrix.one_apply, finsupp.single, eq_comm]
+end
+
+lemma to_matrix_update (x : M) :
+  he.to_matrix (function.update v i x) = matrix.update_column (he.to_matrix v) i (he.repr x) :=
+begin
+  ext j k,
+  rw [is_basis.to_matrix, linear_equiv_matrix_apply' he he (he.constr (update v i x)),
+      matrix.update_column_apply, constr_basis, he.to_matrix_apply],
+  split_ifs,
+  { rw [h, update_same i x v] },
+  { rw [update_noteq h, he.equiv_fun_apply] },
+end
+
+/-- From a basis `e : ι → M`, build a linear equivalence between families of vectors `v : ι → M`,
+and matrices, making the matrix whose columns are the vectors `v i` written in the basis `e`. -/
+def to_matrix_equiv {e : ι → M} (he : is_basis R e) : (ι → M) ≃ₗ[R] matrix ι ι R :=
+{ to_fun := he.to_matrix,
+  map_add' := λ v w, begin
+    ext i j,
+    change _ = _ + _,
+    simp [he.to_matrix_apply]
+  end,
+  map_smul' := begin
+    intros c v,
+    ext i j,
+    simp [he.to_matrix_apply]
+  end,
+  inv_fun := λ m j, ∑ i, (m i j) • e i,
+  left_inv := begin
+    intro v,
+    ext j,
+    simp [he.to_matrix_apply, he.equiv_fun_total (v j)]
+  end,
+  right_inv := begin
+    intros x,
+    ext k l,
+    simp [he.to_matrix_apply, he.equiv_fun.map_sum, he.equiv_fun.map_smul,
+          fintype.sum_apply k (λ i, x i l • he.equiv_fun (e i)),
+          he.equiv_fun_self]
+  end }
+
+end is_basis
 
+end is_basis_to_matrix
+
+open_locale matrix
+
+section det
+open matrix
 variables {R ι M M' : Type*} [comm_ring R]
   [add_comm_group M] [module R M]
   [add_comm_group M'] [module R M']
@@ -335,8 +430,43 @@ def linear_equiv.of_is_unit_det {f : M →ₗ[R] M'} {hv : is_basis R v} {hv' :
     simp [h]
   end }
 
+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 :=
+{ to_fun := λ v, det (he.to_matrix v),
+  map_add' := begin
+    intros v i x y,
+    simp only [he.to_matrix_update, linear_map.map_add],
+    apply det_update_column_add
+  end,
+  map_smul' := begin
+    intros u i c x,
+    simp only [he.to_matrix_update, algebra.id.smul_eq_mul, map_smul_eq_smul_map],
+    apply det_update_column_smul
+  end }
+
+lemma is_basis.det_apply (v : ι → M) : he.det v = det (he.to_matrix v) := rfl
+
+lemma is_basis.det_self : he.det e = 1 :=
+by simp [he.det_apply]
+
+lemma is_basis.iff_det {v : ι → M} : is_basis R v ↔ is_unit (he.det v) :=
+begin
+  split,
+  { intro hv,
+    change is_unit (linear_equiv_matrix he he (equiv_of_is_basis he hv $ equiv.refl ι)).det,
+    apply linear_equiv.is_unit_det },
+  { intro h,
+    convert linear_equiv.is_basis he (linear_equiv.of_is_unit_det h),
+    ext i,
+    exact (constr_basis he).symm },
+end
+
 end det
 
+namespace matrix
+
 section trace
 
 variables (n) (R : Type v) (M : Type w) [semiring R] [add_comm_monoid M] [semimodule R M]
@@ -685,4 +815,4 @@ square matrices. -/
 def alg_equiv_matrix {R : Type v} {M : Type w}
   [comm_ring R] [add_comm_group M] [module R M] [decidable_eq n] {b : n → M} (h : is_basis R b) :
   module.End R M ≃ₐ[R] matrix n n R :=
-(equiv_fun_basis h).alg_conj.trans alg_equiv_matrix'
+h.equiv_fun.alg_conj.trans alg_equiv_matrix'