feat(LinearAlgebra/Multilinear/DirectSum, LinearAlgebra/DirectSum/{PiTensorProduct,Finsupp}): interaction between MultilinearMap and DirectSum, and between PiTensorProduct and DirectSum

Mathlib.lean

@@ -2559,6 +2559,7 @@ import Mathlib.LinearAlgebra.Dimension.LinearMap
 import Mathlib.LinearAlgebra.Dimension.Localization
 import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 import Mathlib.LinearAlgebra.DirectSum.Finsupp
+import Mathlib.LinearAlgebra.DirectSum.PiTensorProduct
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 import Mathlib.LinearAlgebra.Dual
 import Mathlib.LinearAlgebra.Eigenspace.Basic
@@ -2631,6 +2632,7 @@ import Mathlib.LinearAlgebra.Matrix.Transvection
 import Mathlib.LinearAlgebra.Matrix.ZPow
 import Mathlib.LinearAlgebra.Multilinear.Basic
 import Mathlib.LinearAlgebra.Multilinear.Basis
+import Mathlib.LinearAlgebra.Multilinear.DirectSum
 import Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
 import Mathlib.LinearAlgebra.Multilinear.TensorProduct
 import Mathlib.LinearAlgebra.Orientation

Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

@@ -6,20 +6,24 @@
 import Mathlib.Algebra.DirectSum.Finsupp
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
+import Mathlib.LinearAlgebra.DirectSum.PiTensorProduct
 
 #align_import linear_algebra.direct_sum.finsupp from "leanprover-community/mathlib"@"9b9d125b7be0930f564a68f1d73ace10cf46064d"
 
 /-!
 # Results on finitely supported functions.
 
-The tensor product of `ι →₀ M` and `κ →₀ N` is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`.
+* The tensor product of `ι →₀ M` and `κ →₀ N` is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`.
+* The tensor product of the family `κ i →₀ M i` indexed by `ι` is linearly equivalent to
+`∏ i, κ i →₀ ⨂[R] i, M i`.
 -/
 
-
 noncomputable section
 
 open DirectSum Set LinearMap Submodule TensorProduct
 
