Refactor draft Alternating Maps Bundle

DeRhamCohomology/DifferentialForm.lean

@@ -185,44 +185,6 @@ theorem ederiv_ederiv (ω : Ω^n⟮E, F⟯) (h : ContDiff ℝ 2 ω) : ederiv (ed
 def pullback (f : E → F) (ω : Ω^k⟮F, G⟯) : Ω^k⟮E, G⟯ :=
     fun x ↦ (ω (f x)).compContinuousLinearMap (fderiv ℝ f x)
 
-/- Pullback within a set of form under a function -/
-def pullbackWithin (f : E → F) (ω : Ω^k⟮F, G⟯) (s : Set E) : Ω^k⟮E, G⟯ :=
-    fun x ↦ (ω (f x)).compContinuousLinearMap (fderivWithin ℝ f s x)
-
-@[simp]
-lemma pullbackWithin_univ {f : E → F} {ω : Ω^k⟮F, G⟯} :
-    pullbackWithin f ω univ = pullback f ω := by
-  ext x v
-  simp [pullbackWithin, pullback]
-
-theorem pullbackWithin_zero (f : E → F) (s : Set E):
-    pullbackWithin f (0 : Ω^k⟮F, G⟯) s = 0 :=
-  rfl
-
-theorem pullbackWithin_add (f : E → F) (ω : Ω^k⟮F, G⟯) (τ : Ω^k⟮F, G⟯) (s : Set E) :
-    pullbackWithin f (ω + τ) s = pullbackWithin f ω s + pullbackWithin f τ s :=
-  rfl
-
-theorem pullbackWithin_sub (f : E → F) (ω : Ω^k⟮F, G⟯) (τ : Ω^k⟮F, G⟯) (s : Set E) :
-    pullbackWithin f (ω - τ) s = pullbackWithin f ω s - pullbackWithin f τ s :=
-  rfl
-
-theorem pullbackWithin_neg (f : E → F) (ω : Ω^k⟮F, G⟯) (s : Set E) :
-    - pullbackWithin f ω s = pullbackWithin f (-ω) s :=
-  rfl
-
-theorem pullbackWithin_smul (f : E → F) (ω : Ω^k⟮F, G⟯) (c : ℝ) (s : Set E) :
-    c • (pullbackWithin f ω s) = pullbackWithin f (c • ω) s :=
-  rfl
-
-theorem pullbackWithin_ofSubsingleton (f : E → F) (ω : F → F →L[ℝ] G) (s : Set E) :
-    pullbackWithin f (ofSubsingleton ω) s = ofSubsingleton (fun e ↦ (ω (f e)).comp (fderivWithin ℝ f s e)) :=
-  rfl
-
-theorem pullbackWithin_constOfIsEmpty (f : E → F) (g : G) (s : Set E) :
-    pullbackWithin f (constOfIsEmpty g) s = fun _ ↦ (ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin 0) g) :=
-  rfl
-
 theorem pullback_zero (f : E → F) :
     pullback f (0 : Ω^k⟮F, G⟯) = 0 :=
   rfl

DeRhamCohomology/Manifold/DifferentialForm.lean

