Differentiating a curve into the total space of a fibre bundle

A curve z into the total space of a fibre bundle is read, near a parameter t, in the chart of the total space centred at z t. By FiberBundle.extChartAt that chart is the trivialization at the base point (z t).proj followed by the base chart there, so the reading of z is the pair of its base curve read in the base chart and of its fibre coordinate read in that trivialization. This file turns that observation into a criterion: the curve has a manifold derivative within a parameter set exactly when it is continuous there and those two coordinate readings have derivatives.

The criterion is the form in which a curve into a vector bundle is compared with a pair of ordinary derivatives, and in particular the form in which an integral curve of a vector field on a tangent bundle is unpacked into an equation on its base curve and one on its velocity.

Main results

• TauCeti.Manifold.hasMFDerivWithinAt_totalSpace_curve_iff: the manifold derivative of a curve into a total space, within a parameter set, read as the pair of the derivative of its base curve in the base chart and of the derivative of its fibre coordinate in the trivialization, both taken at the current point of the curve.
• TauCeti.Manifold.hasMFDerivAt_totalSpace_curve_iff: its unrestricted case.
• TauCeti.Manifold.extChartAt_totalSpace_apply_snd: the fibre coordinate of a point in a chart of the total space is its fibre coordinate in the trivialization at the centre of the chart.
• Bundle.TotalSpace.hasMFDerivAt_smul_curve: in a vector bundle, the velocity of a scalar curve r ↦ f r • z through the fibre of z.
• TauCeti.Manifold.hasMFDerivAt_totalSpaceMk_add_smul: in a vector bundle, the velocity of a straight line r ↦ a + r • b in the fibre over x.

theorem TauCeti.Manifold.extChartAt_totalSpace_apply_snd {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {V : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] (x y : Bundle.TotalSpace F V) : (↑(extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x) y).2 = (↑(trivializationAt F V x.proj) y).2

The fibre coordinate of a point y in the chart of the total space at x is its fibre coordinate in the trivialization at x.proj: by FiberBundle.extChartAt that chart is the trivialization followed by a chart of the base, which leaves the fibre coordinate unchanged.

theorem TauCeti.Manifold.hasMFDerivWithinAt_totalSpace_curve_iff_of_continuousWithinAt {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {V : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] {z : 𝕜 → Bundle.TotalSpace F V} {s : Set 𝕜} {t : 𝕜} {a : EB} {b : F} (hz : ContinuousWithinAt z s t) : HasMFDerivAt[s] z t (ContinuousLinearMap.smulRight 1 (a, b)) ↔ HasDerivWithinAt (fun (r : 𝕜) => ↑(extChartAt IB (z t).proj) (z r).proj) a s t ∧ HasDerivWithinAt (fun (r : 𝕜) => (↑(trivializationAt F V (z t).proj) (z r)).2) b s t

A curve into the total space which is continuous within s at t has a manifold derivative there exactly when its base curve, read in the base chart at the current base point, and its fibre coordinate, read in the trivialization at that same point, have the corresponding derivatives. This is TauCeti.Manifold.hasMFDerivWithinAt_totalSpace_curve_iff with the continuity of the curve supplied as a hypothesis rather than as a conjunct.

theorem TauCeti.Manifold.hasMFDerivWithinAt_totalSpace_curve_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {V : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] {z : 𝕜 → Bundle.TotalSpace F V} {s : Set 𝕜} {t : 𝕜} {a : EB} {b : F} : HasMFDerivAt[s] z t (ContinuousLinearMap.smulRight 1 (a, b)) ↔ ContinuousWithinAt z s t ∧ HasDerivWithinAt (fun (r : 𝕜) => ↑(extChartAt IB (z t).proj) (z r).proj) a s t ∧ HasDerivWithinAt (fun (r : 𝕜) => (↑(trivializationAt F V (z t).proj) (z r)).2) b s t

The manifold derivative of a curve into a total space. A curve into the total space of a fibre bundle has the manifold derivative determined by (a, b) within the parameter set s at t exactly when it is continuous there, its base curve read in the base chart at the current base point has derivative a, and its fibre coordinate read in the trivialization at that point has derivative b.

theorem TauCeti.Manifold.hasMFDerivAt_totalSpace_curve_iff {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {V : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] {z : 𝕜 → Bundle.TotalSpace F V} {t : 𝕜} {a : EB} {b : F} : HasMFDerivAt% z t (ContinuousLinearMap.smulRight 1 (a, b)) ↔ ContinuousAt z t ∧ HasDerivAt (fun (r : 𝕜) => ↑(extChartAt IB (z t).proj) (z r).proj) a t ∧ HasDerivAt (fun (r : 𝕜) => (↑(trivializationAt F V (z t).proj) (z r)).2) b t

The unrestricted case of TauCeti.Manifold.hasMFDerivWithinAt_totalSpace_curve_iff.

theorem Bundle.TotalSpace.trivializationAt_smul_snd {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {V : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] [TopologicalSpace B] [FiberBundle F V] [(x : B) → AddCommMonoid (V x)] [(x : B) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (y : TotalSpace F V) (c : 𝕜) : (↑(trivializationAt F V y.proj) ⟨y.proj, c • y.snd⟩).2 = c • (↑(trivializationAt F V y.proj) y).2

The fibre coordinate of c • y is c times that of y, by linearity of the trivialization at the base point of y.

theorem Bundle.TotalSpace.hasMFDerivAt_smul_curve {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {V : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] {t : 𝕜} [(x : B) → AddCommMonoid (V x)] [(x : B) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (y : TotalSpace F V) {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' t) : HasMFDerivAt% (fun (r : 𝕜) => ⟨y.proj, f r • y.snd⟩) t (ContinuousLinearMap.smulRight 1 (0, f' • (↑(trivializationAt F V y.proj) y).2))

If f has derivative f' at t, then the curve r ↦ f r • y in the fibre of y has velocity (0, f' • ξ) at t, read in the chart at y, where ξ is the fibre coordinate of y.

theorem TauCeti.Manifold.hasMFDerivAt_totalSpaceMk_add_smul {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} {V : B → Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (Bundle.TotalSpace F V)] [(x : B) → TopologicalSpace (V x)] {EB : Type u_5} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type u_6} [TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [TopologicalSpace B] [ChartedSpace HB B] [FiberBundle F V] [(x : B) → AddCommMonoid (V x)] [(x : B) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] (x : B) (a b : V x) : HasMFDerivAt% (fun (r : 𝕜) => ⟨x, a + r • b⟩) 0 (ContinuousLinearMap.smulRight 1 (0, (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F V x) x) b))

The velocity of a line in a fibre. In the fibre of a vector bundle over x, the line r ↦ a + r • b has velocity (0, ξ) at r = 0, read in the chart at a, where ξ is the fibre coordinate of b in the trivialization at x.