feat(linear_algebra/bilinear_form): equivalence with matrices, given …

…a basis (#5095)

This PR defines the equivalence between bilinear forms on an arbitrary module and matrices, given a basis of that module. It updates the existing equivalence between bilinear forms on `n → R` so that the overall structure of the file matches that of `linear_algebra.matrix`, i.e. there are two pairs of equivs, one for `n → R` and one for any `M` with a basis.

Changes:
 - `bilin_form_equiv_matrix`, `bilin_form.to_matrix` and `matrix.to_bilin_form` have been consolidated as linear equivs `bilin_form.to_matrix'` and `matrix.to_bilin'`. Other declarations have been renamed accordingly.
 - `quadratic_form.to_matrix` and `matrix.to_quadratic_form` are renamed by analogy to `quadratic_form.to_matrix'` and `matrix.to_quadratic_form'`
 - replaced some `classical.decidable_eq` in lemma statements with instance parameters, because otherwise we have to use `congr` to apply these lemmas when a `decidable_eq` instance is available

Additions:
 - `bilin_form.to_matrix` and `matrix.to_bilin`: given a basis, the equivalences between bilinear forms on any module and matrices
 - lemmas from `to_matrix'` and `to_bilin'` have been ported to `to_matrix` and `to_bilin`
 - `bilin_form.congr`, a dependency of `bilin_form.to_matrix`, states that `bilin_form R M` and `bilin_form R M'` are linearly equivalent if `M` and `M'` are
 - assorted lemmas involving `std_basis`

Deletions:
 - `bilin_form.to_matrix_smul`: use `linear_equiv.map_smul` instead



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/linear_algebra/basis.lean

@@ -515,7 +515,7 @@ section module
 variables {η : Type*} {ιs : η → Type*} {Ms : η → Type*}
 variables [ring R] [∀i, add_comm_group (Ms i)] [∀i, module R (Ms i)]
 
-lemma linear_independent_std_basis
+lemma linear_independent_std_basis [decidable_eq η]
   (v : Πj, ιs j → (Ms j)) (hs : ∀i, linear_independent R (v i)) :
   linear_independent R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (v ji.1 ji.2)) :=
 begin
@@ -546,7 +546,7 @@ end
 
 variable [fintype η]
 
-lemma is_basis_std_basis (s : Πj, ιs j → (Ms j)) (hs : ∀j, is_basis R (s j)) :
+lemma is_basis_std_basis [decidable_eq η] (s : Πj, ιs j → (Ms j)) (hs : ∀j, is_basis R (s j)) :
   is_basis R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (s ji.1 ji.2)) :=
 begin
   split,
@@ -569,20 +569,36 @@ end
 section
 variables (R η)
 
-lemma is_basis_fun₀ : is_basis R
+lemma is_basis_fun₀ [decidable_eq η] : is_basis R
     (λ (ji : Σ (j : η), unit),
        (std_basis R (λ (i : η), R) (ji.fst)) 1) :=
-@is_basis_std_basis R η (λi:η, unit) (λi:η, R) _ _ _ _ (λ _ _, (1 : R))
+@is_basis_std_basis R η (λi:η, unit) (λi:η, R) _ _ _ _ _ (λ _ _, (1 : R))
   (assume i, @is_basis_singleton_one _ _ _ _)
 
-lemma is_basis_fun : is_basis R (λ i, std_basis R (λi:η, R) i 1) :=
+lemma is_basis_fun [decidable_eq η] : is_basis R (λ i, std_basis R (λi:η, R) i 1) :=
 begin
   apply (is_basis_fun₀ R η).comp (λ i, ⟨i, punit.star⟩),
   apply bijective_iff_has_inverse.2,
   use sigma.fst,
   simp [function.left_inverse, function.right_inverse]
 end
 
+@[simp] lemma is_basis_fun_repr [decidable_eq η] (x : η → R) (i : η) :
+  (pi.is_basis_fun R η).repr x i = x i :=
+begin
+  conv_rhs { rw ← (pi.is_basis_fun R η).total_repr x },
+  rw [finsupp.total_apply, finsupp.sum_fintype],
+  show (pi.is_basis_fun R η).repr x i =
+    (∑ j, λ i, (pi.is_basis_fun R η).repr x j • std_basis R (λ _, R) j 1 i) i,
+  rw [finset.sum_apply, finset.sum_eq_single i],
+  { simp only [pi.smul_apply, smul_eq_mul, std_basis_same, mul_one] },
+  { rintros b - hb, simp only [std_basis_ne _ _ _ _ hb.symm, smul_zero] },
+  { intro,
+    have := finset.mem_univ i,
+    contradiction },
+  { intros, apply zero_smul },
+end
+
 end
 
 end module