+section TensorProduct
+
 variable (R M N ι κ : Type*)
   [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
 
@@ -88,4 +92,109 @@
   aesop (add norm [Finsupp.single_apply])
 #align finsupp_tensor_finsupp'_single_tmul_single finsuppTensorFinsupp'_single_tmul_single
 
+end TensorProduct
+
+/-!
+The case of `PiTensorProduct`.
+-/
+
+section PiTensorProduct
+
+open PiTensorProduct BigOperators
+
+attribute [local ext] TensorProduct.ext
+
+variable (R : Type*) [CommSemiring R]
+
+variable {ι : Type*}
+
+variable [Fintype ι]
+
+variable [DecidableEq ι]
+
+variable (κ : ι → Type*) [(i : ι) → DecidableEq (κ i)]
+
+variable (M : ι → Type*)
+
+variable [∀ i, AddCommMonoid (M i)]
+
+variable [∀ i, Module R (M i)]
+
+variable [(i : ι) → (x : M i) → Decidable (x ≠ 0)]
+
+/-- If `ι` is a `Fintype`, `κ i` is a family of types indexed by `ι` and `M i` is a family
+of modules indexed by `ι`, then the tensor product of the family `κ i →₀ M i` is linearly
+equivalent to `∏ i, κ i →₀ ⨂[R] i, M i`.
+-/
+def finsuppPiTensorProduct : (⨂[R] i, κ i →₀ M i) ≃ₗ[R] ((i : ι) → κ i) →₀ ⨂[R] i, M i :=
+  PiTensorProduct.congr (fun i ↦ finsuppLEquivDirectSum R (M i) (κ i)) ≪≫ₗ
+  (PiTensorProduct.directSum R (fun (i : ι) ↦ fun (_ : κ i) ↦ M i)) ≪≫ₗ
+  (finsuppLEquivDirectSum R (⨂[R] i, M i) ((i : ι) → κ i)).symm
+
+@[simp]
+theorem finsuppPiTensorProduct_tprod_single (p : (i : ι) → κ i) (m : (i : ι) → M i) :
+    finsuppPiTensorProduct R κ M (⨂ₜ[R] i, Finsupp.single (p i) (m i)) =
+    Finsupp.single p (⨂ₜ[R] i, m i) := by
+  classical
+  simp only [finsuppPiTensorProduct, PiTensorProduct.directSum, LinearEquiv.trans_apply,
+    congr_tprod, finsuppLEquivDirectSum_single, LinearEquiv.ofLinear_apply, lift.tprod,
+    MultilinearMap.fromDirectSumEquiv_apply, compMultilinearMap_apply, map_sum,
+    finsuppLEquivDirectSum_symm_lof]
+  rw [Finset.sum_subset (piFinset_support_lof_sub R κ p _)]
+  · rw [Finset.sum_singleton]
+    simp only [lof_apply]
+  · intro q _ hq
+    simp only [Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq, not_forall, not_not] at hq
+    obtain ⟨i, hi⟩ := hq
+    simp only [Finsupp.single_eq_zero]
+    exact (tprod R).map_coord_zero i hi
+
+@[simp]
+theorem finsuppPiTensorProduct_apply (f : (i : ι) → (κ i →₀ M i)) (p : (i : ι) → κ i) :
+    finsuppPiTensorProduct R κ M (⨂ₜ[R] i, f i) p = ⨂ₜ[R] i, f i (p i) := by
+  rw [congrArg (tprod R) (funext (fun i ↦ (Eq.symm (Finsupp.sum_single (f i)))))]
+  erw [MultilinearMap.map_sum_finset (tprod R)]
+  simp only [map_sum, finsuppPiTensorProduct_tprod_single]
+  rw [Finset.sum_apply']
+  rw [← Finset.sum_union_eq_right (s₁ := {p}) (fun _ _ h ↦ by
+       simp only [Fintype.mem_piFinset, Finsupp.mem_support_iff, ne_eq, not_forall, not_not] at h
+       obtain ⟨i, hi⟩ := h
+       rw [(tprod R).map_coord_zero i hi, Finsupp.single_zero, Finsupp.coe_zero, Pi.zero_apply]),
+   Finset.sum_union_eq_left (fun _ _ h ↦ Finsupp.single_eq_of_ne (Finset.not_mem_singleton.mp h)),
+   Finset.sum_singleton, Finsupp.single_eq_same]
+
+@[simp]
+theorem finsuppPiTensorProduct_symm_single_tprod (p : (i : ι) → κ i) (m : (i : ι) → M i) :
+    (finsuppPiTensorProduct R κ M).symm (Finsupp.single p (⨂ₜ[R] i, m i)) =
+    ⨂ₜ[R] i, Finsupp.single (p i) (m i) :=
+  (LinearEquiv.symm_apply_eq _).2 (finsuppPiTensorProduct_tprod_single _ _ _ _ _).symm
+
+variable [(x : R) → Decidable (x ≠ 0)]
+
+/-- A variant of `finsuppPiTensorProduct` where all modules `M i` are the ground ring.
+-/
+def finsuppPiTensorProduct' : (⨂[R] i, (κ i →₀ R)) ≃ₗ[R] ((i : ι) → κ i) →₀ R :=
+  finsuppPiTensorProduct R κ (fun _ ↦ R) ≪≫ₗ
+  Finsupp.lcongr (Equiv.refl ((i : ι) → κ i)) (constantBaseRingEquiv ι R)
+
+@[simp]
+theorem finsuppPiTensorProduct'_apply_apply (f : (i : ι) → κ i →₀ R) (p : (i : ι) → κ i) :
+    finsuppPiTensorProduct' R κ (⨂ₜ[R] i, f i) p = ∏ i, f i (p i) := by
+  simp only [finsuppPiTensorProduct', LinearEquiv.trans_apply, Finsupp.lcongr_apply_apply,
+    Equiv.refl_symm, Equiv.refl_apply, finsuppPiTensorProduct_apply, constantBaseRingEquiv_tprod]
+
+@[simp]
+theorem finsuppPiTensorProduct'_tprod_single (p : (i : ι) → κ i) (r : ι → R) :
+    finsuppPiTensorProduct' R κ (⨂ₜ[R] i, Finsupp.single (p i) (r i)) =
+    Finsupp.single p (∏ i, r i) := by
+  ext q
+  simp only [finsuppPiTensorProduct'_apply_apply]
+  by_cases h : q = p
+  · rw [h]; simp only [Finsupp.single_eq_same]
+  · obtain ⟨i, hi⟩ := Function.ne_iff.mp h
+    rw [Finsupp.single_eq_of_ne (Ne.symm h), Finset.prod_eq_zero (Finset.mem_univ i)
+      (by rw [(Finsupp.single_eq_of_ne (Ne.symm hi))])]
+
+end PiTensorProduct
+
 end

Mathlib/LinearAlgebra/DirectSum/PiTensorProduct.lean

@@ -0,0 +1,70 @@
+/-
+Copyright (c) 2024 Sophie Morel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sophie Morel
+-/
+import Mathlib.LinearAlgebra.PiTensorProduct
+import Mathlib.Algebra.DirectSum.Module
+import Mathlib.LinearAlgebra.Multilinear.DirectSum
+
+/-!
+# Tensor products of direct sums
+
+This file shows that taking `PiTensorProduct`s commutes with taking `DirectSum`s in all arguments.
+
+## Main results
+
+* `PiTensorProduct.directSum`: the linear equivalence between a `PiTensorProduct` of `DirectSum`s
+and the `DirectSum` of the `PiTensorProduct`s.
+-/
+
+suppress_compilation
+
+namespace PiTensorProduct
+
+open PiTensorProduct DirectSum LinearMap
+
+open scoped TensorProduct
+
+variable (R : Type*) [CommSemiring R]
+
+variable {ι : Type*} [Fintype ι] [DecidableEq ι]
+
+variable {κ : ι → Type*} [(i : ι) → DecidableEq (κ i)]
+
+variable (M : (i : ι) → κ i → Type*) (M' : Type*)
+
+variable [Π i (j : κ i), AddCommMonoid (M i j)] [AddCommMonoid M']
+
+variable [Π i (j : κ i), Module R (M i j)] [Module R M']
+
+variable [Π i (j : κ i) (x : M i j),  Decidable (x ≠ 0)]
+
+/-- The linear equivalence `⨂[R] i, (⨁ j : κ i, M i j) ≃ ⨁ p : (i : ι) → κ i, ⨂[R] i, M i (p i)`,
+ i.e. "tensor product distributes over direct sum". -/
+protected def directSum :
+    (⨂[R] i, (⨁ j : κ i, M i j)) ≃ₗ[R] ⨁ p : Π i, κ i, ⨂[R] i, M i (p i) := by
+  refine LinearEquiv.ofLinear (R := R) (R₂ := R) ?toFun ?invFun ?left ?right
+  · exact lift (MultilinearMap.fromDirectSumEquiv R (M := M)
+      (fun p ↦ (DirectSum.lof R _ _ p).compMultilinearMap (PiTensorProduct.tprod R)))
+  · exact DirectSum.toModule R _ _ (fun p ↦ lift (LinearMap.compMultilinearMap
+      (PiTensorProduct.map (fun i ↦ DirectSum.lof R _ _ (p i))) (tprod R)))
+  · ext p x
+    simp only [compMultilinearMap_apply, coe_comp, Function.comp_apply, toModule_lof, lift.tprod,
+      map_tprod, MultilinearMap.fromDirectSumEquiv_apply, id_comp]
+    rw [Finset.sum_subset (piFinset_support_lof_sub R κ p x)]
+    · rw [Finset.sum_singleton]
+      simp only [lof_apply]
+    · simp only [Finset.mem_singleton, Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq,
+        not_forall, not_not, forall_exists_index, forall_eq, lof_apply]
+      intro i hi
+      rw [(tprod R).map_coord_zero i hi, LinearMap.map_zero]
+  · ext x
+    simp only [compMultilinearMap_apply, coe_comp, Function.comp_apply, lift.tprod,
+      MultilinearMap.fromDirectSumEquiv_apply, map_sum, toModule_lof, map_tprod, id_coe, id_eq]
+    change _ = tprod R (fun i ↦ x i)
+    rw [funext (fun i ↦ Eq.symm (DirectSum.sum_support_of (fun j ↦ M i j) (x i)))]
+    rw [MultilinearMap.map_sum_finset]
+    rfl
+
+end PiTensorProduct

Mathlib/LinearAlgebra/Multilinear/DirectSum.lean

@@ -0,0 +1,166 @@
+/-
+Copyright (c) 2024 Sophie Morel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sophie Morel
+-/
+import Mathlib.Algebra.DirectSum.Module
+import Mathlib.LinearAlgebra.Multilinear.Basic
+
+/-!
+# Multilinear maps from direct sums
+
+This file describes multilinear maps on direct sums.
+
+## Main results
+
+* `MultilinearMap.fromDirectSumEquiv` : If 'ι` is a `Fintype`, `κ i` is a family of types
+indexed by `ι` and we are given a `R`-module `M i j` for every `i : ι` and `j : κ i`, this is
+the linear equivalence between `Π p : (i : ι) → κ i, MultilinearMap R (fun i ↦ M i (p i)) M'` and
+`MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M'`.
+-/
+
+namespace MultilinearMap
+
+open DirectSum LinearMap BigOperators Function
+
+variable (R : Type*) [CommSemiring R]
+
+variable {ι : Type*} [Fintype ι] [DecidableEq ι]
+
+variable (κ : ι → Type*) [(i : ι) → DecidableEq (κ i)]
+
+variable {M : (i : ι) → κ i → Type*} {M' : Type*}
+
+variable [Π i (j : κ i), AddCommMonoid (M i j)] [AddCommMonoid M']
+
+variable [Π i (j : κ i), Module R (M i j)] [Module R M']
+
+variable [Π i (j : κ i) (x : M i j), Decidable (x ≠ 0)]
+
+theorem fromDirectSum_aux1 (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M')
+    (x : Π i, ⨁ (j : κ i), M i j) {p : Π i, κ i}
+    (hp : p ∉ Fintype.piFinset (fun i ↦ (x i).support)) :
+    (f p) (fun j ↦ (x j) (p j)) = 0 := by
+  simp only [Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq, not_forall, not_not] at hp
+  obtain ⟨i, hi⟩ := hp
+  exact (f p).map_coord_zero i hi
+
+theorem fromDirectSum_aux2 (x : Π i, ⨁ (j : κ i), M i j) (i : ι) (p : Π i, κ i)
+    (a : ⨁ (j : κ i), M i j) :
+    (fun j ↦ (update x i a j) (p j)) = update (fun j ↦ x j (p j)) i (a (p i)) := by
+  ext j
+  by_cases h : j =i
+  · rw [h]; simp only [update_same]
+  · simp only [ne_eq, h, not_false_eq_true, update_noteq]
+
+/-- Given a family indexed by `p : Π i : ι, κ i` of multilinear maps on the
+`fun i ↦ M i (p i)`, construct a multilinear map on `fun i ↦ ⨁ j : κ i, M i j`.-/
+def fromDirectSum (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M') :
+    MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M' where
+  toFun x := ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i))
+  map_add' x i a b := by
+    simp only
+    rename_i myinst _ _ _ _ _ _ _
+    conv_lhs => rw [← Finset.sum_union_eq_right (s₁ := @Fintype.piFinset _ myinst _ _
+        (fun j ↦ (update x i a j).support)
+        ∪ @Fintype.piFinset _ myinst _ _ (fun j ↦ (update x i b j).support))
+        (fun p _ hp ↦ by
+          letI := myinst
+          exact fromDirectSum_aux1 _ _ f _ hp)]
+    rw [Finset.sum_congr rfl (fun p _ ↦ by rw [fromDirectSum_aux2 _ _ _ p (a + b)])]
+    erw [Finset.sum_congr rfl (fun p _ ↦ (f p).map_add _ i (a (p i)) (b (p i)))]
+    rw [Finset.sum_add_distrib]
+    congr 1
+    · conv_lhs => rw [← Finset.sum_congr rfl (fun p _ ↦ by rw [← fromDirectSum_aux2 _ _ _ p a]),
+                    Finset.sum_congr (Finset.union_assoc _ _ _) (fun _ _ ↦ rfl)]
+      rw [Finset.sum_union_eq_left (fun p _ hp ↦ by
+        letI := myinst
+        exact fromDirectSum_aux1 _ _ f _ hp)]
+    · conv_lhs => rw [← Finset.sum_congr rfl (fun p _ ↦ by rw [← fromDirectSum_aux2 _ _ _ p b]),
+        Finset.sum_congr (Finset.union_assoc _ _ _) (fun _ _ ↦ rfl),
+        Finset.sum_congr (Finset.union_comm _ _) (fun _ _ ↦ rfl),
+        Finset.sum_congr (Finset.union_assoc _ _ _) (fun _ _ ↦ rfl)]
+      rw [Finset.sum_union_eq_left (fun p _ hp ↦ by
+        letI := myinst
+        exact fromDirectSum_aux1 _ _ f _ hp)]
+  map_smul' x i c a := by
+    simp only
+    rename_i myinst _ _ _ _ _ _ _
+    conv_lhs => rw [← Finset.sum_union_eq_right (s₁ := @Fintype.piFinset _ myinst _ _
+      (fun j ↦ (update x i a j).support))
+        (fun p _ hp ↦ by
+          letI := myinst
+          exact fromDirectSum_aux1 _ _ f _ hp),
+      Finset.sum_congr rfl (fun p _ ↦ by rw [fromDirectSum_aux2 _ _ _ p _])]
+    erw [Finset.sum_congr rfl (fun p _ ↦ (f p).map_smul _ i c (a (p i)))]
+    rw [← Finset.smul_sum]
+    conv_lhs => rw [← Finset.sum_congr rfl (fun p _ ↦ by rw [← fromDirectSum_aux2 _ _ _ p _]),
+      Finset.sum_union_eq_left (fun p _ hp ↦ by
+          letI := myinst
+          exact fromDirectSum_aux1 _ _ f _ hp)]
+
+@[simp]
+theorem fromDirectSum_apply (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M')
+    (x : Π i, ⨁ (j : κ i), M i j) : fromDirectSum R κ f x =
+    ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) := rfl
+
+/-- The construction `MultilinearMap.fromDirectSum`, as an `R`-linear map.-/
+def fromDirectSumₗ : ((p : Π i, κ i) → MultilinearMap R (fun i ↦ M i (p i)) M') →ₗ[R]
+    MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M' where
+  toFun := fromDirectSum R κ
+  map_add' f g := by
+    ext x
+    simp only [fromDirectSum_apply, Pi.add_apply, MultilinearMap.add_apply]
+    rw [Finset.sum_add_distrib]
+  map_smul' c f := by
+    ext x
+    simp only [fromDirectSum_apply, Pi.smul_apply, MultilinearMap.smul_apply, RingHom.id_apply]
+    rw [Finset.smul_sum]
+
+@[simp]
+theorem fromDirectSumₗ_apply (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M')
+    (x : Π i, ⨁ (j : κ i), M i j) : fromDirectSumₗ R κ f x =
+    ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) := rfl
+
+theorem _root_.piFinset_support_lof_sub (p : Π i, κ i) (a : Π i, M i (p i)) :
+    Fintype.piFinset (fun i ↦ DFinsupp.support (lof R (κ i) (M i) (p i) (a i))) ⊆ {p} := by
+  intro q
+  simp only [Fintype.mem_piFinset, ne_eq, Finset.mem_singleton]
+  simp_rw [DirectSum.lof_eq_of]
+  exact fun hq ↦ funext fun i ↦ Finset.mem_singleton.mp (DirectSum.support_of_subset _ (hq i))
+
+/-- The linear equivalence between families indexed by `p : Π i : ι, κ i` of multilinear maps
+on the `fun i ↦ M i (p i)` and the space of multilinear map on `fun i ↦ ⨁ j : κ i, M i j`.-/
+def fromDirectSumEquiv : ((p : Π i, κ i) → MultilinearMap R (fun i ↦ M i (p i)) M') ≃ₗ[R]
+    MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M' := by
+  refine LinearEquiv.ofLinear (fromDirectSumₗ R κ) (LinearMap.pi
+    (fun p ↦ MultilinearMap.compLinearMapₗ (fun i ↦ DirectSum.lof R (κ i) _ (p i)))) ?_ ?_
+  · ext f x
+    simp only [coe_comp, Function.comp_apply, fromDirectSumₗ_apply, pi_apply,
+      MultilinearMap.compLinearMapₗ_apply, MultilinearMap.compLinearMap_apply, id_coe, id_eq]
+    change _ = f (fun i ↦ x i)
+    rw [funext (fun i ↦ Eq.symm (DirectSum.sum_support_of (fun j ↦ M i j) (x i)))]
+    rw [MultilinearMap.map_sum_finset]
+    rfl
+  · ext f p a
+    simp only [coe_comp, Function.comp_apply, LinearMap.pi_apply, compLinearMapₗ_apply,
+      compLinearMap_apply, fromDirectSumₗ_apply, id_coe, id_eq]
+    rw [Finset.sum_subset (piFinset_support_lof_sub R κ p a)]
+    · rw [Finset.sum_singleton]
+      simp only [lof_apply]
+    · simp only [Finset.mem_singleton, Fintype.mem_piFinset, DFinsupp.mem_support_toFun, ne_eq,
+        not_forall, not_not, forall_exists_index, forall_eq, lof_apply]
+      intro i hi
+      exact (f p).map_coord_zero i hi
+
+@[simp]
+theorem fromDirectSumEquiv_apply (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) M')
+    (x : Π i, ⨁ (j : κ i), M i j) : fromDirectSumEquiv R κ f x =
+    ∑ p in Fintype.piFinset (fun i ↦ (x i).support), f p (fun i ↦ x i (p i)) := rfl
+
+@[simp]
+theorem fromDirectSumEquiv_symm_apply (f : MultilinearMap R (fun i ↦ ⨁ j : κ i, M i j) M')
+    (p : Π i, κ i) : (fromDirectSumEquiv R κ).symm f p =
+    f.compLinearMap (fun i ↦ DirectSum.lof R (κ i) _ (p i)) := rfl
+
+end MultilinearMap