Theorems · Theorem · global analysis

TangentBundle.tangentMap_tangentBundle_pure

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [Is : IsManifold I 1 M] (p : TangentBundle I M),
  tangentMap I I.tangent (Bundle.zeroSection E (TangentSpace I)) p = ⟨⟨p.proj, 0⟩, (p.snd, 0)⟩

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.

Defined in

Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Cited by

0 results in Mathlib

Foundations

Depth 217 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceIsManifold