Added apply functionality, tried proving properties wedge product

DeRhamCohomology/Alternating/Basic.lean

@@ -1,6 +1,7 @@
 import Mathlib.Topology.Algebra.Module.Basic
 import Mathlib.Topology.Algebra.Module.Alternating.Basic
 import Mathlib.Analysis.NormedSpace.Alternating.Basic
+import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
 
 noncomputable section
 suppress_compilation
@@ -41,6 +42,16 @@ theorem compContinuousAlternatingMap₂_apply (f : N →L[𝕜] N' →L[𝕜] N'
     f.compContinuousAlternatingMap₂ g h m m' = f (g m) (h m') :=
   rfl
 
+theorem compContinuousAlternatingMap₂_mul_apply
+    (g : M [⋀^ι]→L[𝕜] 𝕜) (h : M' [⋀^ι']→L[𝕜] 𝕜) (m : ι → M) (m': ι' → M') :
+    (ContinuousLinearMap.mul 𝕜 𝕜).compContinuousAlternatingMap₂ g h m m' = (g m) * (h m') :=
+  rfl
+
+theorem compContinuousAlternatingMap₂_lsmul_apply
+    (g : M [⋀^ι]→L[𝕜] 𝕜) (h : M' [⋀^ι']→L[𝕜] N) (m : ι → M) (m': ι' → M') :
+    (ContinuousLinearMap.lsmul 𝕜 𝕜).compContinuousAlternatingMap₂ g h m m' = (g m) • (h m') :=
+  rfl
+
 end ContinuousLinearMap
 
 namespace ContinuousMultilinearMap
@@ -85,6 +96,10 @@ def domDomCongr (σ : ι ≃ ι') (f : M [⋀^ι]→L[𝕜] N) : M [⋀^ι']→L
       f.map_eq_zero_of_eq (v ∘ σ) (i := σ.symm i) (j := σ.symm j)
         (by simpa using hv) (σ.symm.injective.ne hij) }
 
