# mathlibdocumentation

geometry.manifold.tangent_bundle

# Basic smooth bundles #

In general, a smooth bundle is a bundle over a smooth manifold, whose fiber is a manifold, and for which the coordinate changes are smooth. In this definition, there are charts involved at several places: in the manifold structure of the base, in the manifold structure of the fibers, and in the local trivializations. This makes it a complicated object in general. There is however a specific situation where things are much simpler: when the fiber is a vector space (no need for charts for the fibers), and when the local trivializations of the bundle and the charts of the base coincide. Then everything is expressed in terms of the charts of the base, making for a much simpler overall structure, which is easier to manipulate formally.

Most vector bundles that naturally occur in differential geometry are of this form: the tangent bundle, the cotangent bundle, differential forms (used to define de Rham cohomology) and the bundle of Riemannian metrics. Therefore, it is worth defining a specific constructor for this kind of bundle, that we call basic smooth bundles.

A basic smooth bundle is thus a smooth bundle over a smooth manifold whose fiber is a vector space, and which is trivial in the coordinate charts of the base. (We recall that in our notion of manifold there is a distinguished atlas, which does not need to be maximal: we require the triviality above this specific atlas). It can be constructed from a basic smooth bundled core, defined below, specifying the changes in the fiber when one goes from one coordinate chart to another one.

## Main definitions #

• basic_smooth_vector_bundle_core I M F: assuming that M is a smooth manifold over the model with corners I on (π, E, H), and F is a normed vector space over π, this structure registers, for each pair of charts of M, a linear change of coordinates on F depending smoothly on the base point. This is the core structure from which one will build a smooth vector bundle with fiber F over M.

Let Z be a basic smooth bundle core over M with fiber F. We define Z.to_vector_bundle_core, the (topological) vector bundle core associated to Z. From it, we get a space Z.to_vector_bundle_core.total_space (which as a Type is just Ξ£ (x : M), F), with the fiber bundle topology. It inherits a manifold structure (where the charts are in bijection with the charts of the basis). We show that this manifold is smooth.

Then we use this machinery to construct the tangent bundle of a smooth manifold.

• tangent_bundle_core I M: the basic smooth bundle core associated to a smooth manifold M over a model with corners I.
• tangent_bundle I M : the total space of tangent_bundle_core I M. It is itself a smooth manifold over the model with corners I.tangent, the product of I and the trivial model with corners on E.
• tangent_space I x : the tangent space to M at x
• tangent_bundle.proj I M: the projection from the tangent bundle to the base manifold

## Implementation notes #

We register the vector space structure on the fibers of the tangent bundle, but we do not register the normed space structure coming from that of F (as it is not canonical, and we also want to keep the possibility to add a Riemannian structure on the manifold later on without having two competing normed space instances on the tangent spaces).

We require F to be a normed space, and not just a topological vector space, as we want to talk about smooth functions on F. The notion of derivative requires a norm to be defined.

## TODO #

construct the cotangent bundle, and the bundles of differential forms. They should follow functorially from the description of the tangent bundle as a basic smooth bundle.

## Tags #

Smooth fiber bundle, vector bundle, tangent space, tangent bundle

structure basic_smooth_vector_bundle_core {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M] (F : Type u_5) [normed_space π F] :
Type (max u_3 u_4 u_5)

Core structure used to create a smooth bundle above M (a manifold over the model with corner I) with fiber the normed vector space F over π, which is trivial in the chart domains of M. This structure registers the changes in the fibers when one changes coordinate charts in the base. We require the change of coordinates of the fibers to be linear, so that the resulting bundle is a vector bundle.

Instances for basic_smooth_vector_bundle_core
def trivial_basic_smooth_vector_bundle_core {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M] (F : Type u_5) [normed_space π F] :

The trivial basic smooth bundle core, in which all the changes of coordinates are the identity.

