From ab950d065ee8ac7038e4a6113909f6ac610ea33a Mon Sep 17 00:00:00 2001
From: MetalCreator666 <57985847+MetalCreator666@users.noreply.github.com>
Date: Fri, 29 Nov 2024 00:52:02 +0100
Subject: [PATCH 1/5] Initial ideas

---
 .../ContinuousAlternatingMap/Curry.lean       |  4 +++
 DeRhamCohomology/DifferentialForm.lean        | 35 +++++++++++++++++++
 2 files changed, 39 insertions(+)

diff --git a/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean b/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
index a7b612c..084fd3b 100644
--- a/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
+++ b/DeRhamCohomology/ContinuousAlternatingMap/Curry.lean
@@ -19,6 +19,10 @@ variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜]
   [NormedAddCommGroup E] [NormedSpace 𝕜 E]
   [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
+/- `TODO` -/
+def curryFin {n : ℕ} (f : E [⋀^Fin (n + 1)]→L[𝕜] F) :
+    E →L[𝕜] E [⋀^Fin n]→L[𝕜] F := by sorry
+
 def uncurryFin {n : ℕ} (f : E →L[𝕜] (E [⋀^Fin n]→L[𝕜] F)) :
     E [⋀^Fin (n + 1)]→L[𝕜] F :=
   AlternatingMap.mkContinuous
diff --git a/DeRhamCohomology/DifferentialForm.lean b/DeRhamCohomology/DifferentialForm.lean
index 04479d8..625b49b 100644
--- a/DeRhamCohomology/DifferentialForm.lean
+++ b/DeRhamCohomology/DifferentialForm.lean
@@ -1,6 +1,16 @@
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import DeRhamCohomology.ContinuousAlternatingMap.Curry
 
+/-
+# Differential Forms
+
+## Main definitions
+* `DifferentialForm E F n`
+* `extDeriv`
+
+
+-/
+
 noncomputable section
 
 variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
@@ -9,10 +19,35 @@ variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
 variable (E F) in
 def DifferentialForm (n : ℕ) := E → E [⋀^Fin n]→L[ℝ] F
 
+
+variable {v : E}
+
 namespace DifferentialForm
 
+instance : Zero (DifferentialForm E F n) :=
+  ⟨ (fun _ => 0) ⟩
+
+@[simp]
+theorem zero_apply : (0 : DifferentialForm E F n) v = 0 :=
+  rfl
+
+instance inhabited : Inhabited (DifferentialForm E F n) :=
+  ⟨0⟩
+
+/- Application of differential form to vector field -/
+def differentialform_apply_vectorfield {n : ℕ} (ω : DifferentialForm E F (n + 1)) (ξ : E → (Fin 1 → E)) :=
+  fun v ↦ (ω v).curryFin (ξ v 0)
+
+
+
 /-- Exterior derivative of a differential form. -/
 def extDeriv (ω : DifferentialForm E F n) : DifferentialForm E F (n + 1) :=
   fun x ↦ .uncurryFin (fderiv ℝ ω x)
 
+theorem extderiv_comp_extderiv (ω : DifferentialForm E F n) :
+  extDeriv (extDeriv ω) = 0 := by
+    sorry
+
+
+
 end DifferentialForm

From 9da3145ff8235bd8c708dcf7b0d476199a8d8a80 Mon Sep 17 00:00:00 2001
From: MetalCreator666 <57985847+MetalCreator666@users.noreply.github.com>
Date: Fri, 29 Nov 2024 20:27:26 +0100
Subject: [PATCH 2/5] pullback definition + first properties

---
 DeRhamCohomology/DifferentialForm.lean | 76 +++++++++++++++++++++-----
 1 file changed, 61 insertions(+), 15 deletions(-)

diff --git a/DeRhamCohomology/DifferentialForm.lean b/DeRhamCohomology/DifferentialForm.lean
index ac10477..d2b7180 100644
--- a/DeRhamCohomology/DifferentialForm.lean
+++ b/DeRhamCohomology/DifferentialForm.lean
@@ -5,11 +5,6 @@ import DeRhamCohomology.ContinuousAlternatingMap.FDeriv
 /-
 # Differential Forms
 
-## Main definitions
-* `DifferentialForm E F n`
-* `extDeriv`
-
-
 -/
 
 noncomputable section
@@ -17,27 +12,54 @@ noncomputable section
 open Filter ContinuousAlternatingMap
 open scoped Topology
 
-variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
-  [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ}
+variable {E F G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [NormedAddCommGroup F] [NormedSpace ℝ F]
+  [NormedAddCommGroup G] [NormedSpace ℝ G] {n k : ℕ}
 
 -- TODO: change notation
 notation "Ω^" n "⟮" E ", " F "⟯" => E → E [⋀^Fin n]→L[ℝ] F
 
-instance : Zero (DifferentialForm E F n) :=
-  ⟨ (fun _ => 0) ⟩
+variable {v : E}
+variable (ω τ : Ω^n⟮E, F⟯)
+variable (f : E → F)
+
+instance : Add (Ω^n⟮E, F⟯) :=
+  ⟨ (fun ω τ => fun v => ω v + τ v) ⟩
 
 @[simp]
-theorem zero_apply : (0 : DifferentialForm E F n) v = 0 :=
+theorem add_apply : (ω + τ) v = ω v + τ v :=
   rfl
 
-instance inhabited : Inhabited (DifferentialForm E F n) :=
-  ⟨0⟩
+instance : Sub (Ω^n⟮E, F⟯) :=
+  ⟨ (fun ω τ => fun v => ω v - τ v) ⟩
+
+@[simp]
+theorem sub_apply : (ω - τ) v = ω v - τ v :=
+  rfl
+
+instance : Neg (Ω^n⟮E, F⟯) :=
+  ⟨fun ω => fun v => -ω v⟩
+
+@[simp]
+theorem neg_apply : (-ω) v = -ω v :=
+  rfl
+
+instance : SMul ℝ (Ω^n⟮E, F⟯) :=
+  ⟨fun c ω => fun v => c • ω v⟩
 
-/- Application of differential form to vector field -/
-def differentialform_apply_vectorfield {n : ℕ} (ω : DifferentialForm E F (n + 1)) (ξ : E → (Fin 1 → E)) :=
-  fun v ↦ (ω v).curryFin (ξ v 0)
+@[simp]
+theorem smul_apply (ω : Ω^n⟮E, F⟯) (c : ℝ) (v : E): (c • ω) v = c • ω v :=
+  rfl
 
+instance : Zero (Ω^n⟮E, F⟯) :=
+  ⟨ (fun _ => 0) ⟩
 
+@[simp]
+theorem zero_apply : (0 : Ω^n⟮E, F⟯) v = 0 :=
+  rfl
+
+instance inhabited : Inhabited (Ω^n⟮E, F⟯) :=
+  ⟨0⟩
 
 /-- Exterior derivative of a differential form. -/
 def ederiv (ω : Ω^n⟮E, F⟯) : Ω^n + 1⟮E, F⟯ :=
@@ -69,3 +91,27 @@ 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 x ↦ ederiv_ederiv_apply ω h.contDiffAt
+
+/- Pullback of a differential form -/
+def pullback (f : E → F) (ω : Ω^k⟮F, G⟯) : Ω^k⟮E, G⟯ :=
+  fun x ↦ (ω (f x)).compContinuousLinearMap (fderiv ℝ f x)
+
+theorem pullback_zero (f : E → F) :
+  pullback f (0 : Ω^k⟮F, G⟯) = 0 :=
+    rfl
+
+theorem pullback_add (f : E → F) (ω : Ω^k⟮F, G⟯) (τ : Ω^k⟮F, G⟯) :
+  pullback f (ω + τ) = pullback f ω + pullback f τ :=
+    rfl
+
+theorem pullback_sub (f : E → F) (ω : Ω^k⟮F, G⟯) (τ : Ω^k⟮F, G⟯) :
+  pullback f (ω - τ) = pullback f ω - pullback f τ :=
+    rfl
+
+theorem pullback_neg (f : E → F) (ω : Ω^k⟮F, G⟯) :
+  - pullback f ω = pullback f (-ω) :=
+    rfl
+
+theorem pullback_smul (f : E → F) (ω : Ω^k⟮F, G⟯) (c : ℝ) :
+  c • (pullback f ω) = pullback f (c • ω) :=
+    rfl

From 723f9cba73d0ad758f955df4124b238cb274ab14 Mon Sep 17 00:00:00 2001
From: MetalCreator666 <57985847+MetalCreator666@users.noreply.github.com>
Date: Mon, 2 Dec 2024 13:01:17 +0100
Subject: [PATCH 3/5] All pullback operations except pullbackCLM

---
 DeRhamCohomology/DifferentialForm.lean | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/DeRhamCohomology/DifferentialForm.lean b/DeRhamCohomology/DifferentialForm.lean
index d2b7180..83019e8 100644
--- a/DeRhamCohomology/DifferentialForm.lean
+++ b/DeRhamCohomology/DifferentialForm.lean
@@ -61,6 +61,19 @@ theorem zero_apply : (0 : Ω^n⟮E, F⟯) v = 0 :=
 instance inhabited : Inhabited (Ω^n⟮E, F⟯) :=
   ⟨0⟩
 
+/- The natural equivalence between differential forms from `E` to `F`
+and maps from `E` to continuous 1-multilinear alternating maps from `E` to `F`. -/
+def ofSubsingleton [Subsingleton (Fin n)] (i : Fin n) :
+    (E → E →L[ℝ] F) ≃ (Ω^n⟮E, F⟯) where
+  toFun f := fun e ↦ ContinuousAlternatingMap.ofSubsingleton ℝ E F i (f e)
+  invFun f := fun e ↦ (ContinuousAlternatingMap.ofSubsingleton ℝ E F i).symm (f e)
+  left_inv _ := rfl
+  right_inv _ := by simp
+
+/- The constant map is a differential form when `Fin n` is empty -/
+def constOfIsEmpty [IsEmpty (Fin n)] (x : F) : Ω^n⟮E, F⟯ :=
+  fun _ ↦ ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin n) x
+
 /-- Exterior derivative of a differential form. -/
 def ederiv (ω : Ω^n⟮E, F⟯) : Ω^n + 1⟮E, F⟯ :=
   fun x ↦ .uncurryFin (fderiv ℝ ω x)
@@ -115,3 +128,10 @@ theorem pullback_neg (f : E → F) (ω : Ω^k⟮F, G⟯) :
 theorem pullback_smul (f : E → F) (ω : Ω^k⟮F, G⟯) (c : ℝ) :
   c • (pullback f ω) = pullback f (c • ω) :=
     rfl
+
+theorem pullback_ofSubsingleton (f : E → F) (ω : F → F →L[ℝ] G) [Subsingleton (Fin k)] (i : Fin k) :
+  pullback f (ofSubsingleton i ω) = ofSubsingleton i (fun e ↦ (ω (f e)).comp (fderiv ℝ f e)) :=
+    rfl
+
+theorem pullback_constOfIsEmpty (f : E → F) [IsEmpty (Fin k)] (g : G) :
+  pullback f (constOfIsEmpty g) = fun _ ↦ (ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin k) g) := rfl