+theorem domDomCongr_apply (σ : ι ≃ ι') (f : M [⋀^ι]→L[𝕜] N) (v : ι' → M) :
+    (domDomCongr σ f) v = f (v ∘ σ) :=
+  rfl
+
 variable
   {M' : Type*} [NormedAddCommGroup M'] [NormedSpace 𝕜 M']
   [Fintype ι] [Fintype ι']

DeRhamCohomology/ContinuousAlternatingMap/Curry.lean

@@ -210,6 +210,10 @@ theorem uncurrySum_coe (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) :
       ∑ σ : Equiv.Perm.ModSumCongr ι ι', uncurrySum.summand f σ :=
   ContinuousMultilinearMap.ext fun _ => rfl
 
+theorem uncurrySum_apply (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) (m : ι ⊕ ι' → E) :
+    uncurrySum f m = (∑ σ : Equiv.Perm.ModSumCongr ι ι', uncurrySum.summand f σ) m :=
+  rfl
+
 def uncurryFinAdd (f : E [⋀^Fin m]→L[𝕜] E [⋀^Fin n]→L[𝕜] F) :
     E [⋀^Fin (m + n)]→L[𝕜] F :=
   ContinuousAlternatingMap.domDomCongr finSumFinEquiv (uncurrySum f)

DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean

@@ -3,6 +3,8 @@ import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
 import DeRhamCohomology.ContinuousAlternatingMap.Curry
 import DeRhamCohomology.Alternating.Basic
 import DeRhamCohomology.Equiv.Fin
+import Mathlib.Algebra.GroupWithZero.Defs
+import Init.Grind.Lemmas
 
 noncomputable section
 suppress_compilation
@@ -61,25 +63,46 @@ theorem add_wedge (g₁ g₂ : M [⋀^Fin m]→L[𝕜] N) (h : M [⋀^Fin n]→L
   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'') :
     (g ∧[f] (h₁ + h₂)) = (g ∧[f] h₁) + (g ∧[f] h₂) := by sorry
 
-theorem smul_wedge (g : M [⋀^Fin m]→L[𝕜] N) (h : M [⋀^Fin n]→L[𝕜] N') (f : N →L[𝕜] N' →L[𝕜] N'') (c : 𝕜) :
-    c • (g ∧[f] h) = (c • g) ∧[f] h := by sorry
+theorem smul_wedge (g : M [⋀^Fin m]→L[𝕜] 𝕜) (h : M [⋀^Fin n]→L[𝕜] 𝕜) (c : 𝕜) :
+    c • (g ∧[𝕜] h) = (c • g) ∧[𝕜] h := by
+  ext x
+  rw[smul_apply, wedge_product_def, uncurryFinAdd, domDomCongr_apply, uncurrySum_apply,
+    ContinuousMultilinearMap.sum_apply, Finset.smul_sum]
+  rw[wedge_product_def, uncurryFinAdd, domDomCongr_apply, uncurrySum_apply,
+    ContinuousMultilinearMap.sum_apply]
+  sorry
 
-theorem wedge_smul (g : M [⋀^Fin m]→L[𝕜] N) (h : M [⋀^Fin n]→L[𝕜] N') (f : N →L[𝕜] N' →L[𝕜] N'') (c : 𝕜) :
-    c • (g ∧[f] h) = g ∧[f] (c • h) := by sorry
+theorem wedge_smul (g : M [⋀^Fin m]→L[𝕜] 𝕜) (h : M [⋀^Fin n]→L[𝕜] 𝕜) (c : 𝕜) :
+    c • (g ∧[𝕜] h) = g ∧[𝕜] (c • h) := by
+  ext x
+  rw[smul_apply, wedge_product_def, uncurryFinAdd, domDomCongr_apply, uncurrySum_apply,
+    ContinuousMultilinearMap.sum_apply, Finset.smul_sum]
+  rw[wedge_product_def, uncurryFinAdd, domDomCongr_apply, uncurrySum_apply,
+    ContinuousMultilinearMap.sum_apply]
+  sorry
 
 /- Antisymmetry of multiplication wedge product -/
-theorem wedge_antisymm (g : M [⋀^Fin m]→L[𝕜] 𝕜) (h : M [⋀^Fin n]→L[𝕜] 𝕜) :
-    (g ∧[𝕜] h) = domDomCongr finAddFlip ((-1)^(m*n) • (h ∧[𝕜] g)) := by sorry
+theorem wedge_antisymm (g : M [⋀^Fin m]→L[𝕜] 𝕜) (h : M [⋀^Fin n]→L[𝕜] 𝕜) (x : Fin (m + n) → M) :
+    (g ∧[𝕜] h) x = domDomCongr finAddFlip ((-1)^(m*n) • (h ∧[𝕜] g)) x := by sorry
 
 theorem wedge_self_odd_zero (g : M [⋀^Fin m]→L[𝕜] 𝕜) (m_odd : Odd m) :
     (g ∧[𝕜] g) = 0 := by
-  let h := wedge_antisymm g g
-  rw[Odd.neg_one_pow (Odd.mul m_odd m_odd)] at h
+  ext x
+  let h := wedge_antisymm g g x
+  rw[Odd.neg_one_pow (Odd.mul m_odd m_odd), domDomCongr_apply, smul_apply] at h
+  have h1 : (g∧[ContinuousLinearMap.mul 𝕜 𝕜]g) x =
+    (g∧[ContinuousLinearMap.mul 𝕜 𝕜]g) (x ∘ ⇑finAddFlip) := by sorry
+  rw[← h1] at h
+  simp only [coe_zero, Pi.zero_apply]
+  have h2 : 2 * (g∧[ContinuousLinearMap.mul 𝕜 𝕜]g) x = 0 := by sorry
+  apply mul_eq_zero.mp at h2
+
+  #check Mathlib.Tactic.CC.or_eq_of_eq_false_left
+
   sorry
 
 end wedge