Equations
@[protected, instance]
def basic_smooth_vector_bundle_core.inhabited {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] :
Equations
theorem basic_smooth_vector_bundle_core.coord_change_comp' {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) {i j k : β₯ M)} {x : M} (hi : x β i.val.to_local_equiv.source) (hj : x β j.val.to_local_equiv.source) (hk : x β k.val.to_local_equiv.source) (v : F) :
β(Z.coord_change j k (βj x)) (β(Z.coord_change i j (βi x)) v) = β(Z.coord_change i k (βi x)) v

A reformulation of coord_change_comp, formulated in terms of a point in M. The conditions on this point a significantly simpler than in coord_change_comp.

theorem basic_smooth_vector_bundle_core.coord_change_self' {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) {i : β₯ M)} {x : M} (hi : x β i.val.to_local_equiv.source) (v : F) :
β(Z.coord_change i i (βi x)) v = v

A reformulation of coord_change_self, formulated in terms of a point in M.

theorem basic_smooth_vector_bundle_core.coord_change_comp_eq_self {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (i j : β₯ M)) {x : H} (hx : x β (i.val.symm.trans j.val).to_local_equiv.source) (v : F) :
β(Z.coord_change j i (β(i.val.symm.trans j.val) x)) (β(Z.coord_change i j x) v) = v

Z.coord_change j i is a partial inverse of Z.coord_change i j.

theorem basic_smooth_vector_bundle_core.coord_change_comp_eq_self' {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) {i j : β₯ M)} {x : M} (hi : x β i.val.to_local_equiv.source) (hj : x β j.val.to_local_equiv.source) (v : F) :
β(Z.coord_change j i (βj x)) (β(Z.coord_change i j (βi x)) v) = v

Z.coord_change j i is a partial inverse of Z.coord_change i j, formulated in terms of a point in M.

theorem basic_smooth_vector_bundle_core.coord_change_continuous {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (i j : β₯ M)) :
theorem basic_smooth_vector_bundle_core.coord_change_smooth {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (i j : β₯ M)) :
def basic_smooth_vector_bundle_core.to_vector_bundle_core {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) :
M F β₯ M)

Vector bundle core associated to a basic smooth bundle core