@@ -20,9 +20,8 @@ variable
   {M'' : Type*} [TopologicalSpace M''] [ChartedSpace H'' M'']
   {f : M → M'} {s t : Set M} {x y : M}
 
-/- This isn't right ...
-Need a ContDiff and ContMDiff version of Alternating maps first??
-Then one can define this as the map M → TangentSpace I [k, ⋀^Fin n]→L[ ℝ ] ℝ -/
-notation "Ω^" k "," n "⟮" I ", " M "⟯" => M → TangentSpace I [⋀^Fin n]→L[ℝ] ℝ
+/- Step 1 : Define differential forms as sections of the continuous alternating maps bundle -/
+
+
 
 namespace DifferentialForm

DeRhamCohomology/Manifold/VectorBundle/Alternating.lean

@@ -0,0 +1,64 @@
+import Mathlib.Geometry.Manifold.VectorBundle.Basic
+import DeRhamCohomology.VectorBundle.Alternating
+
+noncomputable section
+
+open Bundle Set ContinuousLinearMap Pretrivialization
+
+open scoped Manifold Bundle
+
+variable {𝕜 ι B F₁ F₂ M : Type*} {E₁ : B → Type*} {E₂ : B → Type*}
+  [NontriviallyNormedField 𝕜]
+  [Fintype ι]
+  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB]
+  {HB : Type*} [TopologicalSpace HB]
+  (IB : ModelWithCorners 𝕜 EB HB)
+  [TopologicalSpace B] [ChartedSpace HB B]
+  [∀ x, AddCommGroup (E₁ x)] [∀ x, Module 𝕜 (E₁ x)]
+  [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁]
+  [TopologicalSpace (TotalSpace F₁ E₁)] [∀ x, TopologicalSpace (E₁ x)] [∀ x, AddCommGroup (E₂ x)]
+  [∀ x, Module 𝕜 (E₂ x)]
+  [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂]
+  [TopologicalSpace (TotalSpace F₂ E₂)] [∀ x, TopologicalSpace (E₂ x)]
+  [∀ x, TopologicalAddGroup (E₂ x)] [∀ x, ContinuousSMul 𝕜 (E₂ x)]
+  {EM : Type*} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM]
+  {HM : Type*} [TopologicalSpace HM]
+  {IM : ModelWithCorners 𝕜 EM HM}
+  [TopologicalSpace M] [ChartedSpace HM M] [SmoothManifoldWithCorners IM M] --{n : ℕ∞}
+  [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁]
+  [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂]
+  -- {e₁ e₁' : Trivialization F₁ (π F₁ E₁)}
+  -- {e₂ e₂' : Trivialization F₂ (π F₂ E₂)}
+
+variable [SmoothVectorBundle F₁ E₁ IB] [SmoothVectorBundle F₂ E₂ IB]
+
+instance Bundle.continuousAlternatingMap.vectorPrebundle.isSmooth :
+   (Bundle.continuousAlternatingMap.vectorPrebundle 𝕜 ι F₁ E₁ F₂ E₂).IsSmooth IB where
+  exists_smoothCoordChange := by
+    rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩
+    refine ⟨continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂', ?_, ?_⟩
+    · -- have h₃ := contMDiffOn_coordChangeL e₁' e₁
+      -- have h₄ := contMDiffOn_coordChangeL e₂ e₂'
+      let s (q : (F₁ →L[𝕜] F₁) × (F₂ →L[𝕜] F₂)) :
+          (F₁ →L[𝕜] F₁) × ((F₁ [⋀^ι]→L[𝕜] F₂) →L[𝕜] (F₁ [⋀^ι]→L[𝕜] F₂)) :=
+        (q.1, ContinuousLinearMap.compContinuousAlternatingMapL 𝕜 F₁ F₂ F₂ q.2)
+      have hs : ContMDiff 𝓘(𝕜, (F₁ →L[𝕜] F₁) × (F₂ →L[𝕜] F₂))
+          𝓘(𝕜, (F₁ →L[𝕜] F₁) × ((F₁ [⋀^ι]→L[𝕜] F₂) →L[𝕜] (F₁ [⋀^ι]→L[𝕜] F₂))) ⊤ s :=
+        -- smooth_id.prod_map (ContinuousLinearMap.smooth _)
+        sorry
+  --     have' := ((continuous_snd.clm_comp
+  --       ((ContinuousAlternatingMap.compContinuousLinearMapL_continuous 𝕜 ι F₁ F₂).comp
+  --       continuous_fst)).comp hs).comp_continuousOn
+  --       (s := (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))) ((h₃.mono ?_).prod (h₄.mono ?_))
+    -- · exact this
+    -- · mfld_set_tac
+    -- · mfld_set_tac
+
+      sorry
+    · rintro b hb v
+      apply continuousAlternatingMapCoordChange_apply
+      exact hb
+
+instance SmoothVectorBundle.continuousAlternatingMap :
+    SmoothVectorBundle (F₁ [⋀^ι]→L[𝕜] F₂) (Bundle.continuousAlternatingMap 𝕜 ι F₁ E₁ F₂ E₂) IB :=
+  (Bundle.continuousAlternatingMap.vectorPrebundle 𝕜 ι F₁ E₁ F₂ E₂).smoothVectorBundle IB