English
The tangent bundle derivative along the zero section has a canonical splitting: it maps to a pair consisting of base-point tangent and zero fiber component.
Русский
Касательное отображение вдоль нулевой секции имеет каноническое разложение на основании и вертикального компонента.
LaTeX
$$$\forall p : TangentBundle I M,\; tangentMap I I.tangent (zeroSection E (TangentSpace I)) p = ⟨⟨p.proj, 0⟩, ⟨p.2, 0⟩⟩$$$
Lean4
/-- The derivative of the zero section of the tangent bundle maps `⟨x, v⟩` to `⟨⟨x, 0⟩, ⟨v, 0⟩⟩`.
Note that, as currently framed, this is a statement in coordinates, thus reliant on the choice
of the coordinate system we use on the tangent bundle.
However, the result itself is coordinate-dependent only to the extent that the coordinates
determine a splitting of the tangent bundle. Moreover, there is a canonical splitting at each
point of the zero section (since there is a canonical horizontal space there, the tangent space
to the zero section, in addition to the canonical vertical space which is the kernel of the
derivative of the projection), and this canonical splitting is also the one that comes from the
coordinates on the tangent bundle in our definitions. So this statement is not as crazy as it
may seem.
TODO define splittings of vector bundles; state this result invariantly. -/
theorem tangentMap_tangentBundle_pure [Is : IsManifold I 1 M] (p : TangentBundle I M) :
tangentMap I I.tangent (zeroSection E (TangentSpace I)) p = ⟨⟨p.proj, 0⟩, ⟨p.2, 0⟩⟩ :=
by
rcases p with ⟨x, v⟩
have N : I.symm ⁻¹' (chartAt H x).target ∈ 𝓝 (I ((chartAt H x) x)) :=
by
apply IsOpen.mem_nhds
· apply (OpenPartialHomeomorph.open_target _).preimage I.continuous_invFun
· simp only [mfld_simps]
have A : MDifferentiableAt I I.tangent (fun x => @TotalSpace.mk M E (TangentSpace I) x 0) x :=
haveI : ContMDiff I (I.prod 𝓘(𝕜, E)) ⊤ (zeroSection E (TangentSpace I : M → Type _)) :=
Bundle.contMDiff_zeroSection 𝕜 (TangentSpace I : M → Type _)
this.mdifferentiableAt le_top
have B : fderivWithin 𝕜 (fun x' : E ↦ (x', (0 : E))) (Set.range I) (I ((chartAt H x) x)) v = (v, 0) :=
by
rw [fderivWithin_eq_fderiv, DifferentiableAt.fderiv_prodMk]
· simp
· exact differentiableAt_fun_id
· exact differentiableAt_const _
· exact ModelWithCorners.uniqueDiffWithinAt_image I
· exact differentiableAt_id.prodMk (differentiableAt_const _)
simp +unfoldPartialApp only [Bundle.zeroSection, tangentMap, mfderiv, A, if_pos, chartAt,
FiberBundle.chartedSpace_chartAt, TangentBundle.trivializationAt_apply, Function.comp_def,
ContinuousLinearMap.map_zero, mfld_simps]
rw [← fderivWithin_inter N] at B
rw [← fderivWithin_inter N, ← B]
congr 1
refine fderivWithin_congr (fun y hy => ?_) ?_
· simp only [mfld_simps] at hy
simp only [hy, mfld_simps]
· simp only [mfld_simps]