Equations
@[simp]
theorem basic_smooth_vector_bundle_core.to_vector_bundle_core_coord_change {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (i j : β₯ M)) (x : M) :
= Z.coord_change i j (β(i.val) x)
@[simp]
theorem basic_smooth_vector_bundle_core.to_vector_bundle_core_index_at {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (x : M) :
= x
@[simp]
theorem basic_smooth_vector_bundle_core.base_set {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (i : β₯ M)) :
@[simp]
theorem basic_smooth_vector_bundle_core.target {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (i : β₯ M)) :
def basic_smooth_vector_bundle_core.chart {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) {e : H} (he : e β ) :

Local chart for the total space of a basic smooth bundle

Equations
theorem basic_smooth_vector_bundle_core.chart_apply {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) {x : M} (z : Z.to_vector_bundle_core.total_space) :
@[simp]
theorem basic_smooth_vector_bundle_core.chart_source {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (e : H) (he : e β ) :
@[simp]
theorem basic_smooth_vector_bundle_core.chart_target {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (e : H) (he : e β ) :
@[protected, instance]
def basic_smooth_vector_bundle_core.to_charted_space {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) :

The total space of a basic smooth bundle is endowed with a charted space structure, where the charts are in bijection with the charts of the basis.

Equations
theorem basic_smooth_vector_bundle_core.to_charted_space_chart_at {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (p : Z.to_vector_bundle_core.total_space) :
p = Z.chart _
theorem basic_smooth_vector_bundle_core.mem_atlas_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (f : F)) :
β β (e : H) (he : e β , f = Z.chart he
@[simp]
theorem basic_smooth_vector_bundle_core.mem_chart_source_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (p q : Z.to_vector_bundle_core.total_space) :
@[simp]
theorem basic_smooth_vector_bundle_core.mem_chart_target_iff {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (p : H Γ F) (q : Z.to_vector_bundle_core.total_space) :
@[simp]
theorem basic_smooth_vector_bundle_core.coe_chart_at_fst {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (p q : Z.to_vector_bundle_core.total_space) :
(β q) p).fst = β p.fst
@[simp]
theorem basic_smooth_vector_bundle_core.coe_chart_at_symm_fst {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) (p : H Γ F) (q : Z.to_vector_bundle_core.total_space) :
@[protected, instance]
def basic_smooth_vector_bundle_core.to_smooth_manifold {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} {I : E H} {M : Type u_4} [ M] {F : Type u_5} [normed_space π F] (Z : F) :

Smooth manifold structure on the total space of a basic smooth bundle

noncomputable def tangent_bundle_core {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M]  :

Basic smooth bundle core version of the tangent bundle of a smooth manifold M modelled over a model with corners I on (E, H). The fibers are equal to E, and the coordinate change in the fiber corresponds to the derivative of the coordinate change in M.

Equations
@[simp]
theorem tangent_bundle_core_coord_change {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M] (i j : β₯ M)) (x : H) :
@[nolint]
def tangent_space {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) {M : Type u_4} [ 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_vector_bundle_core.fiber x, but we use E to help the kernel.

Equations
• = E
Instances for tangent_space
@[nolint, reducible]
def tangent_bundle {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ 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
def tangent_bundle.proj {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M]  :

The projection from the tangent bundle of a smooth manifold to the manifold. As the tangent bundle is represented internally as a sigma type, the notation p.1 also works for the projection of the point p.

Equations
• = Ξ» (p : M), p.fst
@[simp]
theorem tangent_bundle.proj_apply {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] (x : M) (v : x) :
@[protected, instance]
def tangent_space.topological_space {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] (x : M) :
Equations
@[protected, instance]
def tangent_space.add_comm_group {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] (x : M) :
Equations
@[protected, instance]
def tangent_space.topological_add_group {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] (x : M) :
@[protected, instance]
def tangent_space.module {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] (x : M) :
module π x)
Equations
@[protected, instance]
def tangent_space.inhabited {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) {M : Type u_4} [ M] (x : M) :
Equations
@[protected, instance]
noncomputable def tangent_bundle.topological_space {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M]  :
Equations
@[protected, instance]
noncomputable def tangent_bundle.charted_space {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M]  :
Equations
@[protected, instance]
def tangent_bundle.smooth_manifold_with_corners {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M]  :
@[protected, instance]
noncomputable def tangent_space.fiber_bundle {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M]  :
Equations
@[protected, instance]
def tangent_space.vector_bundle {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M]  :
vector_bundle π E
theorem tangent_bundle_proj_continuous {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M]  :

The tangent bundle projection on the basis is a continuous map.

theorem tangent_bundle_proj_open {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (M : Type u_4) [ M]  :

The tangent bundle projection on the basis is an open map.

@[simp]
theorem tangent_bundle_model_space_chart_at {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (p : H) :

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.

@[simp]
theorem tangent_bundle_model_space_coe_chart_at {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (p : H) :
β p) =
@[simp]
theorem tangent_bundle_model_space_coe_chart_at_symm {π : Type u_1} {E : Type u_2} [normed_space π E] {H : Type u_3} (I : E H) (p : H) :
def tangent_bundle_model_space_homeomorph {π : Type u_1} {E : Type u_2} [normed_space π E] (H : Type u_3) (I : E H) :

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

Equations
@[simp]
theorem tangent_bundle_model_space_homeomorph_coe {π : Type u_1} {E : Type u_2} [normed_space π E] (H : Type u_3) (I : E H) :
@[simp]
theorem tangent_bundle_model_space_homeomorph_coe_symm {π : Type u_1} {E : Type u_2} [normed_space π E] (H : Type u_3) (I : E H) :