mathlib documentation

geometry.manifold.vector_bundle.tangent

Tangent bundles #

This file defines the tangent bundle as a smooth vector bundle.

Let M be a smooth manifold with corners with model I on (E, H). We define the tangent bundle of M using the vector_bundle_core construction indexed by the charts of M with fibers E. Given two charts i, j : local_homeomorph M H, the coordinate change between i and j at a point x : M is the derivative of the composite

  I.symm   i.symm    j     I
E -----> H -----> M --> H --> E

within the set range I βŠ† E at I (i x) : E. This defines a smooth vector bundle tangent_bundle with fibers tangent_space.

Main definitions #

Auxiliary lemma for tangent spaces: the derivative of a coordinate change between two charts is smooth on its source.

noncomputable def hidden.tangent_bundle_core {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners π•œ E H) (M : Type u_4) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] :

Let M be a smooth manifold with corners with model I on (E, H). Then vector_bundle_core I M is the vector bundle core for the tangent bundle over M. It is indexed by the atlas of M, with fiber E and its change of coordinates from the chart i to the chart j at point x : M is the derivative of the composite

  I.symm   i.symm    j     I
E -----> H -----> M --> H --> E

within the set range I βŠ† E at I (i x) : E.

Equations
Instances for hidden.tangent_bundle_core
@[simp]
theorem hidden.tangent_bundle_core_index_at {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners π•œ E H) (M : Type u_4) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (x : M) :
@[nolint]
def hidden.tangent_space {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners π•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (x : M) :
Type u_2

The tangent space at a point of the manifold M. It is just E. We could use instead (tangent_bundle_core I M).to_topological_vector_bundle_core.fiber x, but we use E to help the kernel.

Equations
Instances for hidden.tangent_space
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[nolint, reducible]
def hidden.tangent_bundle {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners π•œ E H) (M : Type u_4) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] :
Type (max u_4 u_2)

The tangent bundle to a smooth manifold, as a Sigma type. Defined in terms of bundle.total_space to be able to put a suitable topology on it.

Equations
@[protected, instance]
def hidden.tangent_space.module {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners π•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (x : M) :
Equations
@[protected, instance]
def hidden.tangent_space.inhabited {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [normed_add_comm_group E] [normed_space π•œ E] {H : Type u_3} [topological_space H] (I : model_with_corners π•œ E H) {M : Type u_4} [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (x : M) :
Equations
@[protected, instance]
@[protected, instance]

The tangent bundle to the model space #

@[simp]

In the tangent bundle to the model space, the charts are just the canonical identification between a product type and a sigma type, a.k.a. equiv.sigma_equiv_prod.

The canonical identification between the tangent bundle to the model space and the product, as a homeomorphism

Equations