GlobalProjectedConnection.lean

1 module
2 public import GlobalRangeBundle
3 public import LocalProjectedCurvature
4 import all ProjectedCurvature
5 public import Mathlib.Geometry.Manifold.VectorField.LieBracket
6 public import Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
7 public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
8 public import Mathlib.Tactic
9 /-! Author: Komorebi P. Paper VII, item 6.4.
10 Actual global manifold derivative, range sections and atlas compatibility.
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.GlobalConnection
21 open KomorebiPaperVII.RangeBundle
22 
23 variable {E H M F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
24   [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
25   [TopologicalSpace M] [ChartedSpace H M]
26   [NormedAddCommGroup F] [NormedSpace ℝ F]
27 
28 /-- The global projected covariant derivative. -/
29 def nabla (P : M → F →L[ℝ] F) (X : ∀ x : M, TangentSpace I x) (s : M → F) (x : M) : F :=
30   P x (mvfderiv I s x (X x))
31 
32 /-- The global operator-valued two-form. -/
33 def curvatureForm (P : M → F →L[ℝ] F) (x : M) (v w : TangentSpace I x) : F →L[ℝ] F :=
34   P x * (mvfderiv I P x v * mvfderiv I P x w -
35     mvfderiv I P x w * mvfderiv I P x v) * P x
36 
37 /-- Actual covariant commutator with the manifold Lie bracket. -/
38 def curvature (P : M → F →L[ℝ] F) (X Y : ∀ x : M, TangentSpace I x)
39     (s : M → F) (x : M) : F :=
40   nabla I P X (nabla I P Y s) x - nabla I P Y (nabla I P X s) x -
41     nabla I P (VectorField.mlieBracket I X Y) s x
42 
43 /-- A connection as a section of Hom(TM, range P), not merely an ambient formula. -/
44 def covariant (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
45     (s : ∀ x, fiber (P x)) (x : M) : TangentSpace I x →L[ℝ] fiber (P x) :=
46   (project (P x) (hPP x)).comp (mvfderiv I (fun y => (s y : F)) x)
47 
48 theorem nabla_in_range (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
49     (X : ∀ x : M, TangentSpace I x) (s : M → F) (x : M) :
50     P x (nabla I P X s x)=nabla I P X s x :=
51   congrArg (fun q : F →L[ℝ] F => q (mvfderiv I s x (X x))) (hPP x)
52 
53 theorem nabla_add_sections (P : M → F →L[ℝ] F) (X : ∀ x : M, TangentSpace I x)
54     (s t : M → F) (x : M) (hs : MDifferentiableAt I 𝓘(ℝ,F) s x)
55     (ht : MDifferentiableAt I 𝓘(ℝ,F) t x) :
56     nabla I P X (s+t) x=nabla I P X s x+nabla I P X t x := by
57   simp [nabla,mvfderiv_add hs ht]
58 
59 theorem nabla_leibniz (P : M → F →L[ℝ] F) (X : ∀ x : M, TangentSpace I x)
60     (s : M → F) (c : M → ℝ) (x : M) (hs : MDifferentiableAt I 𝓘(ℝ,F) s x)
61     (hc : MDifferentiableAt I 𝓘(ℝ,ℝ) c x) (hPs : P x (s x)=s x) :
62     nabla I P X (c • s) x = (mvfderiv I c x (X x)) • s x + c x • nabla I P X s x := by
63   simp [nabla,mvfderiv_smul hc hs,hPs,add_comm]
64 
65 theorem nabla_add_vectors (P : M → F →L[ℝ] F) (X Y : ∀ x : M, TangentSpace I x)
66     (s : M → F) (x : M) :
67     nabla I P (X+Y) s x = nabla I P X s x+nabla I P Y s x := by simp [nabla]
68 
69 theorem nabla_smul_vector (P : M → F →L[ℝ] F) (X : ∀ x : M, TangentSpace I x)
70     (s : M → F) (c : M → ℝ) (x : M) :
71     nabla I P (c • X) s x=c x • nabla I P X s x := by simp [nabla]
72 
73 theorem nabla_germ (P : M → F →L[ℝ] F) (X : ∀ x : M, TangentSpace I x)
74     (s t : M → F) (x : M) (h : s =ᶠ[𝓝 x] t) : nabla I P X s x=nabla I P X t x := by
75   have hd : mvfderiv I s x=mvfderiv I t x := h.mfderiv_eq
76   simp only [nabla,hd]
77 
78 variable [IsManifold I ∞ M]
79 
80 /-- Differentiating a smooth vector-valued function along a smooth vector field is smooth. -/
81 theorem smooth_directional (s : M → F) (X : ∀ x : M, TangentSpace I x)
82     (hs : ContMDiff I 𝓘(ℝ,F) ∞ s)
83     (hX : ContMDiff I I.tangent ∞ (fun x => (X x : TangentBundle I M))) :
84     ContMDiff I 𝓘(ℝ,F) ∞ (fun x => mvfderiv I s x (X x)) := by
85   exact (contMDiff_snd_tangentBundle_modelSpace F 𝓘(ℝ,F)).comp
86     ((hs.contMDiff_tangentMap (m := ∞) (by simp)).comp hX)
87 
88 theorem smooth_nabla (P : M → F →L[ℝ] F) (s : M → F)
89     (X : ∀ x : M, TangentSpace I x)
90     (hP : ContMDiff I 𝓘(ℝ,F →L[ℝ] F) ∞ P) (hs : ContMDiff I 𝓘(ℝ,F) ∞ s)
91     (hX : ContMDiff I I.tangent ∞ (fun x => (X x : TangentBundle I M))) :
92     ContMDiff I 𝓘(ℝ,F) ∞ (nabla I P X s) := hP.clm_apply (smooth_directional I s X hs hX)
93 
94 variable [CompleteSpace F]
95 
96 /-- The local connection in the derived range coordinates. -/
97 def localNabla (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x) (a : M)
98     (X : ∀ x : M, TangentSpace I x) (u : M → fiber (P a)) (x : M) : fiber (P a) :=
99   toCoord P hPP a x (nabla I P X (fun y => fromCoord P a y (u y)) x)
100 
101 /-- Local reconstruction gives the same global connection on the whole open domain. -/
102 theorem localNabla_represents_global (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
103     (hP : ContMDiff I 𝓘(ℝ,F →L[ℝ] F) ∞ P) (a : M)
104     (X : ∀ x : M, TangentSpace I x) (s : M → F) (hPs : ∀ x, P x (s x)=s x)
105     (x : M) (hx : x ∈ domain P a) :
106     localNabla I P hPP a X (fun y => toCoord P hPP a y (s y)) x =
107       toCoord P hPP a x (nabla I P X s x) := by
108   unfold localNabla
109   congr 1
110   apply nabla_germ
111   filter_upwards [(isOpen_domain P hP.continuous a).mem_nhds hx] with y hy
112   exact fromCoord_toCoord P hPP a y hy (s y) (hPs y)
113 
114 /-- The constructed local connections agree on every overlap. -/
115 theorem local_connections_glue (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
116     (hP : ContMDiff I 𝓘(ℝ,F →L[ℝ] F) ∞ P) (a b : M)
117     (X : ∀ x : M, TangentSpace I x) (s : M → F) (hPs : ∀ x, P x (s x)=s x)
118     (x : M) (hx : x ∈ domain P a ∩ domain P b) :
119     transition P hPP a b x (localNabla I P hPP a X (fun y => toCoord P hPP a y (s y)) x) =
120       localNabla I P hPP b X (fun y => toCoord P hPP b y (s y)) x := by
121   rw [localNabla_represents_global I P hPP hP a X s hPs x hx.1,
122     localNabla_represents_global I P hPP hP b X s hPs x hx.2]
123   change toCoord P hPP b x (fromCoord P a x (toCoord P hPP a x (nabla I P X s x))) = _
124   rw [fromCoord_toCoord P hPP a x hx.1 _ (nabla_in_range I P hPP X s x)]
125 
126 end KomorebiPaperVII.GlobalConnection
127 
128 /-! Declaration-level dependency audit. -/
129 #print axioms KomorebiPaperVII.GlobalConnection.nabla_in_range
130 #print axioms KomorebiPaperVII.GlobalConnection.nabla_add_sections
131 #print axioms KomorebiPaperVII.GlobalConnection.nabla_leibniz
132 #print axioms KomorebiPaperVII.GlobalConnection.nabla_add_vectors
133 #print axioms KomorebiPaperVII.GlobalConnection.nabla_smul_vector
134 #print axioms KomorebiPaperVII.GlobalConnection.nabla_germ
135 #print axioms KomorebiPaperVII.GlobalConnection.smooth_directional
136 #print axioms KomorebiPaperVII.GlobalConnection.smooth_nabla
137 #print axioms KomorebiPaperVII.GlobalConnection.localNabla_represents_global
138 #print axioms KomorebiPaperVII.GlobalConnection.local_connections_glue

Back to source controls