ProjectedBundleCompletion.lean

1 module
2 public import ManifoldProjectedCurvature
3 public import Mathlib.Tactic
4 /-! Author: Komorebi P. Paper VII, item 6.4.
5 Intrinsic atlas, section and gauge compatibility for the constructed global range bundle.
6 The explicit atlas is used directly; no bundle, gluing or curvature hypothesis is supplied.
7 -/
8 @[expose] public section
9 set_option autoImplicit false
10 set_option backward.isDefEq.respectTransparency false
11 set_option backward.isDefEq.respectTransparency.types false
12 set_option linter.unusedSectionVars false
13 open scoped Manifold ContDiff Topology
14 open Set Filter
15 noncomputable section
16 namespace KomorebiPaperVII.BundleCompletion
17 open KomorebiPaperVII.RangeBundle KomorebiPaperVII.GlobalConnection
18 
19 variable {E H M F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
20   [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
21   [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
22   [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
23 
24 /-- The actual total-space trivialization domains are open. -/
25 theorem total_domain_open (P : M → F →L[ℝ] F)
26     (hP : ContMDiff I 𝓘(ℝ,F →L[ℝ] F) ∞ P) (a : M) :
27     IsOpen {z : Total P | z.val.1 ∈ domain P a} :=
28   (isOpen_domain P hP.continuous a).preimage continuous_subtype_val.fst
29 
30 /-- The transition formula applies to the actual local product homeomorphisms. -/
31 theorem localProduct_overlap (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
32     (hP : ContMDiff I 𝓘(ℝ,F →L[ℝ] F) ∞ P) (a b x : M)
33     (hxa : x ∈ domain P a) (hxb : x ∈ domain P b) (v : fiber (P a)) :
34     localProduct P hPP hP b
35       ⟨((localProduct P hPP hP a).symm (⟨x,hxa⟩,v)).val,hxb⟩ =
36       (⟨x,hxb⟩,transition P hPP a b x v) := rfl
37 
38 /-- Smoothness in the actual bundle coordinates is equivalent to ambient smoothness.
39 Only a local range condition near the point is required. -/
40 theorem smooth_section_iff (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
41     (hP : ContMDiff I 𝓘(ℝ,F →L[ℝ] F) ∞ P) (a x : M) (hx : x ∈ domain P a)
42     (s : M → F) (hPs : ∀ᶠ y in 𝓝 x, P y (s y)=s y) :
43     ContMDiffAt I 𝓘(ℝ,F) ∞ s x ↔
44       ContMDiffAt I 𝓘(ℝ,fiber (P a)) ∞ (fun y => toCoord P hPP a y (s y)) x := by
45   constructor
46   · intro hs
47     exact ((smooth_toCoord P hPP hP a x hx).contMDiffAt
48       ((isOpen_domain P hP.continuous a).mem_nhds hx)).clm_apply hs
49   · intro hs
50     have hr := (smooth_fromCoord P hP a x).clm_apply hs
51     apply hr.congr_of_eventuallyEq
52     filter_upwards [hPs,(isOpen_domain P hP.continuous a).mem_nhds hx] with y hy hya
53     exact (fromCoord_toCoord P hPP a y hya (s y) hy).symm
54 
55 /-- The local connection obeys the full change-of-coordinate law for arbitrary local
56 coordinate functions, without assuming a global section or its smooth extension. -/
57 theorem local_connections_gauge (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
58     (hP : ContMDiff I 𝓘(ℝ,F →L[ℝ] F) ∞ P) (a b x : M)
59     (hx : x ∈ domain P a ∩ domain P b) (X : ∀ y : M, TangentSpace I y)
60     (u : M → fiber (P a)) :
61     localNabla I P hPP b X (fun y => transition P hPP a b y (u y)) x =
62       transition P hPP a b x (localNabla I P hPP a X u x) := by
63   have hs : ∀ y, P y (fromCoord P a y (u y))=fromCoord P a y (u y) :=
64     fun y => fromCoord_range P hPP a y (u y)
65   change localNabla I P hPP b X (fun y => toCoord P hPP b y (fromCoord P a y (u y))) x = _
66   rw [localNabla_represents_global I P hPP hP b X (fun y => fromCoord P a y (u y)) hs x hx.2]
67   change toCoord P hPP b x (nabla I P X (fun y => fromCoord P a y (u y)) x) =
68     toCoord P hPP b x (fromCoord P a x
69       (toCoord P hPP a x (nabla I P X (fun y => fromCoord P a y (u y)) x)))
70   rw [fromCoord_toCoord P hPP a x hx.1 _ (nabla_in_range I P hPP X _ x)]
71 
72 /-- Curvature is an alternating two-form, with values in the actual range endomorphisms. -/
73 theorem curvatureForm_self (P : M → F →L[ℝ] F) (x : M) (v : TangentSpace I x) :
74     curvatureForm I P x v v=0 := by simp [curvatureForm]
75 
76 theorem curvatureForm_swap (P : M → F →L[ℝ] F) (x : M) (v w : TangentSpace I x) :
77     curvatureForm I P x v w = -curvatureForm I P x w v := by
78   unfold curvatureForm
79   noncomm_ring
80 
81 theorem curvatureForm_add_left (P : M → F →L[ℝ] F) (x : M) (u v w : TangentSpace I x) :
82     curvatureForm I P x (u+v) w=curvatureForm I P x u w+curvatureForm I P x v w := by
83   simp only [curvatureForm,map_add]
84   noncomm_ring
85 
86 theorem curvatureForm_smul_left (P : M → F →L[ℝ] F) (x : M) (c : ℝ) (v w : TangentSpace I x) :
87     curvatureForm I P x (c • v) w=c • curvatureForm I P x v w := by
88   simp only [curvatureForm,map_smul,smul_mul_assoc,mul_smul_comm,← smul_sub]
89 
90 theorem curvatureForm_in_range (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
91     (x : M) (v w : TangentSpace I x) (z : F) :
92     P x (curvatureForm I P x v w z)=curvatureForm I P x v w z := by
93   have hh : P x*curvatureForm I P x v w=curvatureForm I P x v w := by
94     simp only [curvatureForm,← mul_assoc,hPP]
95   exact congrArg (fun L : F →L[ℝ] F => L z) hh
96 
97 /-- Curvature as an endomorphism of the actual fiber, not just of the ambient space. -/
98 def fiberCurvature (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
99     (x : M) (v w : TangentSpace I x) : fiber (P x) →L[ℝ] fiber (P x) :=
100   ((curvatureForm I P x v w).codRestrict (fiber (P x))
101     (curvatureForm_in_range P hPP x v w)).comp (fiber (P x)).subtypeL
102 
103 @[simp] theorem fiberCurvature_coe (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
104     (x : M) (v w : TangentSpace I x) (z : fiber (P x)) :
105     (fiberCurvature P hPP x v w z : F)=curvatureForm I P x v w z := rfl
106 
107 /-- Zero, identity and all constant projector bundles have vanishing curvature form. -/
108 theorem constant_projector_flat (p : F →L[ℝ] F) (x : M) (v w : TangentSpace I x) :
109     curvatureForm I (fun _ : M => p) x v w=0 := by simp [curvatureForm,mvfderiv_const]
110 
111 /-- Smoothness of range sections does not depend on the chosen bundle chart. -/
112 theorem smooth_section_chart_independent (P : M → F →L[ℝ] F) (hPP : ∀ x, P x*P x=P x)
113     (hP : ContMDiff I 𝓘(ℝ,F →L[ℝ] F) ∞ P) (a b x : M)
114     (hx : x ∈ domain P a ∩ domain P b) (s : M → F)
115     (hPs : ∀ᶠ y in 𝓝 x, P y (s y)=s y) :
116     ContMDiffAt I 𝓘(ℝ,fiber (P a)) ∞ (fun y => toCoord P hPP a y (s y)) x ↔
117     ContMDiffAt I 𝓘(ℝ,fiber (P b)) ∞ (fun y => toCoord P hPP b y (s y)) x :=
118   (smooth_section_iff P hPP hP a x hx.1 s hPs).symm.trans
119     (smooth_section_iff P hPP hP b x hx.2 s hPs)
120 
121 end KomorebiPaperVII.BundleCompletion
122 
123 /-! Declaration-level dependency audit. -/
124 #print axioms KomorebiPaperVII.BundleCompletion.total_domain_open
125 #print axioms KomorebiPaperVII.BundleCompletion.localProduct_overlap
126 #print axioms KomorebiPaperVII.BundleCompletion.smooth_section_iff
127 #print axioms KomorebiPaperVII.BundleCompletion.local_connections_gauge
128 #print axioms KomorebiPaperVII.BundleCompletion.curvatureForm_self
129 #print axioms KomorebiPaperVII.BundleCompletion.curvatureForm_swap
130 #print axioms KomorebiPaperVII.BundleCompletion.curvatureForm_add_left
131 #print axioms KomorebiPaperVII.BundleCompletion.curvatureForm_smul_left
132 #print axioms KomorebiPaperVII.BundleCompletion.curvatureForm_in_range
133 #print axioms KomorebiPaperVII.BundleCompletion.fiberCurvature_coe
134 #print axioms KomorebiPaperVII.BundleCompletion.constant_projector_flat
135 #print axioms KomorebiPaperVII.BundleCompletion.smooth_section_chart_independent

Back to source controls