feat: more connections between TensorProduct and map₂ (#29391)

The new lemmas about `map₂` are analogous to the lemmas about `Set.image2`.

Author: eric-wieser

Mathlib/Algebra/Lie/TensorProduct.lean

@@ -192,7 +192,7 @@ theorem lieIdeal_oper_eq_tensor_map_range :
     ⁅I, N⁆ = ((toModuleHom R L M).comp (mapIncl I N : I ⊗[R] N →ₗ⁅R,L⁆ L ⊗[R] M)).range := by
   rw [← toSubmodule_inj, lieIdeal_oper_eq_linear_span, LieModuleHom.toSubmodule_range,
     LieModuleHom.toLinearMap_comp, LinearMap.range_comp, mapIncl_def, toLinearMap_map,
-    TensorProduct.map_range_eq_span_tmul, Submodule.map_span]
+    TensorProduct.range_map_eq_span_tmul, Submodule.map_span]
   congr; ext m; constructor
   · rintro ⟨⟨x, hx⟩, ⟨n, hn⟩, rfl⟩; use x ⊗ₜ n; constructor
     · use ⟨x, hx⟩, ⟨n, hn⟩; rfl

Mathlib/Algebra/Module/Submodule/Bilinear.lean

@@ -20,6 +20,10 @@ This file provides `Submodule.map₂`, which is later used to implement `Submodu
 
 This file is quite similar to the n-ary section of `Data.Set.Basic` and to `Order.Filter.NAry`.
 Please keep them in sync.
+
+## TODO
+
+Generalize this file to semilinear maps.
 -/
 
 
@@ -147,4 +151,33 @@ theorem map₂_span_singleton_eq_map (f : M →ₗ[R] N →ₗ[R] P) (m : M) :
 theorem map₂_span_singleton_eq_map_flip (f : M →ₗ[R] N →ₗ[R] P) (s : Submodule R M) (n : N) :
     map₂ f s (span R {n}) = map (f.flip n) s := by rw [← map₂_span_singleton_eq_map, map₂_flip]
 
+section comp
+variable {M₂ N₂ P₂ : Type*}
+variable [AddCommMonoid M₂] [AddCommMonoid N₂] [AddCommMonoid P₂]
+variable [Module R M₂] [Module R N₂] [Module R P₂]
+
+theorem map_map₂ (f : P →ₗ[R] P₂) (g : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
+    map f (map₂ g p q) = map₂ (g.compr₂ f) p q :=
+  map_iSup _ _ |>.trans <| iSup_congr fun _ => map_comp _ _ _ |>.symm
+
+theorem map₂_map_right
+    (f : M →ₗ[R] N₂ →ₗ[R] P) (g : N →ₗ[R] N₂) (p : Submodule R M) (q : Submodule R N) :
+    map₂ f p (map g q) = map₂ (f.compl₂ g) p q :=
+  iSup_congr fun _ => map_comp _ _ _ |>.symm
+
+theorem map₂_map_left
+    (f : M₂ →ₗ[R] N →ₗ[R] P) (g : M →ₗ[R] M₂) (p : Submodule R M) (q : Submodule R N) :
+    map₂ f (map g p) q = map₂ (f ∘ₗ g) p q := by
+  rw [← map₂_flip, map₂_map_right, ← map₂_flip]
+  rfl
+
+theorem map₂_map_map
+    (f : M₂ →ₗ[R] N₂ →ₗ[R] P) (g : M →ₗ[R] M₂) (h : N →ₗ[R] N₂)
+    (p : Submodule R M) (q : Submodule R N) :
+    map₂ f (map g p) (map h q) = map₂ (f.compl₁₂ g h) p q := by
+  rw [map₂_map_right, map₂_map_left]
+  rfl
+
+end comp
+
 end Submodule

Mathlib/LinearAlgebra/TensorProduct/Basic.lean

@@ -731,27 +731,34 @@ lemma map_comm (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (x : N ⊗[R] M) :
     map f g (TensorProduct.comm R N M x) = TensorProduct.comm R Q P (map g f x) :=
   DFunLike.congr_fun (map_comp_comm_eq _ _) _
 
-theorem map_range_eq_span_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
+theorem range_map (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
+    range (map f g) = .map₂ (mk R _ _) (range f) (range g) := by
+  simp_rw [← Submodule.map_top, Submodule.map₂_map_map, ← map₂_mk_top_top_eq_top,
+    Submodule.map_map₂]
+  rfl
+
+theorem range_map_eq_span_tmul (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
     range (map f g) = Submodule.span R { t | ∃ m n, f m ⊗ₜ g n = t } := by
   simp only [← Submodule.map_top, ← span_tmul_eq_top, Submodule.map_span]
   congr; ext t
   simp
 
+@[deprecated (since := "2025-09-07")] alias map_range_eq_span_tmul := range_map_eq_span_tmul
+
 /-- Given submodules `p ⊆ P` and `q ⊆ Q`, this is the natural map: `p ⊗ q → P ⊗ Q`. -/
 @[simp]
 def mapIncl (p : Submodule R P) (q : Submodule R Q) : p ⊗[R] q →ₗ[R] P ⊗[R] Q :=
   map p.subtype q.subtype
 
 lemma range_mapIncl (p : Submodule R P) (q : Submodule R Q) :
-    LinearMap.range (mapIncl p q) = Submodule.span R (Set.image2 (· ⊗ₜ ·) p q) := by
-  rw [mapIncl, map_range_eq_span_tmul]
-  congr; ext; simp
+    LinearMap.range (mapIncl p q) = .map₂ (mk R _ _) p q := by
+  simp_rw [mapIncl, range_map, Submodule.range_subtype]
 
 theorem map₂_eq_range_lift_comp_mapIncl (f : P →ₗ[R] Q →ₗ[R] M)
     (p : Submodule R P) (q : Submodule R Q) :
     Submodule.map₂ f p q = LinearMap.range (lift f ∘ₗ mapIncl p q) := by
-  simp_rw [LinearMap.range_comp, range_mapIncl, Submodule.map_span,
-    Set.image_image2, Submodule.map₂_eq_span_image2, lift.tmul]
+  simp_rw [LinearMap.range_comp, range_mapIncl, Submodule.map_map₂]
+  rfl
 
 section
 
@@ -772,7 +779,7 @@ lemma map_map (f₂ : M₂ →ₗ[R] M₃) (g₂ : N₂ →ₗ[R] N₃) (f₁ :
 lemma range_mapIncl_mono {p p' : Submodule R P} {q q' : Submodule R Q} (hp : p ≤ p') (hq : q ≤ q') :
     LinearMap.range (mapIncl p q) ≤ LinearMap.range (mapIncl p' q') := by
   simp_rw [range_mapIncl]
-  exact Submodule.span_mono (Set.image2_subset hp hq)
+  exact Submodule.map₂_le_map₂ hp hq
 
 theorem lift_comp_map (i : P →ₗ[R] Q →ₗ[R] Q') (f : M →ₗ[R] P) (g : N →ₗ[R] Q) :
     (lift i).comp (map f g) = lift ((i.comp f).compl₂ g) :=

Mathlib/LinearAlgebra/TensorProduct/Quotient.lean

@@ -106,7 +106,7 @@ noncomputable def quotientTensorEquiv (m : Submodule R M) :
     simp only [Submodule.map_sup]
     erw [Submodule.map_id, Submodule.map_id]
     simp only [sup_eq_left]
-    rw [map_range_eq_span_tmul, map_range_eq_span_tmul]
+    rw [range_map_eq_span_tmul, range_map_eq_span_tmul]
     simp)
 
 @[simp]
@@ -136,7 +136,7 @@ noncomputable def tensorQuotientEquiv (n : Submodule R N) :
     simp only [Submodule.map_sup]
     erw [Submodule.map_id, Submodule.map_id]
     simp only [sup_eq_right]
-    rw [map_range_eq_span_tmul, map_range_eq_span_tmul]
+    rw [range_map_eq_span_tmul, range_map_eq_span_tmul]
     simp)
 
 @[simp]