Basic facts about tangent spaces

The tangent space TangentSpace I x of a manifold modelled on I : ModelWithCorners 𝕜 E H is linearly equivalent to the model vector space E, so its dimension is that of E. Tangent spaces at propositionally equal points are identified by tangentSpaceCast.

Main results

• TauCeti.finrank_tangentSpace: the tangent space at any point has the dimension of the model vector space.
• TauCeti.heq_tangentSpaceCast: over equal base points, tangentSpaceCast is heterogeneously the identity.

@[simp]

theorem TauCeti.finrank_tangentSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] (x : M) : Module.finrank 𝕜 (TangentSpace I x) = Module.finrank 𝕜 E

The tangent space at any point of a manifold has the dimension of the model vector space.

theorem TauCeti.heq_tangentSpaceCast {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {x y : M} (hxy : x = y) (w : TangentSpace I x) : (tangentSpaceCast I x y) w ≍ w

Over equal base points, tangentSpaceCast is heterogeneously the identity. This identifies tangent vectors over base points that agree only propositionally, for instance when comparing points of tangent bundles with Bundle.TotalSpace.ext.