ManifoldProjectedCurvature.lean

1 module
2 public import GlobalProjectedConnection
3 import all ProjectedCurvature
4 import all Mathlib.Geometry.Manifold.IsManifold.Basic
5 import all Mathlib.Geometry.Manifold.VectorField.LieBracket
6 import all Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
7 public import Mathlib.Tactic
8 /-! Author: Komorebi P. Paper VII, sixth block.
9 Curvature of the actual global connection on arbitrary smooth real manifolds
10 without boundary, modelled on a complete normed space. No global chart is assumed.
11 -/
12 @[expose] public section
13 set_option autoImplicit false
14 set_option backward.isDefEq.respectTransparency false
15 set_option backward.isDefEq.respectTransparency.types false
16 set_option linter.unusedSectionVars false
17 open scoped Manifold ContDiff Topology
18 open Set Filter
19 noncomputable section
20 namespace KomorebiPaperVII.ManifoldCurvature
21 open KomorebiPaperVII.GlobalConnection
22 
23 variable {E M F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
24   [TopologicalSpace M] [ChartedSpace E M] [IsManifold 𝓘(ℝ,E) ∞ M]
25   [NormedAddCommGroup F] [NormedSpace ℝ F]
26 
27 /-- Derivative in the chart centred at the point being differentiated. -/
28 theorem derivative_in_chart (s : M → F) (x : M)
29     (hs : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,F) s x) :
30     mvfderiv 𝓘(ℝ,E) s x =
31       fderiv ℝ (s ∘ (extChartAt 𝓘(ℝ,E) x).symm) (extChartAt 𝓘(ℝ,E) x x) := by
32   simpa [writtenInExtChartAt, mfld_simps] using hs.mvfderiv
33 
34 theorem differentiable_in_chart (s : M → F) (x : M)
35     (hs : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,F) s x) :
36     DifferentiableAt ℝ (s ∘ (extChartAt 𝓘(ℝ,E) x).symm) (extChartAt 𝓘(ℝ,E) x x) := by
37   simpa [differentiableWithinAt_univ] using (hs.mdifferentiableWithinAt (s := Set.univ)).differentiableWithinAt_comp_extChartAt_symm
38 
39 theorem smooth_in_chart (s : M → F) (a : M)
40     (hs : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F) ∞ s) :
41     ContDiffAt ℝ ∞ (s ∘ (extChartAt 𝓘(ℝ,E) a).symm) (extChartAt 𝓘(ℝ,E) a a) := by
42   have hi : ContMDiffAt 𝓘(ℝ,E) 𝓘(ℝ,E) ∞ (extChartAt 𝓘(ℝ,E) a).symm
43       (extChartAt 𝓘(ℝ,E) a a) := by
44     simpa [contMDiffWithinAt_univ] using (contMDiffWithinAt_extChartAt_symm_range (I := 𝓘(ℝ,E)) (n := ∞)
45       a (mem_extChartAt_target a))
46   exact ((hs _).comp _ hi).contDiffAt
47 
48 /-- Manifold product rule for operator evaluation, proved from actual derivatives. -/
49 theorem derivative_clm_apply (P : M → F →L[ℝ] F) (s : M → F) (x : M)
50     (hP : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,F →L[ℝ] F) P x)
51     (hs : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,F) s x) (v : TangentSpace 𝓘(ℝ,E) x) :
52     mvfderiv 𝓘(ℝ,E) (fun y => P y (s y)) x v =
53       P x (mvfderiv 𝓘(ℝ,E) s x v)+mvfderiv 𝓘(ℝ,E) P x v (s x) := by
54   rw [derivative_in_chart _ x (hP.clm_apply hs),derivative_in_chart P x hP,
55     derivative_in_chart s x hs]
56   have hd := congrArg (fun q : E →L[ℝ] F => q v)
57     (fderiv_clm_apply (differentiable_in_chart P x hP) (differentiable_in_chart s x hs))
58   simpa [Function.comp_def] using! hd
59 
60 /-- The actual pullback of a vector field into a chart. -/
61 def chartField (a : M) (X : ∀ x : M, TangentSpace 𝓘(ℝ,E) x) : E → E :=
62   VectorField.mpullbackWithin 𝓘(ℝ,E) 𝓘(ℝ,E) (extChartAt 𝓘(ℝ,E) a).symm X
63     (Set.range 𝓘(ℝ,E))
64 
65 theorem chartField_self (a : M) (X : ∀ x : M, TangentSpace 𝓘(ℝ,E) x) :
66     chartField a X (extChartAt 𝓘(ℝ,E) a a)=X a := by
67   dsimp only [chartField]
68   rw [VectorField.mpullbackWithin_apply]
69   have he : (X ((extChartAt 𝓘(ℝ,E) a).symm (extChartAt 𝓘(ℝ,E) a a)) : E) = X a := by
70     exact congrArg (fun z : M => (show E from X z)) (extChartAt_to_inv (I := 𝓘(ℝ,E)) a)
71   rw [he]
72   exact mfderivWithin_extChartAt_symm_inverse_apply (I := 𝓘(ℝ,E)) (X a)
73 
74 theorem chartField_differentiable (a : M) (X : ∀ x : M, TangentSpace 𝓘(ℝ,E) x)
75     (hX : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,E).tangent
76       (fun x => (X x : TangentBundle 𝓘(ℝ,E) M)) a) :
77     DifferentiableAt ℝ (chartField a X) (extChartAt 𝓘(ℝ,E) a a) := by
78   simpa [chartField, differentiableWithinAt_univ] using (hX.mdifferentiableWithinAt (s := Set.univ)).differentiableWithinAt_mpullbackWithin_vectorField
79 
80 theorem bracket_in_chart (a : M) (X Y : ∀ x : M, TangentSpace 𝓘(ℝ,E) x) :
81     VectorField.mlieBracket 𝓘(ℝ,E) X Y a =
82       VectorField.lieBracket ℝ (chartField a X) (chartField a Y) (extChartAt 𝓘(ℝ,E) a a) := by
83   rw [VectorField.mlieBracket,VectorField.mlieBracketWithin_apply]
84   rw [mfderiv_extChartAt_self, ContinuousLinearMap.inverse_id]
85   change VectorField.lieBracketWithin ℝ (chartField a X) (chartField a Y)
86     ((extChartAt 𝓘(ℝ,E) a).symm ⁻¹' Set.univ ∩ Set.range 𝓘(ℝ,E))
87     (extChartAt 𝓘(ℝ,E) a a) = _
88   simp
89 
90 /-- The chain rule identifies directional derivatives on every point of a chart domain. -/
91 theorem directional_chart_pullback (s : M → F)
92     (hs : MDifferentiable 𝓘(ℝ,E) 𝓘(ℝ,F) s)
93     (Y : ∀ x : M, TangentSpace 𝓘(ℝ,E) x) (a : M) (u : E)
94     (hu : u ∈ (extChartAt 𝓘(ℝ,E) a).target) :
95     fderiv ℝ (s ∘ (extChartAt 𝓘(ℝ,E) a).symm) u (chartField a Y u) =
96       mvfderiv 𝓘(ℝ,E) s ((extChartAt 𝓘(ℝ,E) a).symm u)
97         (Y ((extChartAt 𝓘(ℝ,E) a).symm u)) := by
98   have hi : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,E) (extChartAt 𝓘(ℝ,E) a).symm u := by
99     simpa [mdifferentiableWithinAt_univ] using (mdifferentiableWithinAt_extChartAt_symm (I := 𝓘(ℝ,E)) hu)
100   have hc := mvfderiv_comp u (hs _) hi
101   have hinv : (mfderiv 𝓘(ℝ,E) 𝓘(ℝ,E) (extChartAt 𝓘(ℝ,E) a).symm u).IsInvertible := by
102     simpa using (isInvertible_mfderivWithin_extChartAt_symm (I := 𝓘(ℝ,E)) hu)
103   have hd : fderiv ℝ (s ∘ (extChartAt 𝓘(ℝ,E) a).symm) u =
104       (mvfderiv 𝓘(ℝ,E) s ((extChartAt 𝓘(ℝ,E) a).symm u)).comp
105         (mfderiv 𝓘(ℝ,E) 𝓘(ℝ,E) (extChartAt 𝓘(ℝ,E) a).symm u) := by
106     convert! hc using 1
107     exact (mfderiv_eq_fderiv : mfderiv 𝓘(ℝ,E) 𝓘(ℝ,F) (s ∘ (extChartAt 𝓘(ℝ,E) a).symm) u = _).symm
108   rw [hd]
109   simp only [ContinuousLinearMap.comp_apply,chartField,VectorField.mpullbackWithin_apply,
110     modelWithCornersSelf_coe,Set.range_id,mfderivWithin_univ]
111   exact congrArg (fun v => mvfderiv 𝓘(ℝ,E) s ((extChartAt 𝓘(ℝ,E) a).symm u) v)
112     (hinv.self_apply_inverse (Y ((extChartAt 𝓘(ℝ,E) a).symm u)))
113 
114 /-- The outer derivative also agrees after localization to an open chart. -/
115 theorem second_directional_in_chart (s : M → F)
116     (hs : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F) ∞ s)
117     (X Y : ∀ x : M, TangentSpace 𝓘(ℝ,E) x)
118     (hY : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞
119       (fun x => (Y x : TangentBundle 𝓘(ℝ,E) M))) (a : M) :
120     mvfderiv 𝓘(ℝ,E) (fun x => mvfderiv 𝓘(ℝ,E) s x (Y x)) a (X a) =
121       fderiv ℝ (fun u => fderiv ℝ (s ∘ (extChartAt 𝓘(ℝ,E) a).symm) u (chartField a Y u))
122         (extChartAt 𝓘(ℝ,E) a a) (chartField a X (extChartAt 𝓘(ℝ,E) a a)) := by
123   rw [chartField_self,derivative_in_chart _ a
124     ((smooth_directional 𝓘(ℝ,E) s Y hs hY).mdifferentiableAt (by simp))]
125   congr 1
126   apply Filter.EventuallyEq.fderiv_eq
127   filter_upwards [(isOpen_extChartAt_target (I := 𝓘(ℝ,E)) a).mem_nhds (mem_extChartAt_target a)]
128     with u hu
129   exact (directional_chart_pullback s (hs.mdifferentiable (by simp)) Y a u hu).symm
130 
131 /-- Flat ambient differentiation obeys the actual manifold Lie-bracket identity. -/
132 theorem derivative_lieBracket (s : M → F)
133     (hs : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F) ∞ s)
134     (X Y : ∀ x : M, TangentSpace 𝓘(ℝ,E) x)
135     (hX : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞
136       (fun x => (X x : TangentBundle 𝓘(ℝ,E) M)))
137     (hY : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞
138       (fun x => (Y x : TangentBundle 𝓘(ℝ,E) M))) (a : M) :
139     mvfderiv 𝓘(ℝ,E) s a (VectorField.mlieBracket 𝓘(ℝ,E) X Y a) =
140       mvfderiv 𝓘(ℝ,E) (fun x => mvfderiv 𝓘(ℝ,E) s x (Y x)) a (X a) -
141       mvfderiv 𝓘(ℝ,E) (fun x => mvfderiv 𝓘(ℝ,E) s x (X x)) a (Y a) := by
142   rw [second_directional_in_chart s hs X Y hY a,second_directional_in_chart s hs Y X hX a,
143     bracket_in_chart,derivative_in_chart s a (hs.mdifferentiableAt (by simp))]
144   exact VectorField.fderiv_apply_lieBracket (E := E) (F := F) (smooth_in_chart s a hs) (by simp)
145     (chartField_differentiable a Y (hY.mdifferentiableAt (by simp)))
146     (chartField_differentiable a X (hX.mdifferentiableAt (by simp)))
147 
148 
149 /-- The differentiated idempotence identity on the actual tangent space. -/
150 theorem projector_jet (P : M → F →L[ℝ] F) (x : M)
151     (hP : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,F →L[ℝ] F) P x)
152     (hPP : ∀ x, P x*P x=P x) (v : TangentSpace 𝓘(ℝ,E) x) :
153     mvfderiv 𝓘(ℝ,E) P x v * P x + P x * mvfderiv 𝓘(ℝ,E) P x v =
154       mvfderiv 𝓘(ℝ,E) P x v := by
155   rw [derivative_in_chart P x hP]
156   have hh := LocalCurvature.projector_jet (P ∘ (extChartAt 𝓘(ℝ,E) x).symm)
157     (extChartAt 𝓘(ℝ,E) x x) (differentiable_in_chart P x hP)
158     (fun y => hPP _) (show E from v)
159   simpa [Function.comp_def] using! hh
160 
161 theorem projector_differential_sandwich (P : M → F →L[ℝ] F) (x : M)
162     (hP : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,F →L[ℝ] F) P x)
163     (hPP : ∀ x, P x*P x=P x) (v : TangentSpace 𝓘(ℝ,E) x) :
164     P x * mvfderiv 𝓘(ℝ,E) P x v * P x = 0 :=
165   Curvature.jet_sandwich_zero _ _ (hPP x) (projector_jet P x hP hPP v)
166 
167 theorem section_jet (P : M → F →L[ℝ] F) (s : M → F) (x : M)
168     (hP : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,F →L[ℝ] F) P x)
169     (hs : MDifferentiableAt 𝓘(ℝ,E) 𝓘(ℝ,F) s x)
170     (hPs : ∀ x, P x (s x)=s x) (v : TangentSpace 𝓘(ℝ,E) x) :
171     mvfderiv 𝓘(ℝ,E) s x v =
172       mvfderiv 𝓘(ℝ,E) P x v (s x) + P x (mvfderiv 𝓘(ℝ,E) s x v) := by
173   have hh := derivative_clm_apply P s x hP hs v
174   have heq : (fun y => P y (s y))=s := funext hPs
175   rw [heq] at hh
176   simpa only [add_comm] using hh
177 
178 theorem nabla_derivative (P : M → F →L[ℝ] F)
179     (Y : ∀ x : M, TangentSpace 𝓘(ℝ,E) x) (s : M → F) (x : M)
180     (hP : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F →L[ℝ] F) ∞ P)
181     (hY : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞
182       (fun x => (Y x : TangentBundle 𝓘(ℝ,E) M)))
183     (hs : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F) ∞ s) (v : TangentSpace 𝓘(ℝ,E) x) :
184     mvfderiv 𝓘(ℝ,E) (nabla 𝓘(ℝ,E) P Y s) x v =
185       P x (mvfderiv 𝓘(ℝ,E) (fun y => mvfderiv 𝓘(ℝ,E) s y (Y y)) x v) +
186       mvfderiv 𝓘(ℝ,E) P x v (mvfderiv 𝓘(ℝ,E) s x (Y x)) :=
187   derivative_clm_apply P _ x (hP.mdifferentiableAt (by simp))
188     ((smooth_directional 𝓘(ℝ,E) s Y hs hY).mdifferentiableAt (by simp)) v
189 
190 /-- Cancellation of second derivatives uses the actual manifold Lie bracket. -/
191 theorem curvature_expansion (P : M → F →L[ℝ] F)
192     (X Y : ∀ x : M, TangentSpace 𝓘(ℝ,E) x) (s : M → F) (x : M)
193     (hP : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F →L[ℝ] F) ∞ P) (hPP : ∀ x, P x*P x=P x)
194     (hX : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞
195       (fun x => (X x : TangentBundle 𝓘(ℝ,E) M)))
196     (hY : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞
197       (fun x => (Y x : TangentBundle 𝓘(ℝ,E) M)))
198     (hs : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F) ∞ s) :
199     curvature 𝓘(ℝ,E) P X Y s x =
200       P x (mvfderiv 𝓘(ℝ,E) P x (X x) (mvfderiv 𝓘(ℝ,E) s x (Y x))) -
201       P x (mvfderiv 𝓘(ℝ,E) P x (Y x) (mvfderiv 𝓘(ℝ,E) s x (X x))) := by
202   have hp (z : F) : P x (P x z)=P x z :=
203     congrArg (fun L : F →L[ℝ] F => L z) (hPP x)
204   have hb := derivative_lieBracket s hs X Y hX hY x
205   unfold curvature
206   simp only [nabla]
207   rw [nabla_derivative P Y s x hP hY hs (X x),nabla_derivative P X s x hP hX hs (Y x)]
208   simp only [map_add,hp,hb,map_sub]
209   abel
210 
211 /-- Item 6.4: the global projected connection has curvature P(dP wedge dP)P.
212 The ambient manifold may require arbitrarily many charts. All differential operators,
213 vector fields and the Lie bracket here are the actual Mathlib manifold constructions. -/
214 theorem projected_connection_curvature (P : M → F →L[ℝ] F)
215     (X Y : ∀ x : M, TangentSpace 𝓘(ℝ,E) x) (s : M → F) (x : M)
216     (hP : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F →L[ℝ] F) ∞ P) (hPP : ∀ x, P x*P x=P x)
217     (hX : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞
218       (fun x => (X x : TangentBundle 𝓘(ℝ,E) M)))
219     (hY : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞
220       (fun x => (Y x : TangentBundle 𝓘(ℝ,E) M)))
221     (hs : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F) ∞ s) (hPs : ∀ x, P x (s x)=s x) :
222     curvature 𝓘(ℝ,E) P X Y s x = curvatureForm 𝓘(ℝ,E) P x (X x) (Y x) (s x) := by
223   have hP1 := hP.mdifferentiableAt (x := x) (by simp)
224   have hs1 := hs.mdifferentiableAt (x := x) (by simp)
225   have hz (v : TangentSpace 𝓘(ℝ,E) x) (z : F) : P x (mvfderiv 𝓘(ℝ,E) P x v (P x z))=0 := by
226     have hh := congrArg (fun L : F →L[ℝ] F => L z)
227       (projector_differential_sandwich P x hP1 hPP v)
228     simpa [mul_apply_eq_comp] using hh
229   rw [curvature_expansion P X Y s x hP hPP hX hY hs]
230   conv_lhs => rw [section_jet P s x hP1 hs1 hPs (Y x),section_jet P s x hP1 hs1 hPs (X x)]
231   simp only [map_add,hz,add_zero]
232   simp [curvatureForm,hPs,map_sub]
233 
234 /-- The global curvature is tensorial: its value depends only on the two tangent vectors
235 and the section value at the point, not on their extensions. -/
236 theorem curvature_is_tensorial (P : M → F →L[ℝ] F)
237     (hP : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F →L[ℝ] F) ∞ P) (hPP : ∀ x, P x*P x=P x)
238     (X Y X' Y' : ∀ x : M, TangentSpace 𝓘(ℝ,E) x) (s t : M → F) (x : M)
239     (hX : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞ (fun x => (X x : TangentBundle 𝓘(ℝ,E) M)))
240     (hY : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞ (fun x => (Y x : TangentBundle 𝓘(ℝ,E) M)))
241     (hX' : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞ (fun x => (X' x : TangentBundle 𝓘(ℝ,E) M)))
242     (hY' : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,E).tangent ∞ (fun x => (Y' x : TangentBundle 𝓘(ℝ,E) M)))
243     (hs : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F) ∞ s) (ht : ContMDiff 𝓘(ℝ,E) 𝓘(ℝ,F) ∞ t)
244     (hPs : ∀ x, P x (s x)=s x) (hPt : ∀ x, P x (t x)=t x)
245     (hXX : X x=X' x) (hYY : Y x=Y' x) (hst : s x=t x) :
246     curvature 𝓘(ℝ,E) P X Y s x=curvature 𝓘(ℝ,E) P X' Y' t x := by
247   rw [projected_connection_curvature P X Y s x hP hPP hX hY hs hPs,
248     projected_connection_curvature P X' Y' t x hP hPP hX' hY' ht hPt,hXX,hYY,hst]
249 
250 end KomorebiPaperVII.ManifoldCurvature
251 
252 
253 /-! Declaration-level dependency audit. -/
254 #print axioms KomorebiPaperVII.ManifoldCurvature.derivative_in_chart
255 #print axioms KomorebiPaperVII.ManifoldCurvature.differentiable_in_chart
256 #print axioms KomorebiPaperVII.ManifoldCurvature.smooth_in_chart
257 #print axioms KomorebiPaperVII.ManifoldCurvature.derivative_clm_apply
258 #print axioms KomorebiPaperVII.ManifoldCurvature.chartField_self
259 #print axioms KomorebiPaperVII.ManifoldCurvature.chartField_differentiable
260 #print axioms KomorebiPaperVII.ManifoldCurvature.bracket_in_chart
261 #print axioms KomorebiPaperVII.ManifoldCurvature.directional_chart_pullback
262 #print axioms KomorebiPaperVII.ManifoldCurvature.second_directional_in_chart
263 #print axioms KomorebiPaperVII.ManifoldCurvature.derivative_lieBracket
264 #print axioms KomorebiPaperVII.ManifoldCurvature.projector_jet
265 #print axioms KomorebiPaperVII.ManifoldCurvature.projector_differential_sandwich
266 #print axioms KomorebiPaperVII.ManifoldCurvature.section_jet
267 #print axioms KomorebiPaperVII.ManifoldCurvature.nabla_derivative
268 #print axioms KomorebiPaperVII.ManifoldCurvature.curvature_expansion
269 #print axioms KomorebiPaperVII.ManifoldCurvature.projected_connection_curvature
270 #print axioms KomorebiPaperVII.ManifoldCurvature.curvature_is_tensorial

Back to source controls