From 0889667b14eff96794ba63405fe633428d32b372 Mon Sep 17 00:00:00 2001
From: MetalCreator666 <57985847+MetalCreator666@users.noreply.github.com>
Date: Mon, 2 Dec 2024 13:06:22 +0100
Subject: [PATCH 4/5] update

---
 DeRhamCohomology/DifferentialForm.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/DeRhamCohomology/DifferentialForm.lean b/DeRhamCohomology/DifferentialForm.lean
index da1868a..8e1c6b2 100644
--- a/DeRhamCohomology/DifferentialForm.lean
+++ b/DeRhamCohomology/DifferentialForm.lean
@@ -2,11 +2,6 @@ import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 import DeRhamCohomology.ContinuousAlternatingMap.Curry
 import DeRhamCohomology.ContinuousAlternatingMap.FDeriv
 
-/-
-# Differential Forms
-
--/
-
 noncomputable section
 
 open Filter ContinuousAlternatingMap

From 8e991b76d586248836334c33172f09633a340aaf Mon Sep 17 00:00:00 2001
From: MetalCreator666 <57985847+MetalCreator666@users.noreply.github.com>
Date: Wed, 4 Dec 2024 16:23:00 +0100
Subject: [PATCH 5/5] Update after review

---
 DeRhamCohomology/DifferentialForm.lean | 63 ++++++++++----------------
 1 file changed, 23 insertions(+), 40 deletions(-)

