feat(LinearAlgebra/PiTensorProduct): dependent version of tmulEquiv (#18534)

Given a family of `R`-modules `N` indexed by `ι ⊕ ι'`, we obtain a linear equivalence `tmulEquivDep : (⨂[R] i₁, N (.inl i₁)) ⊗[R] (⨂[R] i₂, N (.inr i₂)) ≃ₗ[R] ⨂[R] i, N i`, which generalizes `tmulEquiv` (which is the case all `N i` are the same module).



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
Co-authored-by: Eric Wieser <efw@google.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: joelriou

Mathlib/Data/Sum/Basic.lean

@@ -111,6 +111,18 @@ theorem update_inr_apply_inr [DecidableEq β] [DecidableEq (α ⊕ β)] {f : α
     {x : γ} : update f (inr i) x (inr j) = update (f ∘ inr) i x j := by
   rw [← update_inr_comp_inr, Function.comp_apply]
 
+@[simp]
+theorem update_inl_apply_inl' {γ : α ⊕ β → Type*} [DecidableEq α] [DecidableEq (α ⊕ β)]
+    {f : (i : α ⊕ β) → γ i} {i : α} {x : γ (.inl i)} (j : α) :
+    update f (.inl i) x (Sum.inl j) = update (fun j ↦ f (.inl j)) i x j :=
+  Function.update_apply_of_injective f Sum.inl_injective i x j
+
+@[simp]
+theorem update_inr_apply_inr' {γ : α ⊕ β → Type*} [DecidableEq β] [DecidableEq (α ⊕ β)]
+    {f : (i : α ⊕ β) → γ i} {i : β} {x : γ (.inr i)} (j : β) :
+    update f (.inr i) x (Sum.inr j) = update (fun j ↦ f (.inr j)) i x j :=
+  Function.update_apply_of_injective f Sum.inr_injective i x j
+
 @[simp]
 lemma rec_update_left {γ : α ⊕ β → Sort*} [DecidableEq α] [DecidableEq β]
     (f : ∀ a, γ (.inl a)) (g : ∀ b, γ (.inr b)) (a : α) (x : γ (.inl a)) :

Mathlib/LinearAlgebra/Multilinear/Basic.lean

@@ -1365,6 +1365,7 @@ protected def piRingEquiv [Fintype ι] : M₂ ≃ₗ[R] MultilinearMap R (fun _
   right_inv f := f.mkPiRing_apply_one_eq_self
 
 end CommSemiring
+
 section Submodule
 
 variable [Ring R] [∀ i, AddCommMonoid (M₁ i)] [AddCommMonoid M'] [AddCommMonoid M₂]

Mathlib/LinearAlgebra/Multilinear/Curry.lean

@@ -22,9 +22,9 @@ in linear functions), called respectively `multilinearCurryLeftEquiv` and
 
 open Fin Function Finset Set
 
-universe uR uS uι v v' v₁ v₂ v₃
+universe uR uS uι uι' v v' v₁ v₂ v₃
 
-variable {R : Type uR} {S : Type uS} {ι : Type uι} {n : ℕ}
+variable {R : Type uR} {S : Type uS} {ι : Type uι} {ι' : Type uι'} {n : ℕ}
   {M : Fin n.succ → Type v} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} {M' : Type v'}
 
 /-!
@@ -223,87 +223,119 @@ def multilinearCurryRightEquiv :
 
 namespace MultilinearMap
 
-variable {ι' : Type*} {R M₂}
 
-/-- A multilinear map on `∀ i : ι ⊕ ι', M'` defines a multilinear map on `∀ i : ι, M'`
-taking values in the space of multilinear maps on `∀ i : ι', M'`. -/
-def currySum (f : MultilinearMap R (fun _ : ι ⊕ ι' => M') M₂) :
-    MultilinearMap R (fun _ : ι => M') (MultilinearMap R (fun _ : ι' => M') M₂) where
+variable {R M₂} {N : (ι ⊕ ι') → Type*}
+  [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)]
+
+/-- Given a family of modules `N : (ι ⊕ ι') → Type*`, a multilinear map
+on `(fun _ : ι ⊕ ι' => M')` induces a multilinear map on
+`(fun (i : ι) ↦ N (.inl i))` taking values in the space of
+linear maps on `(fun (i : ι') ↦ N (.inr i))`. -/
+def currySum (f : MultilinearMap R N M₂) :
+    MultilinearMap R (fun i : ι ↦ N (.inl i)) (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂) where
   toFun u :=
-    { toFun := fun v => f (Sum.elim u v)
-      map_update_add' := fun v i x y => by
-        letI := Classical.decEq ι
-        simp only [← Sum.update_elim_inr, f.map_update_add]
-      map_update_smul' := fun v i c x => by
-        letI := Classical.decEq ι
-        simp only [← Sum.update_elim_inr, f.map_update_smul] }
+    { toFun v := f (Sum.rec u v)
+      map_update_add' := by letI := Classical.decEq ι; aesop
+      map_update_smul' := by letI := Classical.decEq ι; aesop }
   map_update_add' u i x y :=
-    ext fun v => by
-      letI := Classical.decEq ι'
-      simp only [MultilinearMap.coe_mk, add_apply, ← Sum.update_elim_inl, f.map_update_add]
+    ext fun _ ↦ by letI := Classical.decEq ι'; simp
   map_update_smul' u i c x :=
-    ext fun v => by
-      letI := Classical.decEq ι'
-      simp only [MultilinearMap.coe_mk, smul_apply, ← Sum.update_elim_inl, f.map_update_smul]
+    ext fun _ ↦ by letI := Classical.decEq ι'; simp
+
+@[simp low]
+theorem currySum_apply (f : MultilinearMap R N M₂)
+    (u : (i : ι) → N (Sum.inl i)) (v : (i : ι') → N (Sum.inr i)) :
+    currySum f u v = f (Sum.rec u v) := rfl
 
 @[simp]
-theorem currySum_apply (f : MultilinearMap R (fun _ : ι ⊕ ι' => M') M₂) (u : ι → M')
-    (v : ι' → M') : f.currySum u v = f (Sum.elim u v) :=
-  rfl
+theorem currySum_apply' {N : Type*} [AddCommMonoid N] [Module R N]
+    (f : MultilinearMap R (fun _ : ι ⊕ ι' ↦ N) M₂)
+    (u : ι → N) (v : ι' → N) :
+    currySum f u v = f (Sum.elim u v) := rfl
 
-/-- A multilinear map on `∀ i : ι, M'` taking values in the space of multilinear maps
-on `∀ i : ι', M'` defines a multilinear map on `∀ i : ι ⊕ ι', M'`. -/
-def uncurrySum (f : MultilinearMap R (fun _ : ι => M') (MultilinearMap R (fun _ : ι' => M') M₂)) :
-    MultilinearMap R (fun _ : ι ⊕ ι' => M') M₂ where
-  toFun u := f (u ∘ Sum.inl) (u ∘ Sum.inr)
-  map_update_add' u i x y := by
-    letI := (@Sum.inl_injective ι ι').decidableEq
-    letI := (@Sum.inr_injective ι ι').decidableEq
-    cases i <;>
-      simp only [MultilinearMap.map_update_add, add_apply, Sum.update_inl_comp_inl,
-        Sum.update_inl_comp_inr, Sum.update_inr_comp_inl, Sum.update_inr_comp_inr]
-  map_update_smul' u i c x := by
-    letI := (@Sum.inl_injective ι ι').decidableEq
-    letI := (@Sum.inr_injective ι ι').decidableEq
-    cases i <;>
-      simp only [MultilinearMap.map_update_smul, smul_apply, Sum.update_inl_comp_inl,
-        Sum.update_inl_comp_inr, Sum.update_inr_comp_inl, Sum.update_inr_comp_inr]
+@[simp]
+lemma currySum_add (f₁ f₂ : MultilinearMap R N M₂):
+    currySum (f₁ + f₂) = currySum f₁ + currySum f₂ := rfl
 
 @[simp]
-theorem uncurrySum_aux_apply
-    (f : MultilinearMap R (fun _ : ι => M') (MultilinearMap R (fun _ : ι' => M') M₂))
-    (u : ι ⊕ ι' → M') : f.uncurrySum u = f (u ∘ Sum.inl) (u ∘ Sum.inr) :=
+lemma currySum_smul (r : R) (f : MultilinearMap R N M₂):
+    currySum (r • f) = r • currySum f := rfl
+
+/-- Given a family of modules `N : (ι ⊕ ι') → Type*`, a multilinear map on
+`(fun (i : ι) ↦ N (.inl i))` taking values in the space of
+linear maps on `(fun (i : ι') ↦ N (.inr i))` induces a multilinear map
+on `(fun _ : ι ⊕ ι' => M')` induces. -/
+def uncurrySum
+    (g : MultilinearMap R (fun i : ι ↦ N (.inl i))
+      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
+    MultilinearMap R N M₂  where
+  toFun u := g (fun i ↦ u (.inl i)) (fun i' ↦ u (.inr i'))
+  map_update_add' := by
+    letI := Classical.decEq ι
+    letI := Classical.decEq ι'
+    rintro _ _ (_ | _) _ _ <;> simp
+  map_update_smul' := by
+    letI := Classical.decEq ι
+    letI := Classical.decEq ι'
+    rintro _ _ (_ | _) _ _ <;> simp
+
+@[simp]
+theorem uncurrySum_apply
+    (g : MultilinearMap R (fun i : ι ↦ N (.inl i))
+      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) (u) :
+    g.uncurrySum u =
+      g (fun i ↦ u (.inl i)) (fun i' ↦ u (.inr i')) := rfl
+
+@[simp]
+lemma uncurrySum_add
+    (g₁ g₂ : MultilinearMap R (fun i : ι ↦ N (.inl i))
+      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
+    uncurrySum (g₁ + g₂) = uncurrySum g₁ + uncurrySum g₂ :=
+  rfl
+
+lemma uncurrySum_smul
+    (r : R) (g : MultilinearMap R (fun i : ι ↦ N (.inl i))
+      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
+    uncurrySum (r • g) = r • uncurrySum g :=
   rfl
 
-variable (ι ι' R M₂ M')
+@[deprecated (since := "2025-04-23")] alias uncurrySum_aux_apply := uncurrySum_apply
 
-/-- Linear equivalence between the space of multilinear maps on `∀ i : ι ⊕ ι', M'` and the space
-of multilinear maps on `∀ i : ι, M'` taking values in the space of multilinear maps
-on `∀ i : ι', M'`. -/
-def currySumEquiv :
-    MultilinearMap R (fun _ : ι ⊕ ι' => M') M₂ ≃ₗ[R]
-      MultilinearMap R (fun _ : ι => M') (MultilinearMap R (fun _ : ι' => M') M₂) where
-  toFun := currySum
-  invFun := uncurrySum
-  left_inv f := ext fun u => by simp
-  right_inv f := by
-    ext
-    simp
-  map_add' f g := by
-    ext
-    rfl
-  map_smul' c f := by
-    ext
+@[simp]
+lemma uncurrySum_currySum (f : MultilinearMap R N M₂) :
+    uncurrySum (currySum f) = f := by
+  ext
+  simp only [uncurrySum_apply, currySum_apply]
+  congr
+  ext (_ | _) <;> simp
+
+@[simp]
+lemma currySum_uncurrySum
+    (g : MultilinearMap R (fun i : ι ↦ N (.inl i))
+      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂)) :
+  currySum (uncurrySum g) = g :=
     rfl
 
-variable {ι ι' R M₂ M'}
+/-- Multilinear maps on `N : (ι ⊕ ι') → Type*` identify to multilinear maps
+from `(fun (i : ι) ↦ N (.inl i))` taking values in the space of
+linear maps on `(fun (i : ι') ↦ N (.inr i))`. -/
+@[simps]
+def currySumEquiv : MultilinearMap R N M₂ ≃ₗ[R]
+    MultilinearMap R (fun i : ι ↦ N (.inl i))
+      (MultilinearMap R (fun i : ι' ↦ N (.inr i)) M₂) where
+  toFun := currySum
+  invFun := uncurrySum
+  left_inv _ := by simp
+  right_inv _ := rfl
+  map_add' := by aesop
+  map_smul' := by aesop
 
 @[simp]
-theorem coe_currySumEquiv : ⇑(currySumEquiv R ι M₂ M' ι') = currySum :=
+theorem coe_currySumEquiv : ⇑(currySumEquiv (R := R) (N := N) (M₂ := M₂)) = currySum :=
   rfl
 
 @[simp]
-theorem coe_currySumEquiv_symm : ⇑(currySumEquiv R ι M₂ M' ι').symm = uncurrySum :=
+theorem coe_currySumEquiv_symm : ⇑(currySumEquiv (R := R) (N := N) (M₂ := M₂)).symm = uncurrySum :=
   rfl
 
 variable (R M₂ M')
@@ -316,7 +348,7 @@ def curryFinFinset {k l n : ℕ} {s : Finset (Fin n)} (hk : #s = k) (hl : #sᶜ
     MultilinearMap R (fun _ : Fin n => M') M₂ ≃ₗ[R]
       MultilinearMap R (fun _ : Fin k => M') (MultilinearMap R (fun _ : Fin l => M') M₂) :=
   (domDomCongrLinearEquiv R R M' M₂ (finSumEquivOfFinset hk hl).symm).trans
-    (currySumEquiv R (Fin k) M₂ M' (Fin l))
+    currySumEquiv
 
 variable {R M₂ M'}
 

Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean

@@ -22,6 +22,47 @@ variable {R ι₁ ι₂ ι₃ ι₄ : Type*}
 variable [CommSemiring R]
 variable {N₁ : Type*} [AddCommMonoid N₁] [Module R N₁]
 variable {N₂ : Type*} [AddCommMonoid N₂] [Module R N₂]
+
+attribute [local simp] add_tmul tmul_add smul_tmul
+
+section
+
+variable {N : ι₁ ⊕ ι₂ → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)]
+
+/-- Given a family of modules `N` indexed by a type `ι₁ ⊕ ι₂`,
+a multilinear map from the modules `N (.inl i₁)` to `N₁` and
+a multilinear map from the modules `N (.inr i₁)` to `N₂`, this
+is the induced multilinear map from all the modules `N i` to `N₁ ⊗ N₂`. -/
+@[simps apply]
+def domCoprodDep (a : MultilinearMap R (fun i₁ ↦ N (.inl i₁)) N₁)
+    (b : MultilinearMap R (fun i₂ ↦ N (.inr i₂)) N₂) :
+    MultilinearMap R N (N₁ ⊗[R] N₂) where
+  toFun v := a (fun i₁ ↦ v (.inl i₁)) ⊗ₜ b (fun i₂ ↦ v (.inr i₂))
+  map_update_add' := by
+    rintro _ _ (_ | _) _ _
+    · letI := Classical.decEq ι₁; simp
+    · letI := Classical.decEq ι₂; simp
+  map_update_smul' := by
+    rintro _ m (i₁ | i₂) p q
+    · letI := Classical.decEq ι₁; simp
+    · letI := Classical.decEq ι₂; simp
+
+/-- A more bundled version of `MultilinearMap.domCoprodDep`, as a linear map
+from the tensor product of spaces of multilinear maps. -/
+def domCoprodDep' :
+    MultilinearMap R (fun i₁ ↦ N (.inl i₁)) N₁ ⊗[R] MultilinearMap R (fun i₂ ↦ N (.inr i₂)) N₂ →ₗ[R]
+        MultilinearMap R N (N₁ ⊗[R] N₂) :=
+  TensorProduct.lift (LinearMap.mk₂ R domCoprodDep
+    (by aesop) (by aesop) (by aesop) (by aesop))
+
+@[simp]
+theorem domCoprodDep'_apply (a : MultilinearMap R (fun i₁ ↦ N (.inl i₁)) N₁)
+    (b : MultilinearMap R (fun i₂ ↦ N (.inr i₂)) N₂) :
+    domCoprodDep' (a ⊗ₜ b) = domCoprodDep a b := by
+  rfl
+
+end
+
 variable {N : Type*} [AddCommMonoid N] [Module R N]
 
 /-- Given two multilinear maps `(ι₁ → N) → N₁` and `(ι₂ → N) → N₂`, this produces the map
@@ -37,39 +78,18 @@ introduces `Sum.elim N'₁ N'₂` types in the result which are difficult to wor
 to the simple case defined here. See [this zulip thread](
 https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Instances.20on.20.60sum.2Eelim.20A.20B.20i.60/near/218484619).
 -/
-@[simps apply]
+@[simps! apply]
 def domCoprod (a : MultilinearMap R (fun _ : ι₁ => N) N₁)
     (b : MultilinearMap R (fun _ : ι₂ => N) N₂) :
-    MultilinearMap R (fun _ : ι₁ ⊕ ι₂ => N) (N₁ ⊗[R] N₂) where
-  toFun v := (a fun i => v (Sum.inl i)) ⊗ₜ b fun i => v (Sum.inr i)
-  map_update_add' _ i p q := by
-    letI := (@Sum.inl_injective ι₁ ι₂).decidableEq
-    letI := (@Sum.inr_injective ι₁ ι₂).decidableEq
-    cases i <;> simp [TensorProduct.add_tmul, TensorProduct.tmul_add]
-  map_update_smul' _ i c p := by
-    letI := (@Sum.inl_injective ι₁ ι₂).decidableEq
-    letI := (@Sum.inr_injective ι₁ ι₂).decidableEq
-    cases i <;> simp [TensorProduct.smul_tmul', TensorProduct.tmul_smul]
+    MultilinearMap R (fun _ : ι₁ ⊕ ι₂ => N) (N₁ ⊗[R] N₂) :=
+  domCoprodDep a b
 
 /-- A more bundled version of `MultilinearMap.domCoprod` that maps
 `((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂)` to `(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂`. -/
 def domCoprod' :
     MultilinearMap R (fun _ : ι₁ => N) N₁ ⊗[R] MultilinearMap R (fun _ : ι₂ => N) N₂ →ₗ[R]
       MultilinearMap R (fun _ : ι₁ ⊕ ι₂ => N) (N₁ ⊗[R] N₂) :=
-  TensorProduct.lift <|
-    LinearMap.mk₂ R domCoprod
-      (fun m₁ m₂ n => by
-        ext
-        simp only [domCoprod_apply, TensorProduct.add_tmul, add_apply])
-      (fun c m n => by
-        ext
-        simp only [domCoprod_apply, TensorProduct.smul_tmul', smul_apply])
-      (fun m n₁ n₂ => by
-        ext
-        simp only [domCoprod_apply, TensorProduct.tmul_add, add_apply])
-      fun c m n => by
-      ext
-      simp only [domCoprod_apply, TensorProduct.tmul_smul, smul_apply]
+  domCoprodDep' (R := R) (N := fun (_ : ι₁ ⊕ ι₂) ↦ N)
 
 @[simp]
 theorem domCoprod'_apply (a : MultilinearMap R (fun _ : ι₁ => N) N₁)