feat(linear_algebra/matrix): M maps some v ≠ 0 to zero iff `det M…

… = 0` (#9041)

A result I have wanted for a long time: the two notions of a "singular" matrix are equivalent over an integral domain. Namely, a matrix `M` is singular iff it maps some nonzero vector to zero, which happens iff its determinant is zero.

Here, I find such a `v` by going through the field of fractions, where everything is a lot easier because all injective endomorphisms are automorphisms. Maybe a bit overkill (and unsatisfying constructively), but it works and is a lot nicer to write out than explicitly finding an element of the kernel.

src/data/matrix/basic.lean

@@ -350,6 +350,14 @@ by convert finset.sum_eq_single i (λ j _, this j) _ using 1; simp
 have ∀ j ≠ i, v j * diagonal w j i = 0 := λ j hij, by simp [diagonal_apply_ne hij],
 by convert finset.sum_eq_single i (λ j _, this j) _ using 1; simp
 
+@[simp] lemma single_dot_product (x : α) (i : m) : dot_product (pi.single i x) v = x * v i :=
+have ∀ j ≠ i, pi.single i x j * v j = 0 := λ j hij, by simp [pi.single_eq_of_ne hij],
+by convert finset.sum_eq_single i (λ j _, this j) _ using 1; simp
+
+@[simp] lemma dot_product_single (x : α) (i : m) : dot_product v (pi.single i x) = v i * x :=
+have ∀ j ≠ i, v j * pi.single i x j = 0 := λ j hij, by simp [pi.single_eq_of_ne hij],
+by convert finset.sum_eq_single i (λ j _, this j) _ using 1; simp
+
 end non_unital_non_assoc_semiring_decidable
 
 section ring
@@ -960,6 +968,13 @@ lemma vec_mul_diagonal [fintype m] [decidable_eq m] (v w : m → α) (x : m) :
   vec_mul v (diagonal w) x = v x * w x :=
 dot_product_diagonal' v w x
 
+/-- Associate the dot product of `mul_vec` to the left. -/
+lemma dot_product_mul_vec [fintype n] [fintype m] [non_unital_semiring R]
+  (v : m → R) (A : matrix m n R) (w : n → R) :
+  dot_product v (mul_vec A w) = dot_product (vec_mul v A) w :=
+by simp only [dot_product, vec_mul, mul_vec, finset.mul_sum, finset.sum_mul, mul_assoc];
+   exact finset.sum_comm
+
 @[simp] lemma mul_vec_zero [fintype n] (A : matrix m n α) : mul_vec A 0 = 0 :=
 by { ext, simp [mul_vec] }
 
@@ -997,6 +1012,16 @@ lemma add_vec_mul [fintype m] (A : matrix m n α) (x y : m → α) :
   vec_mul (x + y) A = vec_mul x A + vec_mul y A :=
 by { ext, apply add_dot_product }
 
+lemma vec_mul_smul [fintype n] [comm_semiring R] [semiring S] [algebra R S]
+  (M : matrix n m S) (b : R) (v : n → S)  :
+  M.vec_mul (b • v) = b • M.vec_mul v :=
+by { ext i, simp only [vec_mul, dot_product, finset.smul_sum, pi.smul_apply, smul_mul_assoc] }
+
+lemma mul_vec_smul [fintype n] [comm_semiring R] [semiring S] [algebra R S]
+  (M : matrix m n S) (b : R) (v : n → S)  :
+  M.mul_vec (b • v) = b • M.mul_vec v :=
+by { ext i, simp only [mul_vec, dot_product, finset.smul_sum, pi.smul_apply, mul_smul_comm] }
+
 end non_unital_non_assoc_semiring
 
 section non_unital_semiring
@@ -1625,4 +1650,18 @@ lemma map_matrix_mul (M : matrix m n α) (N : matrix n o α) (i : m) (j : o) (f
   f (matrix.mul M N i j) = matrix.mul (λ i j, f (M i j)) (λ i j, f (N i j)) i j :=
 by simp [matrix.mul_apply, ring_hom.map_sum]
 
+lemma map_dot_product [semiring R] [semiring S] (f : R →+* S) (v w : n → R) :
+  f (matrix.dot_product v w) = matrix.dot_product (f ∘ v) (f ∘ w) :=
+by simp only [matrix.dot_product, f.map_sum, f.map_mul]
+
+lemma map_vec_mul [semiring R] [semiring S]
+  (f : R →+* S) (M : matrix n m R) (v : n → R) (i : m) :
+  f (M.vec_mul v i) = ((M.map f).vec_mul (f ∘ v) i) :=
+by simp only [matrix.vec_mul, matrix.map_apply, ring_hom.map_dot_product]
+
+lemma map_mul_vec [semiring R] [semiring S]
+  (f : R →+* S) (M : matrix m n R) (v : n → R) (i : m) :
+  f (M.mul_vec v i) = ((M.map f).mul_vec (f ∘ v) i) :=
+by simp only [matrix.mul_vec, matrix.map_apply, ring_hom.map_dot_product]
+
 end ring_hom

src/linear_algebra/bilinear_form.lean

@@ -1583,11 +1583,15 @@ open matrix
 variables {A : Type*} [integral_domain A] [module A M₃] (B₃ : bilin_form A M₃)
 variables {ι : Type*} [decidable_eq ι] [fintype ι]
 
-theorem nondegenerate_of_det_ne_zero' (M : matrix ι ι A) (h : M.det ≠ 0) :
+theorem _root_.matrix.nondegenerate.to_bilin' {M : matrix ι ι R₃} (h : M.nondegenerate) :
   (to_bilin' M).nondegenerate :=
-λ x hx, matrix.nondegenerate_of_det_ne_zero h x (λ y,
+λ x hx, h.eq_zero_of_ortho (λ y,
   by simpa only [to_bilin'_apply, dot_product, mul_vec, finset.mul_sum, mul_assoc] using hx y)
 
+theorem nondegenerate_of_det_ne_zero' (M : matrix ι ι A) (h : M.det ≠ 0) :
+  (to_bilin' M).nondegenerate :=
+(matrix.nondegenerate_of_det_ne_zero h).to_bilin'
+
 theorem nondegenerate_of_det_ne_zero (b : basis ι A M₃) (h : (to_matrix b B₃).det ≠ 0) :
   B₃.nondegenerate :=
 begin

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -470,6 +470,12 @@ lemma is_unit_det_of_left_inverse (h : B ⬝ A = 1) : is_unit A.det :=
 lemma is_unit_det_of_right_inverse (h : A ⬝ B = 1) : is_unit A.det :=
 @is_unit_of_invertible _ _ _ (det_invertible_of_right_inverse _ _ h)
 
+lemma det_ne_zero_of_left_inverse [nontrivial α] (h : B ⬝ A = 1) : A.det ≠ 0 :=
+is_unit.ne_zero (matrix.is_unit_det_of_left_inverse h)
+
+lemma det_ne_zero_of_right_inverse [nontrivial α] (h : A ⬝ B = 1) : A.det ≠ 0 :=
+is_unit.ne_zero (matrix.is_unit_det_of_right_inverse h)
+
 lemma nonsing_inv_left_right (h : A ⬝ B = 1) : B ⬝ A = 1 :=
 begin
   have h' : is_unit B.det := is_unit_det_of_left_inverse h,
@@ -670,14 +676,32 @@ divides `b`. -/
   A.mul_vec (cramer A b) = A.det • b :=
 by rw [cramer_eq_adjugate_mul_vec, mul_vec_mul_vec, mul_adjugate, smul_mul_vec_assoc, one_mul_vec]
 
+section nondegenerate
+
+variables {m R A : Type*} [fintype m] [comm_ring R] [integral_domain A]
+
+/-- A matrix `M` is nondegenerate if for all `v ≠ 0`, there is a `w ≠ 0` with `w ⬝ M ⬝ v ≠ 0`. -/
+def nondegenerate (M : matrix m m R) :=
+∀ v, (∀ w, matrix.dot_product v (mul_vec M w) = 0) → v = 0
+
+/-- If `M` is nondegenerate and `w ⬝ M ⬝ v = 0` for all `w`, then `v = 0`. -/
+lemma nondegenerate.eq_zero_of_ortho {M : matrix m m R} (hM : nondegenerate M)
+  {v : m → R} (hv : ∀ w, matrix.dot_product v (mul_vec M w) = 0) : v = 0 :=
+hM v hv
+
+/-- If `M` is nondegenerate and `v ≠ 0`, then there is some `w` such that `w ⬝ M ⬝ v ≠ 0`. -/
+lemma nondegenerate.exists_not_ortho_of_ne_zero {M : matrix m m R} (hM : nondegenerate M)
+  {v : m → R} (hv : v ≠ 0) : ∃ w, matrix.dot_product v (mul_vec M w) ≠ 0 :=
+not_forall.mp (mt hM.eq_zero_of_ortho hv)
+
 /-- If `M` has a nonzero determinant, then `M` as a bilinear form on `n → A` is nondegenerate.
 
 See also `bilin_form.nondegenerate_of_det_ne_zero'` and `bilin_form.nondegenerate_of_det_ne_zero`.
 -/
-theorem nondegenerate_of_det_ne_zero {A : Type*} [integral_domain A]
-  {M : matrix n n A} (hM : M.det ≠ 0)
-  (v : n → A) (hv : ∀ w, matrix.dot_product v (mul_vec M w) = 0) : v = 0 :=
+theorem nondegenerate_of_det_ne_zero {M : matrix n n A} (hM : M.det ≠ 0) :
+  nondegenerate M :=
 begin
+  intros v hv,
   ext i,
   specialize hv (M.cramer (pi.single i 1)),
   refine (mul_eq_zero.mp _).resolve_right hM,
@@ -688,4 +712,16 @@ begin
   { intros, have := finset.mem_univ i, contradiction }
 end
 
+theorem eq_zero_of_vec_mul_eq_zero {M : matrix n n A} (hM : M.det ≠ 0) {v : n → A}
+  (hv : M.vec_mul v = 0) : v = 0 :=
+(nondegenerate_of_det_ne_zero hM).eq_zero_of_ortho
+  (λ w, by rw [dot_product_mul_vec, hv, zero_dot_product])
+
+theorem eq_zero_of_mul_vec_eq_zero {M : matrix n n A} (hM : M.det ≠ 0) {v : n → A}
+  (hv : M.mul_vec v = 0) :
+  v = 0 :=
+eq_zero_of_vec_mul_eq_zero (by rwa det_transpose) ((vec_mul_transpose M v).trans hv)
+
+end nondegenerate
+
 end matrix

src/linear_algebra/matrix/to_lin.lean

@@ -152,6 +152,10 @@ lemma linear_map.to_matrix'_mul [fintype m] [decidable_eq m]
   (f * g).to_matrix' = f.to_matrix' ⬝ g.to_matrix' :=
 linear_map.to_matrix'_comp f g
 
+lemma matrix.ker_to_lin'_eq_bot_iff {M : matrix n n R} :
+  M.to_lin'.ker = ⊥ ↔ ∀ v, M.mul_vec v = 0 → v = 0 :=
+by simp only [submodule.eq_bot_iff, linear_map.mem_ker, matrix.to_lin'_apply]
+
 /-- If `M` and `M'` are each other's inverse matrices, they provide an equivalence between `m → A`
 and `n → A` corresponding to `M.mul_vec` and `M'.mul_vec`. -/
 @[simps]

src/linear_algebra/matrix/to_linear_equiv.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
 import linear_algebra.matrix.nonsingular_inverse
 import linear_algebra.matrix.to_lin
+import ring_theory.localization
 
 /-!
 # Matrices and linear equivalences
@@ -16,6 +17,10 @@ to linear equivs.
 
  * `matrix.to_linear_equiv`: a matrix with an invertible determinant forms a linear equiv
 
+## Main results
+
+ * `matrix.exists_mul_vec_eq_zero_iff`: `M` maps some `v ≠ 0` to zero iff `det M = 0`
+
 ## Tags
 
 matrix, linear_equiv, determinant, inverse
@@ -92,4 +97,89 @@ range_eq_top.mpr (to_linear_equiv b A hA).surjective
 
 end to_linear_equiv
 
+section nondegenerate
+
+open_locale matrix
+
+/-- This holds for all integral domains (see `matrix.exists_mul_vec_eq_zero_iff`),
+not just fields, but it's easier to prove it for the field of fractions first. -/
+lemma exists_mul_vec_eq_zero_iff_aux {K : Type*} [decidable_eq n] [field K] {M : matrix n n K} :
+  (∃ (v ≠ 0), M.mul_vec v = 0) ↔ M.det = 0 :=
+begin
+  split,
+  { rintros ⟨v, hv, mul_eq⟩,
+    contrapose! hv,
+    exact eq_zero_of_mul_vec_eq_zero hv mul_eq },
+  { contrapose!,
+    intros h,
+    have : M.to_lin'.ker = ⊥,
+    { simpa only [ker_to_lin'_eq_bot_iff, not_imp_not] using h },
+    have : M ⬝ linear_map.to_matrix'
+      ((linear_equiv.of_injective_endo M.to_lin' this).symm : (n → K) →ₗ[K] (n → K)) = 1,
+    { refine matrix.to_lin'.injective (linear_map.ext $ λ v, _),
+      rw [matrix.to_lin'_mul, matrix.to_lin'_one, matrix.to_lin'_to_matrix', linear_map.comp_apply],
+      exact (linear_equiv.of_injective_endo M.to_lin' this).apply_symm_apply v },
+    exact matrix.det_ne_zero_of_right_inverse this }
+end
+
+lemma exists_mul_vec_eq_zero_iff {A : Type*} [decidable_eq n] [integral_domain A]
+  {M : matrix n n A} :
+  (∃ (v ≠ 0), M.mul_vec v = 0) ↔ M.det = 0 :=
+begin
+  have : (∃ (v ≠ 0), mul_vec ((algebra_map A (fraction_ring A)).map_matrix M) v = 0) ↔ _ :=
+    exists_mul_vec_eq_zero_iff_aux,
+  rw [← ring_hom.map_det, is_fraction_ring.to_map_eq_zero_iff] at this,
+  refine iff.trans _ this, split; rintro ⟨v, hv, mul_eq⟩,
+  { refine ⟨λ i, algebra_map _ _ (v i), mt (λ h, funext $ λ i, _) hv, _⟩,
+    { exact is_fraction_ring.injective A (fraction_ring A) (congr_fun h i) },
+    { ext i,
+      refine (ring_hom.map_mul_vec _ _ _ i).symm.trans _,
+      rw [mul_eq, pi.zero_apply, ring_hom.map_zero, pi.zero_apply] } },
+  { letI := classical.dec_eq (fraction_ring A),
+    obtain ⟨⟨b, hb⟩, ba_eq⟩ := is_localization.exist_integer_multiples_of_finset
+      (non_zero_divisors A) (finset.univ.image v),
+    choose f hf using ba_eq,
+    refine ⟨λ i, f _ (finset.mem_image.mpr ⟨i, finset.mem_univ i, rfl⟩),
+            mt (λ h, funext $ λ i, _) hv, _⟩,
+    { have := congr_arg (algebra_map A (fraction_ring A)) (congr_fun h i),
+      rw [hf, subtype.coe_mk, pi.zero_apply, ring_hom.map_zero, algebra.smul_def,
+          mul_eq_zero, is_fraction_ring.to_map_eq_zero_iff] at this,
+      exact this.resolve_left (mem_non_zero_divisors_iff_ne_zero.mp hb), },
+    { ext i,
+      refine is_fraction_ring.injective A (fraction_ring A) _,
+      calc algebra_map A (fraction_ring A) (M.mul_vec (λ (i : n), f (v i) _) i)
+          = ((algebra_map A (fraction_ring A)).map_matrix M).mul_vec
+              (algebra_map _ (fraction_ring A) b • v) i : _
+      ... = 0 : _,
+      { simp_rw [ring_hom.map_mul_vec, mul_vec, dot_product, function.comp_app, hf,
+          subtype.coe_mk, ring_hom.map_matrix_apply, pi.smul_apply, smul_eq_mul,
+          algebra.smul_def] },
+      { rw [mul_vec_smul, mul_eq, pi.smul_apply, pi.zero_apply, smul_zero] } } },
+end
+
+lemma exists_vec_mul_eq_zero_iff {A : Type*} [decidable_eq n] [integral_domain A]
+  {M : matrix n n A} :
+  (∃ (v ≠ 0), M.vec_mul v = 0) ↔ M.det = 0 :=
+by simpa only [← M.det_transpose, ← mul_vec_transpose] using exists_mul_vec_eq_zero_iff
+
+theorem nondegenerate_iff_det_ne_zero {A : Type*} [decidable_eq n] [integral_domain A]
+  {M : matrix n n A} :
+  nondegenerate M ↔ M.det ≠ 0 :=
+begin
+  refine iff.trans _ (not_iff_not.mpr exists_vec_mul_eq_zero_iff),
+  simp only [not_exists],
+  split,
+  { intros hM v hv hMv,
+    obtain ⟨w, hwMv⟩ := hM.exists_not_ortho_of_ne_zero hv,
+    simpa only [dot_product_mul_vec, hMv, zero_dot_product] using hwMv },
+  { intros h v hv,
+    refine not_imp_not.mp (h v) (funext $ λ i, _),
+    simpa only [dot_product_mul_vec, dot_product_single, mul_one] using hv (pi.single i 1) }
+end
+
+alias nondegenerate_iff_det_ne_zero ↔
+  matrix.nondegenerate.det_ne_zero matrix.nondegenerate.of_det_ne_zero
+
+end nondegenerate
+
 end matrix