diffeology update

SciLean/Analysis/Diffeology/Connection.lean

@@ -1,4 +1,7 @@
 import SciLean.Analysis.Diffeology.PlotHomotopy
+import SciLean.Analysis.Diffeology.Prod
+import SciLean.Analysis.Diffeology.NormedSpace
+
 
 namespace SciLean
 
@@ -18,13 +21,18 @@ class Connection {X : Type*} (E : X → Type*) [Diffeology X] [∀ x, Diffeology
     lift c r t (lift c s r v) = lift c s t v
 
   smooth_comp {n m}
-    {p : ℝ^n → Sigma E}
+    {p : ℝ^n → Sigma E} {x}
     {ht : PlotPointHomotopy (fun u => (p u).1) x}
     {hp₂ : ht.transportSection' lift (fun u => (p u).2) ∈ plots n}
     (f : ℝ^m → ℝ^n) (hf : ContDiff ℝ ⊤ f)
     (ht' : PlotPointHomotopy (fun u => (p (f u)).1) x) :
     ht'.transportSection' lift (fun u => (p (f u)).2) ∈ plots m
 
+  const_lift {n} {x y : X}
+    {path : PlotHomotopy (fun _ : ℝ^n => x) (fun _ : ℝ^n => y)}
+    (p : ℝ^n → E x) (hp : p ∈ plots n) :
+    PlotPointHomotopy.transportSection' path lift p ∈ plots n
+
 
 def PlotPointHomotopy.transportSection
     {X : Type*} {E : X → Type*} [Diffeology X] [∀ x, Diffeology (E x)] [Connection E]
@@ -62,8 +70,97 @@ instance {X : Type*} (E : X → Type*) [Diffeology X] [∀ x, Diffeology (E x)]
     · apply Diffeology.const_plot
     · intros x₀ ht
       simp at ht
-      simp
       unfold PlotPointHomotopy.transportSection
-      unfold PlotPointHomotopy.transportSection'
-      simp
-      sorry
+      apply Connection.const_lift
+      apply const_plot
+
+
+variable
+  {X : Type*} [Diffeology X]
+  {E : X → Type*} [∀ x, Diffeology (E x)] [Connection E]
+
+def DDSmooth (f : (x : X) → E x) : Prop :=
+  DSmooth (fun x => Sigma.mk x (f x))
+
+class DVec (X : Type*) extends AddCommGroup X, Module ℝ X, Diffeology X, TangentSpace X (fun _ => X) where
+  add_smooth : TSSmooth (fun x : X×X => x.1+x.2)
+  smul_smooth : TSSmooth (fun x : ℝ×X => x.1•x.2)
+
+
+instance [AddCommGroup X] [Module ℝ X] : Diffeology X := sorry
+instance [AddCommGroup X] [Module ℝ X] : TangentSpace X (fun _ => X) := sorry
+
+instance [AddCommGroup X] [Module ℝ X] : Connection (fun _ : α => X) := sorry
+
+open TangentSpace in
+instance {X : Type*} [Diffeology X] (TX : X → Type*) [∀ x, AddCommGroup (TX x)] [∀ x, Module ℝ (TX x)]
+    [TangentSpace X TX] [∀ x, Diffeology (TX x)] [Connection TX] :
+    TangentSpace (Sigma TX) (fun x => TX x.1 × TX x.1) := sorry
+
+
+instance   {X : Type*} [Diffeology X] {TX : X → Type*} [∀ x, AddCommGroup (TX x)] [∀ x, Module ℝ (TX x)] [TangentSpace X TX]
+  {E : X → Type*} [∀ x, Diffeology (E x)]
+  {TE : (x : X) → E x → Type*} [∀ x e, AddCommGroup (TE x e)] [∀ x e, Module ℝ (TE x e)] [∀ x, TangentSpace (E x) (TE x)] [Connection E] :
+  TangentSpace (Sigma E) (fun x => TX x.1 × TE x.1 x.2) := sorry
+
+
+-- def covDeriv
+--   {X : Type*} [Diffeology X] {TX : X → Type*} [∀ x, AddCommGroup (TX x)] [∀ x, Module ℝ (TX x)] [TangentSpace X TX] [TangentSpace X TX]
+--   {E : X → Type*} [∀ x, Diffeology (E x)]
+--   {TE : (x : X) → E x → Type*} [∀ x e, AddCommGroup (TE x e)] [∀ x e, Module ℝ (TE x e)] [∀ x, TangentSpace (E x) (TE x)] [Connection E]
+--   (f : (x : X) → E x) (x : X) (dx : TX x) : TE _ (f x)  :=
+--   let c := TangentSpace.exp x dx
+--   let c' := fun x => f (c x)
+--   let c' := fun t => Sigma.mk (c t) (f (c t))
+--   let v'' := TangentSpace.tangentMap c' sorry 0 1
+--   cast (by simp[c',c]; rw[TangentSpace.exp_at_zero]) v''.2
+
+
+open Classical in
+noncomputable
+def covDeriv
+  {X : Type*} [Diffeology X] {TX : X → Type*}
+  [∀ x, AddCommGroup (TX x)] [∀ x, Module ℝ (TX x)] [TangentSpace X TX]
+  {Y : Type*} [Diffeology Y] {TY : Y → Type*}
+  [∀ y, AddCommGroup (TY y)] [∀ y, Module ℝ (TY y)] [TangentSpace Y TY]
+  {E : Y → Type*} [∀ x, Diffeology (E x)] {TE : (y : Y) → E y → Type*}
+  [∀ y e, AddCommGroup (TE y e)] [∀ y e, Module ℝ (TE y e)] [∀ y, TangentSpace (E y) (TE y)] [Connection E]
+  {g : X → Y} (f : (x : X) → E (g x)) (x : X) (dx : TX x) : TE _ (f x)  :=
+  let c := TangentSpace.exp x dx
+  let c' := fun t => Sigma.mk (g (c t)) (f (c t))
+  if hc : c' ∈ Diffeology.plots 1 then
+    let v'' := TangentSpace.tangentMap c' hc 0 1
+    cast (by simp[c',c]; rw[TangentSpace.exp_at_zero]) v''.2
+  else
+    0
+
+
+example {X} [AddCommGroup X] [Module ℝ X] [Diffeology X] [TangentSpace X (fun _ => X)] :
+  TangentSpace (X×X) (fun _ => X × X) := by infer_instance
+
+open TangentSpace
+
+
+variable (n : ℕ)
+
+#synth TangentSpace (Fin n → ℝ) (fun x => Fin n → ℝ)
+
+-- instance {W : Type*} [Diffeology W] {X : Type*} [Diffeology X] (f : W → X) [Fact (DSmooth f)] (E : X → Type*) [∀ x, Diffeology (E x)]
+--   [Connection E] : Connection (fun w => E (f w)) := sorry
+
+noncomputable
+instance {X : Type*} [Diffeology X] (TX : X → Type*) [∀ x, DVec (TX x)]
+    [TangentSpace X TX] [∀ x, Diffeology (TX x)] [Connection TX] :
+    TangentSpace (Sigma TX) (fun x => TX x.1 × TX x.1) where
+
+  tangentMap {n} p hp u du :=
+    let dy := tangentMap (fun u => (p u).1) hp.1 u du
+    let dz := covDeriv (fun u => (p u).2) u du
+    (dy,dz)
+  tangentMap_comp := sorry
+  tangentMap_const := sorry
+  tangentMap_linear := sorry
+  exp := sorry
+  exp_at_zero := sorry
+  exp_is_plot := sorry
+  tangentMap_exp_at_zero := sorry

SciLean/Analysis/Diffeology/Prod.lean

@@ -1,4 +1,5 @@
 import SciLean.Analysis.Diffeology.Basic
+import SciLean.Analysis.Diffeology.TangentSpace
 
 namespace SciLean
 
@@ -11,11 +12,11 @@ open Diffeology in
 instance : Diffeology (X × Y) where
   plots := fun n p =>
     Prod.fst ∘ p ∈ plots n ∧ Prod.snd ∘ p ∈ plots n
-  smooth_comp := by
+  plot_comp := by
     intros n m p f hp hf
     constructor
-    · exact Diffeology.smooth_comp hp.1 hf
-    · exact Diffeology.smooth_comp hp.2 hf
+    · exact Diffeology.plot_comp hp.1 hf
+    · exact Diffeology.plot_comp hp.2 hf
   const_plot := by
     intros n x
     constructor
@@ -30,35 +31,35 @@ instance
     [∀ y, AddCommGroup (TY y)] [∀ y, Module ℝ (TY y)] [TangentSpace Y TY] :
     TangentSpace (X × Y) (fun xy => TX xy.1 × TY xy.2) where
 
-  tangent c hc x dx := (tangent (Prod.fst ∘ c) hc.1 x dx, tangent (Prod.snd ∘ c) hc.2 x dx)
+  tangentMap c hc x dx := (tangentMap (Prod.fst ∘ c) hc.1 x dx, tangentMap (Prod.snd ∘ c) hc.2 x dx)
 
-  smooth_comp := by
+  tangentMap_comp := by
     intros n m p f hp hf x dx
-    have := smooth_comp hp.1 hf x dx
-    have := smooth_comp hp.2 hf x dx
+    have := tangentMap_comp hp.1 hf x dx
+    have := tangentMap_comp hp.2 hf x dx
     simp_all [Function.comp_def]
 
-  tangent_const := by
+  tangentMap_const := by
     intro n x t dt
-    have := tangent_const x.1 t dt
-    have := tangent_const x.2 t dt
+    have := tangentMap_const x.1 t dt
+    have := tangentMap_const x.2 t dt
     simp_all [Function.comp_def]
 
-  curve x dx t := (curve x.1 dx.1 t, curve x.2 dx.2 t)
-  curve_at_zero := by intros; simp
-  curve_is_plot x dx:= ⟨curve_is_plot x.1 dx.1, curve_is_plot x.2 dx.2⟩
+  exp x dx t := (exp x.1 dx.1 t, exp x.2 dx.2 t)
+  exp_at_zero := by intros; simp
+  exp_is_plot x dx:= ⟨exp_is_plot x.1 dx.1, exp_is_plot x.2 dx.2⟩
 
-  tangent_curve_at_zero := by
+  tangentMap_exp_at_zero := by
     intros x dx t
-    have := tangent_curve_at_zero x.1 dx.1 t
-    have := tangent_curve_at_zero x.2 dx.2 t
+    have := tangentMap_exp_at_zero x.1 dx.1 t
+    have := tangentMap_exp_at_zero x.2 dx.2 t
     simp_all [Function.comp_def]
     ext <;> simp
 
-  tangent_linear := by
+  tangentMap_linear := by
     intros n c hc x
-    have := (tangent_linear _ hc.1 x).1
-    have := (tangent_linear _ hc.1 x).2
-    have := (tangent_linear _ hc.2 x).1
-    have := (tangent_linear _ hc.2 x).2
+    have := (tangentMap_linear _ hc.1 x).1
+    have := (tangentMap_linear _ hc.1 x).2
+    have := (tangentMap_linear _ hc.2 x).1
+    have := (tangentMap_linear _ hc.2 x).2
     constructor <;> simp_all