added framework for uncurrySum proofs + def uncurrySum

DeRhamCohomology/ContinuousAlternatingMap/Curry.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Analysis.NormedSpace.Alternating.Basic
+import Mathlib.LinearAlgebra.Alternating.DomCoprod
 import DeRhamCohomology.AlternatingMap.Curry
 import DeRhamCohomology.Multilinear.Curry
 import DeRhamCohomology.Alternating.Basic
@@ -84,8 +85,104 @@ theorem uncurryFin_uncurryFinCLM_comp_of_symmetric {f : E →L[𝕜] E →L[𝕜
     Fin.succAbove_succAbove_predAbove, Fin.neg_one_pow_succAbove_add_predAbove, pow_succ',
     neg_one_mul, neg_smul, Fin.removeNth_apply, add_neg_cancel]
 
-def uncurrySum (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) : E [⋀^ι ⊕ ι']→L[𝕜] F := sorry
-  #check ContinuousMultilinearMap.uncurrySum
+
+variable [DecidableEq ι] [DecidableEq ι']
+
+/-- summand used in `ContinuousAlternatingMap.uncurrySum` -/
+-- Current try with separate inputs, to put together in uncurrySum
+def uncurrySum.summand (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) (σ : Equiv.Perm.ModSumCongr ι ι') :
+    ContinuousMultilinearMap 𝕜 (fun _ : ι ⊕ ι' => E) F := sorry
+  /- Want to be able to use a proof similar to below, but need `flip` -/
+  -- Quotient.liftOn' σ
+  --   (fun σ =>
+  --     Equiv.Perm.sign σ •
+  --       (ContinuousMultilinearMap.uncurrySum `(flip to go from f Alternating to Multilinear)`
+  --         : ContinuousMultilinearMap 𝕜 (fun _ => E) (F)).domDomCongr σ)
+  --   fun σ₁ σ₂ H => by
+  --   rw [QuotientGroup.leftRel_apply] at H
+  --   obtain ⟨⟨sl, sr⟩, h⟩ := H
+  --   ext v
+  --   simp only [MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply,
+  --     coe_multilinearMap, MultilinearMap.smul_apply]
+  --   replace h := inv_mul_eq_iff_eq_mul.mp h.symm
+  --   have : Equiv.Perm.sign (σ₁ * Perm.sumCongrHom _ _ (sl, sr))
+  --     = Equiv.Perm.sign σ₁ * (Equiv.Perm.sign sl * Equiv.Perm.sign sr) := by simp
+  --   rw [h, this, mul_smul, mul_smul, smul_left_cancel_iff, ← TensorProduct.tmul_smul,
+  --     TensorProduct.smul_tmul']
+  --   simp only [Sum.map_inr, Perm.sumCongrHom_apply, Perm.sumCongr_apply, Sum.map_inl,
+  --     Function.comp_apply, Perm.coe_mul]
+  --   erw [← a.map_congr_perm fun i => v (σ₁ _), ← b.map_congr_perm fun i => v (σ₁ _)]
+
+/-- Swapping elements in `σ` with equal values in `v` results in an addition that cancels -/
+theorem uncurrySum.summand_add_swap_smul_eq_zero (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F)
+    (σ : Equiv.Perm.ModSumCongr ι ι') {v : ι ⊕ ι' → E}
+    {i j : ι ⊕ ι'} (hv : v i = v j) (hij : i ≠ j) :
+    uncurrySum.summand f σ v + uncurrySum.summand f (Equiv.swap i j • σ) v = 0 := sorry
+  /- Want to use a proof similar to below, but need `uncurrySum.summand` defined first -/
+  -- refine Quotient.inductionOn' σ fun σ => ?_
+  -- dsimp only [Quotient.liftOn'_mk'', Quotient.map'_mk'', MulAction.Quotient.smul_mk,
+  --   uncurrySum.summand]
+  -- rw [smul_eq_mul, Perm.sign_mul, Perm.sign_swap hij]
+  -- simp only [one_mul, neg_mul, Function.comp_apply, Units.neg_smul, Perm.coe_mul, Units.val_neg,
+  --   MultilinearMap.smul_apply, MultilinearMap.neg_apply, MultilinearMap.domDomCongr_apply,
+  --   MultilinearMap.domCoprod_apply]
+  -- convert add_neg_cancel (G := F) _ using 6 <;>
+  --   · ext k
+  --     rw [Equiv.apply_swap_eq_self hv]
+
+/-- Swapping elements in `σ` with equal values in `v` result in zero if the swap has no effect
+on the quotient. -/
+theorem uncurrySum.summand_eq_zero_of_smul_invariant (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F)
+    (σ : Equiv.Perm.ModSumCongr ι ι') {v : ι ⊕ ι' → E}
+    {i j : ι ⊕ ι'} (hv : v i = v j) (hij : i ≠ j) :
+    Equiv.swap i j • σ = σ → uncurrySum.summand f σ v = 0 := sorry
+  /- Want to use a proof similar to below, but need `uncurrySum.summand` first-/
+  -- refine Quotient.inductionOn' σ fun σ => ?_
+  -- dsimp only [Quotient.liftOn'_mk'', Quotient.map'_mk'', MultilinearMap.smul_apply,
+  --   MultilinearMap.domDomCongr_apply, MultilinearMap.domCoprod_apply, domCoprod.summand]
+  -- intro hσ
+  -- cases' hi : σ⁻¹ i with val val <;> cases' hj : σ⁻¹ j with val_1 val_1 <;>
+  --   rw [Perm.inv_eq_iff_eq] at hi hj <;> substs hi hj <;> revert val val_1
+  -- -- Porting note: `on_goal` is not available in `case _ | _ =>`, so the proof gets tedious.
+  -- -- the term pairs with and cancels another term
+  -- case inl.inr =>
+  --   intro i' j' _ _ hσ
+  --   obtain ⟨⟨sl, sr⟩, hσ⟩ := QuotientGroup.leftRel_apply.mp (Quotient.exact' hσ)
+  --   replace hσ := Equiv.congr_fun hσ (Sum.inl i')
+  --   dsimp only at hσ
+  --   rw [smul_eq_mul, ← mul_swap_eq_swap_mul, mul_inv_rev, swap_inv, inv_mul_cancel_right] at hσ
+  --   simp at hσ
+  -- case inr.inl =>
+  --   intro i' j' _ _ hσ
+  --   obtain ⟨⟨sl, sr⟩, hσ⟩ := QuotientGroup.leftRel_apply.mp (Quotient.exact' hσ)
+  --   replace hσ := Equiv.congr_fun hσ (Sum.inr i')
+  --   dsimp only at hσ
+  --   rw [smul_eq_mul, ← mul_swap_eq_swap_mul, mul_inv_rev, swap_inv, inv_mul_cancel_right] at hσ
+  --   simp at hσ
+  -- -- the term does not pair but is zero
+  -- case inr.inr =>
+  --   intro i' j' hv hij _
+  --   convert smul_zero (M := ℤˣ) (A := N₁ ⊗[R'] N₂) _
+  --   convert TensorProduct.tmul_zero (R := R') (M := N₁) N₂ _
+  --   exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)
+  -- case inl.inl =>
+  --   intro i' j' hv hij _
+  --   convert smul_zero (M := ℤˣ) (A := N₁ ⊗[R'] N₂) _
+  --   convert TensorProduct.zero_tmul (R := R') N₁ (N := N₂) _
+  --   exact AlternatingMap.map_eq_zero_of_eq _ _ hv fun hij' => hij (hij' ▸ rfl)
+
+def uncurrySum (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) : E [⋀^ι ⊕ ι']→L[𝕜] F :=
+    { ∑ σ : Equiv.Perm.ModSumCongr ι ι', uncurrySum.summand f σ with
+    toFun := fun v => (⇑(∑ σ : Equiv.Perm.ModSumCongr ι ι', uncurrySum.summand f σ)) v
+    map_eq_zero_of_eq' := fun v i j hv hij => by
+      dsimp only
+      rw [ContinuousMultilinearMap.sum_apply]
+      exact
+        Finset.sum_involution (fun σ _ => Equiv.swap i j • σ)
+          (fun σ _ => uncurrySum.summand_add_swap_smul_eq_zero f σ hv hij)
+          (fun σ _ => mt <| uncurrySum.summand_eq_zero_of_smul_invariant f σ hv hij)
+          (fun σ _ => Finset.mem_univ _) fun σ _ =>
+          Equiv.swap_smul_involutive i j σ }
 
 def uncurryFinAdd (f : E [⋀^Fin m]→L[𝕜] E [⋀^Fin n]→L[𝕜] F) :
     E [⋀^Fin (m + n)]→L[𝕜] F :=

DeRhamCohomology/Multilinear/Curry.lean

@@ -13,7 +13,8 @@ variable
   {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
   {F : Type*} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
 
-def uncurrySum  (a : ContinuousMultilinearMap 𝕜 (fun _ : ι => E)
+@[simps apply]
+def uncurrySum (a : ContinuousMultilinearMap 𝕜 (fun _ : ι => E)
     (ContinuousMultilinearMap 𝕜 (fun _ : ι' => E) F)) :
     ContinuousMultilinearMap 𝕜 (fun _ : ι ⊕ ι' => E) F where
   toFun v := a (fun i => v (Sum.inl i)) (fun j => v (Sum.inr j))