Proven smul_wedge

urkud · Jan 22, 2025 · e65825c · e65825c
1 parent dfdbddb
commit e65825c
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 1 deletion.
diff --git a/DeRhamCohomology/Alternating/Basic.lean b/DeRhamCohomology/Alternating/Basic.lean
@@ -78,6 +78,10 @@ def flipAlternating (f : ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ M) (M' [
       map_eq_zero_of_eq' := sorry }
     1 sorry
 
+theorem flipAlternating_apply (f : ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ M) (M' [⋀^ι']→L[𝕜] N))
+    (m : ι → M) (m' : ι' → M') : flipAlternating f m' m = f m m' :=
+  rfl
+
 end ContinuousMultilinearMap
 
 namespace ContinuousAlternatingMap

diff --git a/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean b/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
@@ -130,6 +130,14 @@ 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 (Quot.mk
+      (⇑(QuotientGroup.leftRel (Equiv.Perm.sumCongrHom ι ι').range)) σ) = Equiv.Perm.sign σ •
+        (ContinuousMultilinearMap.uncurrySum
+          (f.toContinuousMultilinearMap.flipAlternating.toContinuousMultilinearMap.flipMultilinear) :
+            ContinuousMultilinearMap 𝕜 (fun _ => E) F).domDomCongr σ :=
+  rfl
+
 theorem uncurrySum.summand_mk'' (f : E [⋀^ι]→L[𝕜] E [⋀^ι']→L[𝕜] F) (σ : Equiv.Perm (ι ⊕ ι')) :
     uncurrySum.summand f (Quotient.mk'' σ) = Equiv.Perm.sign σ •
       (ContinuousMultilinearMap.uncurrySum

diff --git a/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean b/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean
@@ -71,7 +71,22 @@ theorem smul_wedge (g : M [⋀^Fin m]→L[𝕜] 𝕜) (h : M [⋀^Fin n]→L[
     ContinuousMultilinearMap.sum_apply, Finset.smul_sum]
   rw[wedge_product_def, uncurryFinAdd, domDomCongr_apply, uncurrySum_apply,
     ContinuousMultilinearMap.sum_apply]
-  sorry
+  apply Finset.sum_congr rfl
+  intro σ hσ
+  rcases σ with ⟨σ₁⟩
+  rw[uncurrySum.summand_mk]
+  simp only [ContinuousMultilinearMap.smul_apply, ContinuousMultilinearMap.domDomCongr_apply,
+    Function.comp_apply, ContinuousMultilinearMap.uncurrySum_apply, ContinuousMultilinearMap.flipMultilinear_apply,
+    coe_toContinuousMultilinearMap, ContinuousMultilinearMap.flipAlternating_apply,
+    ContinuousLinearMap.compContinuousAlternatingMap₂_apply, ContinuousLinearMap.mul_apply', ← smul_assoc,
+    smul_comm]
+  rw[smul_assoc, smul_eq_mul, ← mul_assoc]
+  rw[uncurrySum.summand_mk]
+  simp only [ContinuousMultilinearMap.smul_apply, ContinuousMultilinearMap.domDomCongr_apply,
+    Function.comp_apply, ContinuousMultilinearMap.uncurrySum_apply, ContinuousMultilinearMap.flipMultilinear_apply,
+    coe_toContinuousMultilinearMap, ContinuousMultilinearMap.flipAlternating_apply,
+    ContinuousLinearMap.compContinuousAlternatingMap₂_apply, ContinuousLinearMap.mul_apply', ← smul_assoc,
+    smul_comm, smul_apply, smul_eq_mul]
 
 theorem wedge_smul (g : M [⋀^Fin m]→L[𝕜] 𝕜) (h : M [⋀^Fin n]→L[𝕜] 𝕜) (c : 𝕜) :
     c • (g ∧[𝕜] h) = g ∧[𝕜] (c • h) := by

diff --git a/DeRhamCohomology/Multilinear/Basic.lean b/DeRhamCohomology/Multilinear/Basic.lean
@@ -100,3 +100,8 @@ def flipMultilinear (f : ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ M) (Conti
       map_update_add' := sorry
       map_update_smul' := sorry }
     1 sorry
+
+theorem flipMultilinear_apply (f : ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ M)
+    (ContinuousMultilinearMap 𝕜 (fun _ : ι' ↦ M') N)) (m : ι → M) (m' : ι' → M') :
+    f.flipMultilinear m' m = f m m' :=
+  rfl