diff --git a/DeRhamCohomology/DifferentialForm.lean b/DeRhamCohomology/DifferentialForm.lean
index 8e1c6b2..c2bdecc 100644
--- a/DeRhamCohomology/DifferentialForm.lean
+++ b/DeRhamCohomology/DifferentialForm.lean
@@ -18,56 +18,38 @@ variable {v : E}
 variable (ω τ : Ω^n⟮E, F⟯)
 variable (f : E → F)
 
-instance : Add (Ω^n⟮E, F⟯) :=
-  ⟨ (fun ω τ => fun v => ω v + τ v) ⟩
-
 @[simp]
 theorem add_apply : (ω + τ) v = ω v + τ v :=
   rfl
 
-instance : Sub (Ω^n⟮E, F⟯) :=
-  ⟨ (fun ω τ => fun v => ω v - τ v) ⟩
-
 @[simp]
 theorem sub_apply : (ω - τ) v = ω v - τ v :=
   rfl
 
-instance : Neg (Ω^n⟮E, F⟯) :=
-  ⟨fun ω => fun v => -ω v⟩
-
 @[simp]
 theorem neg_apply : (-ω) v = -ω v :=
   rfl
 
-instance : SMul ℝ (Ω^n⟮E, F⟯) :=
-  ⟨fun c ω => fun v => c • ω v⟩
-
 @[simp]
