feat(LinearAlgebra/Finsupp/linearCombination): add bilinearCombination (

#22678)

Add `Finsupp.bilinearCombination` and `Fintype.bilinearCombination` as bilinear maps.

Previously, `Fintype.linearCombination` was a bilinear map, but `Finsupp.linearCombination` was only linear in the second variable.
That made `Fintype.linearCombination` unusable in the noncommutative case.
By consistency, `Fintype.linearCombination` is downgraded to a linear map.

Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

@@ -11,10 +11,16 @@ import Mathlib.LinearAlgebra.Finsupp.Supported
 
 ## Main definitions
 
-* `Finsupp.linearCombination R (v : ι → M)`: sends `l : ι → R` to the linear combination of
+* `Finsupp.linearCombination R (v : ι → M)`: sends `l : ι →₀ R` to the linear combination of
   `v i` with coefficients `l i`;
 * `Finsupp.linearCombinationOn`: a restricted version of `Finsupp.linearCombination` with domain
 
+* `Fintype.linearCombination R (v : ι → M)`: sends `l : ι → R` to the linear combination of
+  `v i` with coefficients `l i` (for a finite type `ι`)
+
+* `Finsupp.bilinearCombination R S`, `Fintype.bilinearCombination R S`:
+  a bilinear version of `Finsupp.linearCombination` and `Fintype.linearCombination`.
+
 ## Tags
 
 function with finite support, module, linear algebra
@@ -59,21 +65,6 @@ theorem linearCombination_single (c : R) (a : α) :
 theorem linearCombination_zero_apply (x : α →₀ R) : (linearCombination R (0 : α → M)) x = 0 := by
   simp [linearCombination_apply]
 
-variable (α M)
-
-@[simp]
-theorem linearCombination_zero : linearCombination R (0 : α → M) = 0 :=
-  LinearMap.ext (linearCombination_zero_apply R)
-
-@[simp]
-theorem linearCombination_single_index (c : M) (a : α) (f : α →₀ R) [DecidableEq α] :
-    linearCombination R (Pi.single a c) f = f a • c := by
-  rw [linearCombination_apply, sum_eq_single a, Pi.single_eq_same]
-  · exact fun i _ hi ↦ by rw [Pi.single_eq_of_ne hi, smul_zero]
-  · exact fun _ ↦ by simp only [single_eq_same, zero_smul]
-
-variable {α M}
-
 theorem linearCombination_linear_comp (f : M →ₗ[R] M') :
     linearCombination R (f ∘ v) = f ∘ₗ linearCombination R v := by
   ext
@@ -95,7 +86,7 @@ theorem linearCombination_surjective (h : Function.Surjective v) :
     Function.Surjective (linearCombination R v) := by
   intro x
   obtain ⟨y, hy⟩ := h x
-  exact ⟨Finsupp.single y 1, by simp [hy]⟩
+  exact ⟨single y 1, by simp [hy]⟩
 
 theorem linearCombination_range (h : Function.Surjective v) :
     LinearMap.range (linearCombination R v) = ⊤ :=
@@ -120,7 +111,7 @@ theorem range_linearCombination : LinearMap.range (linearCombination R v) = span
     intro x hx
     rcases hx with ⟨i, hi⟩
     rw [SetLike.mem_coe, LinearMap.mem_range]
-    use Finsupp.single i 1
+    use single i 1
     simp [hi]
 
 theorem lmapDomain_linearCombination (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v i) = v' (f i)) :
@@ -258,6 +249,41 @@ theorem linearCombination_onFinset {s : Finset α} {f : α → R} (g : α → M)
   contrapose! h
   simp [h]
 
+variable (α M)
+
+@[simp]
+theorem linearCombination_zero : linearCombination R (0 : α → M) = 0 :=
+  LinearMap.ext (linearCombination_zero_apply R)
+
+@[simp]
+theorem linearCombination_single_index (c : M) (a : α) (f : α →₀ R) [DecidableEq α] :
+    linearCombination R (Pi.single a c) f = f a • c := by
+  rw [linearCombination_apply, sum_eq_single a, Pi.single_eq_same]
+  · exact fun i _ hi ↦ by rw [Pi.single_eq_of_ne hi, smul_zero]
+  · exact fun _ ↦ by simp only [single_eq_same, zero_smul]
+
+
+variable {α M}
+
+variable [Module S M] [SMulCommClass R S M]
+
+variable (S) in
+/-- `Finsupp.bilinearCombination R S v f` is the linear combination of vectors in `v` with weights
+in `f`.
+
+This map is linear in `v` if `R` is commutative, and always linear in `f`.
+See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
+-/
+def bilinearCombination : (α → M) →ₗ[S] (α →₀ R) →ₗ[R] M where
+  toFun v := linearCombination R v
+  map_add' u v := by ext; simp [Finset.sum_add_distrib, Pi.add_apply, smul_add]
+  map_smul' r v := by ext; simp [Finset.smul_sum, smul_comm]
+
+@[simp]
+theorem bilinearCombination_apply :
+    bilinearCombination R S v = linearCombination R v :=
+  rfl
+
 end LinearCombination
 
 end Finsupp
@@ -268,36 +294,29 @@ variable {α M : Type*} (R : Type*) [Fintype α] [Semiring R] [AddCommMonoid M]
 variable (S : Type*) [Semiring S] [Module S M] [SMulCommClass R S M]
 variable (v : α → M)
 
-/-- `Fintype.linearCombination R S v f` is the linear combination of vectors in `v` with weights
+/-- `Fintype.linearCombination R v f` is the linear combination of vectors in `v` with weights
 in `f`. This variant of `Finsupp.linearCombination` is defined on fintype indexed vectors.
 
 This map is linear in `v` if `R` is commutative, and always linear in `f`.
 See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
 -/
-protected def Fintype.linearCombination : (α → M) →ₗ[S] (α → R) →ₗ[R] M where
-  toFun v :=
-    { toFun := fun f => ∑ i, f i • v i
-      map_add' := fun f g => by simp_rw [← Finset.sum_add_distrib, ← add_smul]; rfl
-      map_smul' := fun r f => by simp_rw [Finset.smul_sum, smul_smul]; rfl }
-  map_add' u v := by ext; simp [Finset.sum_add_distrib, Pi.add_apply, smul_add]
-  map_smul' r v := by ext; simp [Finset.smul_sum, smul_comm]
-
-variable {S}
+protected def Fintype.linearCombination : (α → R) →ₗ[R] M where
+  toFun f := ∑ i, f i • v i
+  map_add' f g := by simp_rw [← Finset.sum_add_distrib, ← add_smul]; rfl
+  map_smul' r f := by simp_rw [Finset.smul_sum, smul_smul]; rfl
 
-theorem Fintype.linearCombination_apply (f) : Fintype.linearCombination R S v f = ∑ i, f i • v i :=
+theorem Fintype.linearCombination_apply (f) : Fintype.linearCombination R v f = ∑ i, f i • v i :=
   rfl
 
 @[simp]
 theorem Fintype.linearCombination_apply_single [DecidableEq α] (i : α) (r : R) :
-    Fintype.linearCombination R S v (Pi.single i r) = r • v i := by
+    Fintype.linearCombination R v (Pi.single i r) = r • v i := by
   simp_rw [Fintype.linearCombination_apply, Pi.single_apply, ite_smul, zero_smul]
   rw [Finset.sum_ite_eq', if_pos (Finset.mem_univ _)]
 
-variable (S)
-
 theorem Finsupp.linearCombination_eq_fintype_linearCombination_apply (x : α → R) :
     linearCombination R v ((Finsupp.linearEquivFunOnFinite R R α).symm x) =
-      Fintype.linearCombination R S v x := by
+      Fintype.linearCombination R v x := by
   apply Finset.sum_subset
   · exact Finset.subset_univ _
   · intro x _ hx
@@ -306,16 +325,34 @@ theorem Finsupp.linearCombination_eq_fintype_linearCombination_apply (x : α →
 
 theorem Finsupp.linearCombination_eq_fintype_linearCombination :
     (linearCombination R v).comp (Finsupp.linearEquivFunOnFinite R R α).symm.toLinearMap =
-      Fintype.linearCombination R S v :=
-  LinearMap.ext <| linearCombination_eq_fintype_linearCombination_apply R S v
-
-variable {S}
+      Fintype.linearCombination R v :=
+  LinearMap.ext <| linearCombination_eq_fintype_linearCombination_apply R v
 
 @[simp]
 theorem Fintype.range_linearCombination :
-    LinearMap.range (Fintype.linearCombination R S v) = Submodule.span R (Set.range v) := by
+    LinearMap.range (Fintype.linearCombination R v) = Submodule.span R (Set.range v) := by
   rw [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearMap.range_comp,
       LinearEquiv.range, Submodule.map_top, Finsupp.range_linearCombination]
+
+/-- `Fintype.bilinearCombination R S v f` is the linear combination of vectors in `v` with weights
+in `f`. This variant of `Finsupp.linearCombination` is defined on fintype indexed vectors.
+
+This map is linear in `v` if `R` is commutative, and always linear in `f`.
+See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
+-/
+protected def Fintype.bilinearCombination : (α → M) →ₗ[S] (α → R) →ₗ[R] M where
+  toFun v := Fintype.linearCombination R v
+  map_add' u v := by ext; simp [Fintype.linearCombination,
+    Finset.sum_add_distrib, Pi.add_apply, smul_add]
+  map_smul' r v := by ext; simp [Fintype.linearCombination, Finset.smul_sum, smul_comm]
+
+variable {S}
+
+@[simp]
+theorem Fintype.bilinearCombination_apply :
+    Fintype.bilinearCombination R S v = Fintype.linearCombination R v :=
+  rfl
+
 section SpanRange
 
 variable {v} {x : M}

Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

@@ -121,7 +121,7 @@ alias ⟨LinearIndependent.injective_linearCombination, _⟩ :=
   linearIndependent_iff_injective_linearCombination
 
 theorem Fintype.linearIndependent_iff_injective [Fintype ι] :
-    LinearIndependent R v ↔ Injective (Fintype.linearCombination R ℕ v) := by
+    LinearIndependent R v ↔ Injective (Fintype.linearCombination R v) := by
   simp [← Finsupp.linearCombination_eq_fintype_linearCombination, LinearIndependent]
 
 theorem LinearIndependent.injective [Nontrivial R] (hv : LinearIndependent R v) : Injective v := by

Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean

@@ -30,10 +30,10 @@ open Polynomial Matrix
 /-- The composition of a matrix (as an endomorphism of `ι → R`) with the projection
 `(ι → R) →ₗ[R] M`. -/
 def PiToModule.fromMatrix [DecidableEq ι] : Matrix ι ι R →ₗ[R] (ι → R) →ₗ[R] M :=
-  (LinearMap.llcomp R _ _ _ (Fintype.linearCombination R R b)).comp algEquivMatrix'.symm.toLinearMap
+  (LinearMap.llcomp R _ _ _ (Fintype.linearCombination R b)).comp algEquivMatrix'.symm.toLinearMap
 
 theorem PiToModule.fromMatrix_apply [DecidableEq ι] (A : Matrix ι ι R) (w : ι → R) :
-    PiToModule.fromMatrix R b A w = Fintype.linearCombination R R b (A *ᵥ w) :=
+    PiToModule.fromMatrix R b A w = Fintype.linearCombination R b (A *ᵥ w) :=
   rfl
 
 theorem PiToModule.fromMatrix_apply_single_one [DecidableEq ι] (A : Matrix ι ι R) (j : ι) :
@@ -44,24 +44,21 @@ theorem PiToModule.fromMatrix_apply_single_one [DecidableEq ι] (A : Matrix ι 
 /-- The endomorphisms of `M` acts on `(ι → R) →ₗ[R] M`, and takes the projection
 to a `(ι → R) →ₗ[R] M`. -/
 def PiToModule.fromEnd : Module.End R M →ₗ[R] (ι → R) →ₗ[R] M :=
-  LinearMap.lcomp _ _ (Fintype.linearCombination R R b)
+  LinearMap.lcomp _ _ (Fintype.linearCombination R b)
 
 theorem PiToModule.fromEnd_apply (f : Module.End R M) (w : ι → R) :
-    PiToModule.fromEnd R b f w = f (Fintype.linearCombination R R b w) :=
+    PiToModule.fromEnd R b f w = f (Fintype.linearCombination R b w) :=
   rfl
 
 theorem PiToModule.fromEnd_apply_single_one [DecidableEq ι] (f : Module.End R M) (i : ι) :
     PiToModule.fromEnd R b f (Pi.single i 1) = f (b i) := by
-  rw [PiToModule.fromEnd_apply]
-  congr
-  convert Fintype.linearCombination_apply_single (S := R) R b i (1 : R)
-  rw [one_smul]
+  rw [PiToModule.fromEnd_apply, Fintype.linearCombination_apply_single, one_smul]
 
 theorem PiToModule.fromEnd_injective (hb : Submodule.span R (Set.range b) = ⊤) :
     Function.Injective (PiToModule.fromEnd R b) := by
   intro x y e
   ext m
-  obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.linearCombination R R b) := by
+  obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.linearCombination R b) := by
     rw [(Fintype.range_linearCombination R b).trans hb]
     exact Submodule.mem_top
   exact (LinearMap.congr_fun e m :)
@@ -78,12 +75,12 @@ def Matrix.Represents (A : Matrix ι ι R) (f : Module.End R M) : Prop :=
 variable {b}
 
 theorem Matrix.Represents.congr_fun {A : Matrix ι ι R} {f : Module.End R M} (h : A.Represents b f)
-    (x) : Fintype.linearCombination R R b (A *ᵥ x) = f (Fintype.linearCombination R R b x) :=
+    (x) : Fintype.linearCombination R b (A *ᵥ x) = f (Fintype.linearCombination R b x) :=
   LinearMap.congr_fun h x
 
 theorem Matrix.represents_iff {A : Matrix ι ι R} {f : Module.End R M} :
     A.Represents b f ↔
-      ∀ x, Fintype.linearCombination R R b (A *ᵥ x) = f (Fintype.linearCombination R R b x) :=
+      ∀ x, Fintype.linearCombination R b (A *ᵥ x) = f (Fintype.linearCombination R b x) :=
   ⟨fun e x => e.congr_fun x, fun H => LinearMap.ext fun x => H x⟩
 
 theorem Matrix.represents_iff' {A : Matrix ι ι R} {f : Module.End R M} :

Mathlib/LinearAlgebra/RootSystem/Base.lean

@@ -129,7 +129,7 @@ lemma eq_one_or_neg_one_of_mem_support_of_smul_mem_aux [Finite ι]
   use f ⟨i, h⟩
   replace hf : P.coroot i = linearCombination R (fun k : b.support ↦ P.coroot k)
       (t • (linearEquivFunOnFinite R _ _).symm (fun x ↦ (f x : R))) := by
-    rw [map_smul, linearCombination_eq_fintype_linearCombination_apply R R,
+    rw [map_smul, linearCombination_eq_fintype_linearCombination_apply,
       Fintype.linearCombination_apply, hf]
     simp_rw [mul_smul, ← Finset.smul_sum]
   let g : b.support →₀ R := single ⟨i, h⟩ 1

Mathlib/RingTheory/LocalRing/Quotient.lean

@@ -97,7 +97,7 @@ lemma basisQuotient_repr {ι} [Fintype ι] (b : Basis ι R S) (x) (i) :
   apply (basisQuotient b).repr.symm.injective
   simp only [Finsupp.linearEquivFunOnFinite_symm_coe, LinearEquiv.symm_apply_apply,
     Basis.repr_symm_apply]
-  rw [Finsupp.linearCombination_eq_fintype_linearCombination_apply _ (R ⧸ p),
+  rw [Finsupp.linearCombination_eq_fintype_linearCombination_apply (R ⧸ p),
     Fintype.linearCombination_apply]
   simp only [Function.comp_apply, basisQuotient_apply,
     Ideal.Quotient.mk_smul_mk_quotient_map_quotient, ← Algebra.smul_def]

Mathlib/Topology/Algebra/Module/Compact.lean

@@ -19,7 +19,7 @@ variable [TopologicalSpace M] [ContinuousAdd M] [ContinuousSMul R M]
 lemma Submodule.isCompact_of_fg [CompactSpace R] {N : Submodule R M} (hN : N.FG) :
     IsCompact (X := M) N := by
   obtain ⟨s, hs⟩ := hN
-  have : LinearMap.range (Fintype.linearCombination R R (α := s) Subtype.val) = N := by
+  have : LinearMap.range (Fintype.linearCombination R (α := s) Subtype.val) = N := by
     simp [Finsupp.range_linearCombination, hs]
   rw [← this]
   refine isCompact_range ?_