Tangent spaces along the zero section

The tangent space of a vector bundle at its zero vector splits canonically into the tangent space of the base and the fibre. The horizontal summand is the differential of the zero section; the vertical summand is the velocity of scalar multiplication through zero. Neither a connection nor a norm on the individual fibres is needed.

This decomposition lets one compute the total differential of a map out of a vector bundle from its restriction to the zero section and its derivatives along the fibres. In particular, these are the two parts of the differential of the normal exponential in the tubular neighbourhood theorem.

The horizontal computation generalizes Mathlib's TangentBundle.tangentMap_tangentBundle_pure, by Sébastien Gouëzel and Floris van Doorn, from tangent bundles to vector bundles. The vertical computation uses the scalar-curve case Bundle.TotalSpace.hasMFDerivAt_smul_curve of the total-space curve criterion.

References

• J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.

noncomputable def TauCeti.Bundle.zeroSectionTangentEquiv {𝕜 : Type u_1} {B : Type u_2} {E : Type u_3} {H : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace B] [ChartedSpace H B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] (b : B) : TangentSpace (I.prod (modelWithCornersSelf 𝕜 F)) (Bundle.zeroSection F V b) ≃L[𝕜] TangentSpace I b × V b

The tangent space at a zero vector, identified with the base tangent space times the fibre. The intrinsic characterization is given by zeroSectionTangentEquiv_mfderiv_zeroSection and zeroSectionTangentEquiv_symm_inr.

theorem TauCeti.Bundle.zeroSectionTangentEquiv_apply {𝕜 : Type u_1} {B : Type u_2} {E : Type u_3} {H : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace B] [ChartedSpace H B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] (b : B) (w : TangentSpace (I.prod (modelWithCornersSelf 𝕜 F)) (Bundle.zeroSection F V b)) : (zeroSectionTangentEquiv b) w = (w.1, (Bundle.Trivialization.symmL 𝕜 (trivializationAt F V b) b) w.2)

The splitting retains the base tangent coordinate and converts the preferred fibre coordinate back to an intrinsic fibre vector.

theorem TauCeti.Bundle.zeroSectionTangentEquiv_symm_apply {𝕜 : Type u_1} {B : Type u_2} {E : Type u_3} {H : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace B] [ChartedSpace H B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] (b : B) (w : TangentSpace I b × V b) : (zeroSectionTangentEquiv b).symm w = (w.1, (Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt F V b) b) w.2)

The inverse splitting reads the fibre vector in the preferred trivialization.

theorem TauCeti.Bundle.zeroSectionTangentEquiv_symm_inr {𝕜 : Type u_1} {B : Type u_2} {E : Type u_3} {H : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace B] [ChartedSpace H B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] (b : B) (v : V b) : (zeroSectionTangentEquiv b).symm (0, v) = ((mfderiv% fun (t : 𝕜) => ⟨b, t • v⟩) 0) 1

A fibre vector gives the vertical tangent vector via the velocity of its scalar line through zero.

theorem TauCeti.Bundle.mfderiv_zeroSection {𝕜 : Type u_1} {B : Type u_2} {E : Type u_3} {H : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace B] [ChartedSpace H B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] [IsManifold I 1 B] [ContMDiffVectorBundle 1 F V I] (b : B) : mfderiv% (Bundle.zeroSection F V) b = ContinuousLinearMap.inl 𝕜 (TangentSpace I b) F

In preferred tangent coordinates, the differential of the zero section is the first summand inclusion.

@[simp]

theorem TauCeti.Bundle.zeroSectionTangentEquiv_mfderiv_zeroSection {𝕜 : Type u_1} {B : Type u_2} {E : Type u_3} {H : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace B] [ChartedSpace H B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] [IsManifold I 1 B] [ContMDiffVectorBundle 1 F V I] (b : B) (u : TangentSpace I b) : (zeroSectionTangentEquiv b) ((mfderiv% (Bundle.zeroSection F V) b) u) = (u, 0)

The differential of the zero section is the horizontal summand of the canonical splitting.

theorem TauCeti.Bundle.zeroSectionTangentEquiv_symm_eq {𝕜 : Type u_1} {B : Type u_2} {E : Type u_3} {H : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace B] [ChartedSpace H B] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {V : B → Type u_6} [(b : B) → AddCommMonoid (V b)] [(b : B) → Module 𝕜 (V b)] [(b : B) → TopologicalSpace (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle 𝕜 F V] [IsManifold I 1 B] [ContMDiffVectorBundle 1 F V I] (b : B) (u : TangentSpace I b) (v : V b) : (zeroSectionTangentEquiv b).symm (u, v) = (mfderiv% (Bundle.zeroSection F V) b) u + (zeroSectionTangentEquiv b).symm (0, v)

The inverse splitting is the sum of the differential of the zero section and the velocity of the scalar line through the given fibre vector. This characterizes the splitting without reference to a trivialization.