feat(LinearAlgebra/PiTensorProduct): add version of subsingletonEquiv for dependent case (#32598)

Dependent `PiTensorProduct`s over singleton types occur naturally when
using `tmulEquivDep` to split off one index from a dependent
`PiTensorProduct`. This PR creates `subsingletonEquivDep` to deal with
this situation.

The non-dependent `subsingletonEquiv` is re-defined as a specialization
of the general case. This changes the definition of `toDirectSum_ι` in
TensorAlgebra/ToTensorPower, and so its proof is therefore changed.

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Co-authored-by: david <david.gross@thp.uni-koeln.de>
Co-authored-by: David Gross <david.gross@thp.uni-koeln.de>

Author: PrParadoxy

Mathlib/LinearAlgebra/PiTensorProduct.lean

@@ -798,33 +798,39 @@ theorem isEmptyEquiv_apply_tprod [IsEmpty ι] (f : Π i, s i) :
 
 variable {ι}
 
-/--
-Tensor product of `M` over a singleton set is equivalent to `M`
--/
-@[simps symm_apply]
-def subsingletonEquiv [Subsingleton ι] (i₀ : ι) : (⨂[R] _ : ι, M) ≃ₗ[R] M where
-  toFun := lift (MultilinearMap.ofSubsingleton R M M i₀ .id)
-  invFun m := tprod R fun _ ↦ m
-  left_inv x := by
-    dsimp only
-    have : ∀ (f : ι → M) (z : M), (fun _ : ι ↦ z) = update f i₀ z := fun f z ↦ by
-      ext i
-      rw [Subsingleton.elim i i₀, Function.update_self]
-    refine x.induction_on ?_ ?_
-    · intro r f
-      simp only [map_smul, LinearMap.id_apply, lift.tprod, ofSubsingleton_apply_apply,
-        this f, MultilinearMap.map_update_smul, update_eq_self]
-    · intro x y hx hy
-      rw [map_add, this 0 (_ + _), MultilinearMap.map_update_add, ← this 0 (lift _ _), hx,
-        ← this 0 (lift _ _), hy]
-  right_inv t := by simp only [ofSubsingleton_apply_apply, LinearMap.id_apply, lift.tprod]
-  map_add' := map_add _
-  map_smul' := map_smul _
+section subsingleton
+
+variable [Subsingleton ι] (i₀ : ι)
+
+/-- Tensor product over a singleton type with element `i₀` is equivalent to `s i₀`. -/
+def subsingletonEquiv : (⨂[R] i : ι, s i) ≃ₗ[R] s i₀ :=
+  LinearEquiv.ofLinear
+    (lift
+      { toFun f := f i₀
+        map_update_add' m i := by rw [Subsingleton.elim i i₀]; simp
+        map_update_smul' m i := by rw [Subsingleton.elim i i₀]; simp })
+    ({ toFun x := tprod R (update (0 : (i : ι) → s i) i₀ x)
+       map_add' := by simp
+       map_smul' := by simp })
+    (by ext _; simp)
+    (by
+      ext f
+      have h : update (0 : (i : ι) → s i) i₀ (f i₀) = f := update_eq_self i₀ f
+      simp [h])
 
 @[simp]
-theorem subsingletonEquiv_apply_tprod [Subsingleton ι] (i : ι) (f : ι → M) :
-    subsingletonEquiv i (tprod R f) = f i :=
-  lift.tprod _
+theorem subsingletonEquiv_apply_tprod (f : (i : ι) → s i) :
+    subsingletonEquiv i₀ (⨂ₜ[R] i, f i) = f i₀ := lift.tprod _
+
+theorem subsingletonEquiv_symm_apply (x : s i₀) :
+    (subsingletonEquiv i₀).symm x = tprod R (fun i ↦ update (0 : (j : ι) → s j) i₀ x i) := rfl
+
+@[simp]
+lemma subsingletonEquiv_symm_apply' (x : M) :
+  (subsingletonEquiv (s := fun _ ↦ M) i₀).symm x = (tprod R fun _ ↦ x) := by
+  simp [LinearEquiv.symm_apply_eq, subsingletonEquiv_apply_tprod]
+
+end subsingleton
 
 variable (R M)
 

Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean

@@ -87,8 +87,8 @@ def toDirectSum : TensorAlgebra R M →ₐ[R] ⨁ n, ⨂[R]^n M :=
 @[simp]
 theorem toDirectSum_ι (x : M) :
     toDirectSum (ι R x) =
-      DirectSum.of (fun n => ⨂[R]^n M) _ (PiTensorProduct.tprod R fun _ : Fin 1 => x) :=
-  TensorAlgebra.lift_ι_apply _ _
+      DirectSum.of (fun n => ⨂[R]^n M) _ (PiTensorProduct.tprod R fun _ : Fin 1 => x) := by
+  simp [toDirectSum, TensorAlgebra.lift_ι_apply, DirectSum.lof_eq_of]
 
 theorem ofDirectSum_comp_toDirectSum :
     ofDirectSum.comp toDirectSum = AlgHom.id R (TensorAlgebra R M) := by