From c99541eb5c4ddd98a017c2e841e11c9b22eb7ff7 Mon Sep 17 00:00:00 2001
From: MetalCreator666 <57985847+MetalCreator666@users.noreply.github.com>
Date: Fri, 17 Jan 2025 11:36:46 +0100
Subject: [PATCH] Addd some functionality

---
 DeRhamCohomology/ContinuousAlternatingMap/Curry.lean | 12 ++++++++++++
 DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean | 11 +++++++++--
 2 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean b/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
index 9860570..ba2d8be 100644
--- a/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
+++ b/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
@@ -130,6 +130,13 @@ def uncurrySum.summand (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) (σ :
       simp [ContinuousMultilinearMap.flipAlternating]
       rfl
 
+theorem uncurrySum.summand_mk'' (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) (σ : Equiv.Perm (ι ⊕ ι')) :
+    uncurrySum.summand f (Quotient.mk'' σ) = Equiv.Perm.sign σ •
+      (ContinuousMultilinearMap.uncurrySum
+        (f.toContinuousMultilinearMap.flipAlternating.toContinuousMultilinearMap.flipMultilinear) :
+          ContinuousMultilinearMap 𝕜 (fun _ => E) F).domDomCongr σ :=
+  rfl
+
 /-- 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}
@@ -198,6 +205,11 @@ def uncurrySum (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) : E [⋀^ι 
           (fun σ _ => Finset.mem_univ _) fun σ _ =>
           Equiv.swap_smul_involutive i j σ }
 
+theorem uncurrySum_coe (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) :
+    ((uncurrySum f).toContinuousMultilinearMap : ContinuousMultilinearMap 𝕜 (fun _ => E) F) =
+      ∑ σ : Equiv.Perm.ModSumCongr ι ι', uncurrySum.summand f σ :=
+  ContinuousMultilinearMap.ext fun _ => rfl
+
 def uncurryFinAdd (f : E [⋀^Fin m]→L[𝕜] E [⋀^Fin n]→L[𝕜] F) :
     E [⋀^Fin (m + n)]→L[𝕜] F :=
   ContinuousAlternatingMap.domDomCongr finSumFinEquiv (uncurrySum f)
diff --git a/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean b/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean
index 789a25a..e20704d 100644
--- a/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean
+++ b/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean
@@ -49,11 +49,18 @@ theorem wedge_product_lsmul {g : M [⋀^Fin m]→L[𝕜] 𝕜} {h : M [⋀^Fin n
 /- Associativity of wedge product -/
 theorem wedge_assoc (g : M [⋀^Fin m]→L[𝕜] N) (h : M [⋀^Fin n]→L[𝕜] N) (f : N →L[𝕜] N →L[𝕜] N)
     (l : M [⋀^Fin p]→L[𝕜] N) (f' : N →L[𝕜] N →L[𝕜] N) :
-    ContinuousAlternatingMap.domDomCongr finAssoc.symm (g ∧[f] h ∧[f'] l) = ((g ∧[f] h) ∧[f'] l) := by sorry
+    ContinuousAlternatingMap.domDomCongr finAssoc.symm (g ∧[f] h ∧[f'] l) = ((g ∧[f] h) ∧[f'] l) := by
+  rw[wedge_product, ContinuousLinearMap.compContinuousAlternatingMap₂, uncurryFinAdd,
+    uncurrySum, ContinuousAlternatingMap.ext_iff]
+  intro x
+  sorry
 
 /- Left distributivity of wedge product -/
 theorem add_wedge (g₁ g₂ : M [⋀^Fin m]→L[𝕜] N) (h : M [⋀^Fin n]→L[𝕜] N') (f : N →L[𝕜] N' →L[𝕜] N'') :
-    ((g₁ + g₂) ∧[f] h) = (g₁ ∧[f] h) + (g₂ ∧[f] h) := by sorry
+    ((g₁ + g₂) ∧[f] h) = (g₁ ∧[f] h) + (g₂ ∧[f] h) := by
+  ext x
+  sorry
+
 
 /- Right distributivity of wedge product -/
 theorem wedge_add (g : M [⋀^Fin m]→L[𝕜] N) (h₁ h₂ : M [⋀^Fin n]→L[𝕜] N') (f : N →L[𝕜] N' →L[𝕜] N'') :