-theorem smul_apply (ω : Ω^n⟮E, F⟯) (c : ℝ) (v : E): (c • ω) v = c • ω v :=
+theorem smul_apply (ω : Ω^n⟮E, F⟯) (c : ℝ) : (c • ω) v = c • ω v :=
   rfl
 
-instance : Zero (Ω^n⟮E, F⟯) :=
-  ⟨ (fun _ => 0) ⟩
-
 @[simp]
 theorem zero_apply : (0 : Ω^n⟮E, F⟯) v = 0 :=
   rfl
 
-instance inhabited : Inhabited (Ω^n⟮E, F⟯) :=
-  ⟨0⟩
-
 /- The natural equivalence between differential forms from `E` to `F`
 and maps from `E` to continuous 1-multilinear alternating maps from `E` to `F`. -/
-def ofSubsingleton [Subsingleton (Fin n)] (i : Fin n) :
-    (E → E →L[ℝ] F) ≃ (Ω^n⟮E, F⟯) where
-  toFun f := fun e ↦ ContinuousAlternatingMap.ofSubsingleton ℝ E F i (f e)
-  invFun f := fun e ↦ (ContinuousAlternatingMap.ofSubsingleton ℝ E F i).symm (f e)
+def ofSubsingleton :
+    (E → E →L[ℝ] F) ≃ (Ω^1⟮E, F⟯) where
+  toFun f := fun e ↦ ContinuousAlternatingMap.ofSubsingleton ℝ E F 0 (f e)
+  invFun f := fun e ↦ (ContinuousAlternatingMap.ofSubsingleton ℝ E F 0).symm (f e)
   left_inv _ := rfl
   right_inv _ := by simp
 
 /- The constant map is a differential form when `Fin n` is empty -/
-def constOfIsEmpty [IsEmpty (Fin n)] (x : F) : Ω^n⟮E, F⟯ :=
-  fun _ ↦ ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin n) x
+def constOfIsEmpty (x : F) : Ω^0⟮E, F⟯ :=
+  fun _ ↦ ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin 0) x
 
 /-- Exterior derivative of a differential form. -/
 def ederiv (ω : Ω^n⟮E, F⟯) : Ω^n + 1⟮E, F⟯ :=
@@ -105,28 +87,29 @@ def pullback (f : E → F) (ω : Ω^k⟮F, G⟯) : Ω^k⟮E, G⟯ :=
   fun x ↦ (ω (f x)).compContinuousLinearMap (fderiv ℝ f x)
 
 theorem pullback_zero (f : E → F) :
-  pullback f (0 : Ω^k⟮F, G⟯) = 0 :=
-    rfl
+    pullback f (0 : Ω^k⟮F, G⟯) = 0 :=
+  rfl
 
 theorem pullback_add (f : E → F) (ω : Ω^k⟮F, G⟯) (τ : Ω^k⟮F, G⟯) :
-  pullback f (ω + τ) = pullback f ω + pullback f τ :=
-    rfl
+    pullback f (ω + τ) = pullback f ω + pullback f τ :=
+  rfl
 
 theorem pullback_sub (f : E → F) (ω : Ω^k⟮F, G⟯) (τ : Ω^k⟮F, G⟯) :
-  pullback f (ω - τ) = pullback f ω - pullback f τ :=
-    rfl
+    pullback f (ω - τ) = pullback f ω - pullback f τ :=
+  rfl
 
 theorem pullback_neg (f : E → F) (ω : Ω^k⟮F, G⟯) :
-  - pullback f ω = pullback f (-ω) :=
-    rfl
+    - pullback f ω = pullback f (-ω) :=
+  rfl
 
 theorem pullback_smul (f : E → F) (ω : Ω^k⟮F, G⟯) (c : ℝ) :
-  c • (pullback f ω) = pullback f (c • ω) :=
-    rfl
+    c • (pullback f ω) = pullback f (c • ω) :=
+  rfl
 
-theorem pullback_ofSubsingleton (f : E → F) (ω : F → F →L[ℝ] G) [Subsingleton (Fin k)] (i : Fin k) :
-  pullback f (ofSubsingleton i ω) = ofSubsingleton i (fun e ↦ (ω (f e)).comp (fderiv ℝ f e)) :=
-    rfl
+theorem pullback_ofSubsingleton (f : E → F) (ω : F → F →L[ℝ] G) :
+    pullback f (ofSubsingleton ω) = ofSubsingleton (fun e ↦ (ω (f e)).comp (fderiv ℝ f e)) :=
+  rfl
 
-theorem pullback_constOfIsEmpty (f : E → F) [IsEmpty (Fin k)] (g : G) :
-  pullback f (constOfIsEmpty g) = fun _ ↦ (ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin k) g) := rfl
+theorem pullback_constOfIsEmpty (f : E → F) (g : G) :
+    pullback f (constOfIsEmpty g) = fun _ ↦ (ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin 0) g) :=
+  rfl