Definitions Wedge product for differential forms + mul/lsmul

urkud · Jan 13, 2025 · bcdd3b2 · bcdd3b2
1 parent 3c623e8
commit bcdd3b2
Show file tree

Hide file tree

Showing 2 changed files with 36 additions and 2 deletions.
diff --git a/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean b/DeRhamCohomology/ContinuousAlternatingMap/Wedge.lean
@@ -32,4 +32,14 @@ theorem wedge_product_def {g : M [⋀^Fin m]→L[𝕜] N} {h : M [⋀^Fin n]→L
     (f ∧ [g, h]) x = uncurryFinAdd (f.compContinuousAlternatingMap₂ g h) x :=
   rfl
 
+/- The wedge product wrt multiplication -/
+theorem wedge_product_mul {g : M [⋀^Fin m]→L[𝕜] 𝕜} {h : M [⋀^Fin n]→L[𝕜] 𝕜} {x : Fin (m + n) → M} :
+    (ContinuousLinearMap.mul 𝕜 𝕜 ∧ [g, h]) x = uncurryFinAdd ((ContinuousLinearMap.mul 𝕜 𝕜).compContinuousAlternatingMap₂ g h) x :=
+  rfl
+
+/- The wedge product wrt scalar multiplication -/
+theorem wedge_product_lsmul {g : M [⋀^Fin m]→L[𝕜] 𝕜} {h : M [⋀^Fin n]→L[𝕜] N} {x : Fin (m + n) → M} :
+    (ContinuousLinearMap.lsmul 𝕜 𝕜 ∧ [g, h]) x = uncurryFinAdd ((ContinuousLinearMap.lsmul 𝕜 𝕜).compContinuousAlternatingMap₂ g h) x :=
+  rfl
+
 end wedge
diff --git a/DeRhamCohomology/DifferentialForm.lean b/DeRhamCohomology/DifferentialForm.lean
@@ -8,8 +8,11 @@ noncomputable section
 open Filter ContinuousAlternatingMap
 open scoped Topology
 
-variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  [NormedAddCommGroup F] [NormedSpace ℝ F] {n m : ℕ}
+variable {E F F' F'' : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [NormedAddCommGroup F] [NormedSpace ℝ F]
+  [NormedAddCommGroup F'] [NormedSpace ℝ F']
+  [NormedAddCommGroup F''] [NormedSpace ℝ F'']
+  {n m : ℕ}
 
 -- TODO: change notation
 notation "Ω^" n "⟮" E ", " F "⟯" => E → E [⋀^Fin n]→L[ℝ] F
@@ -44,3 +47,24 @@ theorem ederiv_ederiv_apply (ω : Ω^n⟮E, F⟯) {x} (h : ContDiffAt ℝ 2 ω x
 
 theorem ederiv_ederiv (ω : Ω^n⟮E, F⟯) (h : ContDiff ℝ 2 ω) : ederiv (ederiv ω) = 0 :=
   funext fun _ ↦ ederiv_ederiv_apply ω h.contDiffAt
+
+/- Wedge product of differential forms -/
+def wedge_product (ω₁ : Ω^m⟮E, F⟯) (ω₂ : Ω^n⟮E, F'⟯) (f : F →L[ℝ] F' →L[ℝ] F'') :
+    Ω^(m + n)⟮E, F''⟯ := fun e => ContinuousAlternatingMap.wedge_product (ω₁ e) (ω₂ e) f
+
+-- TODO: change notation
+notation f "∧" "[" ω₁ "," ω₂ "]" => wedge_product ω₁ ω₂ f
+
+theorem wedge_product_def {ω₁ : Ω^m⟮E, F⟯} {ω₂ : Ω^n⟮E, F'⟯} {f : F →L[ℝ] F' →L[ℝ] F''}
+    {x : E} : (f ∧ [ω₁, ω₂]) x = ContinuousAlternatingMap.wedge_product (ω₁ x) (ω₂ x) f :=
+  rfl
+
+/- The wedge product wrt multiplication -/
+theorem wedge_product_mul {ω₁ : Ω^m⟮E, ℝ⟯} {ω₂ : Ω^n⟮E, ℝ⟯} {x : E} :
+    (ContinuousLinearMap.mul ℝ ℝ ∧ [ω₁, ω₂]) x = ContinuousAlternatingMap.wedge_product (ω₁ x) (ω₂ x) (ContinuousLinearMap.mul ℝ ℝ) :=
+  rfl
+
+/- The wedge product wrt scalar multiplication -/
+theorem wedge_product_lsmul {ω₁ : Ω^m⟮E, ℝ⟯} {ω₂ : Ω^n⟮E, F⟯} {x : E} :
+    (ContinuousLinearMap.lsmul ℝ ℝ ∧ [ω₁, ω₂]) x = ContinuousAlternatingMap.wedge_product (ω₁ x) (ω₂ x) (ContinuousLinearMap.lsmul ℝ ℝ) :=
+  rfl